diff options
| author | Andreas Grois <andi@grois.info> | 2024-07-12 22:01:57 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-07-12 22:01:57 +0200 |
| commit | f7ac27f54a76582354964bae21ee03937c108187 (patch) | |
| tree | a26faa679e820dfd932c614c8423902bd63c1400 /Day9.lean | |
| parent | 775f27f47861641561ea8fe4dc8b9ce1e48a47f9 (diff) | |
Squashed commit of the following:
commit 7aeefe2e761a4892ff2f438e00f3ec7e6d286c5c
Author: Andreas Grois <andi@grois.info>
Date: Fri Jul 12 21:59:44 2024 +0200
Finish Lean 4.9 update.
commit 8a5576ae983203035f6bf0c807b36f1b4d7b63a6
Author: Andreas Grois <andi@grois.info>
Date: Fri Jul 12 21:40:21 2024 +0200
Lean 4.9 upgrade, heap is where it was before...
commit db34881e21391c96a6a0b939552b0f6f77d05bd8
Author: Andreas Grois <andi@grois.info>
Date: Fri Jul 12 00:31:22 2024 +0200
Further Lean 4.9 compat...
commit 22444613d58c5bd1a3fcdad0cd6c8d3aee1f3214
Author: Andreas Grois <andi@grois.info>
Date: Thu Jul 11 22:15:11 2024 +0200
Further Lean 4.9 porting
commit a4ace32cbb02959f9625578b511c2486e0816367
Author: Andreas Grois <andi@grois.info>
Date: Wed Jul 10 23:18:29 2024 +0200
Continue porting to Lean 4.9
commit d0f411bcc42b5cb7c72c2ed65ae35875c72e95dd
Author: Andreas Grois <andi@grois.info>
Date: Wed Jul 10 23:10:34 2024 +0200
Continue port to Lean 4.9
commit 835ce644b97840048de0df40676ff6f3a8b99985
Author: Andreas Grois <andi@grois.info>
Date: Wed Jul 10 22:14:59 2024 +0200
Partial port to Lean 4.9. Not compiling yet.
Diffstat (limited to 'Day9.lean')
| -rw-r--r-- | Day9.lean | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -36,7 +36,7 @@ private def extrapolate : List Int → Int case cons b bs hb => rw[←differences_length_independent_arg] assumption a + extrapolate (differences (a :: as)) -termination_by extrapolate a => a.length +termination_by a => a.length def part1 : List (List Int) → Int := List.foldl Int.add 0 ∘ List.map (extrapolate ∘ List.reverse) |