From 2a9261d1ba962deff9fcc1784be44563af513af5 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Fri, 10 Oct 2025 00:30:19 +0200 Subject: Lean 4.18 --- Day9.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Day9.lean') diff --git a/Day9.lean b/Day9.lean index d024823..8fc449c 100644 --- a/Day9.lean +++ b/Day9.lean @@ -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)) -- cgit v1.2.3