diff options
| author | Andreas Grois <andi@grois.info> | 2025-10-10 00:30:19 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2025-10-10 00:30:19 +0200 |
| commit | 2a9261d1ba962deff9fcc1784be44563af513af5 (patch) | |
| tree | e6c805e970924027723a159aa751e9aa0269ce7b /Day13.lean | |
| parent | 671ccf18e506398fd8eb65ebac92ec6d2fd03ccd (diff) | |
Lean 4.18
Diffstat (limited to 'Day13.lean')
| -rw-r--r-- | Day13.lean | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -51,7 +51,7 @@ match parse input with <;> simp only [Bool.false_eq_true, ↓reduceIte, gt_iff_lt] rw[←List.mapM'_eq_mapM] unfold List.mapM' - have h₂ : (input.toSubstring.splitOn "\n\n") ≠ [] := List.isEmpty_eq_false.mp h₁ + have h₂ : (input.toSubstring.splitOn "\n\n") ≠ [] := List.isEmpty_eq_false_iff.mp h₁ cases h₃ : input.toSubstring.splitOn "\n\n" case false.nil => contradiction case false.cons b bs => |