summaryrefslogtreecommitdiff
path: root/Day9.lean
diff options
context:
space:
mode:
authorAndreas Grois <andi@grois.info>2025-10-10 00:30:19 +0200
committerAndreas Grois <andi@grois.info>2025-10-10 00:30:19 +0200
commit2a9261d1ba962deff9fcc1784be44563af513af5 (patch)
treee6c805e970924027723a159aa751e9aa0269ce7b /Day9.lean
parent671ccf18e506398fd8eb65ebac92ec6d2fd03ccd (diff)
Lean 4.18
Diffstat (limited to 'Day9.lean')
-rw-r--r--Day9.lean4
1 files changed, 2 insertions, 2 deletions
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))