diff options
Diffstat (limited to 'Day9.lean')
| -rw-r--r-- | Day9.lean | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -31,8 +31,8 @@ private def extrapolate : List Int → Int 0 else have : (differences (a :: as)).length < as.length + 1 := by - simp_arith[differences] - induction (as) <;> simp_arith[differences] + simp +arith[differences] + induction (as) <;> simp +arith[differences] case cons b bs hb => rw[←differences_length_independent_arg] assumption a + extrapolate (differences (a :: as)) |
