We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 0bfeb51 commit f333e24Copy full SHA for f333e24
HumanEvalLean/HumanEval46.lean
@@ -37,8 +37,8 @@ def fib4Reference : Nat → Nat
37
| 1 => 0
38
| 2 => 2
39
| 3 => 0
40
- | (k + 4) =>
41
- fib4Reference (k + 4 - 1) + fib4Reference (k + 4 - 2) + fib4Reference (k + 4 - 3) + fib4Reference (k + 4 - 4)
+ | k + 4 =>
+ fib4Reference (k + 3) + fib4Reference (k + 2) + fib4Reference (k + 1) + fib4Reference k
42
43
theorem sum_mod_eq_sum {vec : Vector Nat 4} :
44
∀ i, vec[i % 4] + vec[(i + 1) % 4] + vec[(i + 2) % 4] + vec[(i + 3) % 4] =
0 commit comments