diff --git a/tasks/human_eval_138.rs b/tasks/human_eval_138.rs index 8a825d0..d0fff3b 100644 --- a/tasks/human_eval_138.rs +++ b/tasks/human_eval_138.rs @@ -9,7 +9,13 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +fn is_equal_to_sum_even(n: u32) -> (b: bool) + ensures + b <==> n % 2 == 0 && n >= 8 // 2 + 2 + 2 + (n - 6) + , +{ + n % 2 == 0 && n >= 8 +} } // verus! fn main() {}