diff options
| author | Andreas Grois <andi@grois.info> | 2025-10-12 18:44:32 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2025-10-12 18:44:32 +0200 |
| commit | 6aaa70943202efaa1e6b4ff8b6b8b6b94a564040 (patch) | |
| tree | 171a1a1b459b82f016e756e8649767a2d1311160 /Day13.lean | |
| parent | 2a9261d1ba962deff9fcc1784be44563af513af5 (diff) | |
Lean 4.19
Diffstat (limited to 'Day13.lean')
| -rw-r--r-- | Day13.lean | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -62,7 +62,7 @@ match parse input with cases List.mapM' (Parsing.RectangularGrid.ofSubstring Day13.Tile.ofChar?) bs case error e => exact True.intro case ok ts => - have h₄ := List.length_cons t ts + have h₄ : (t :: ts).length = ts.length + 1 := List.length_cons unfold bind Monad.toBind Except.instMonad simp only [Except.bind, Except.map, h₄, Nat.zero_lt_succ] |