diff options
| author | Andreas Grois <andi@grois.info> | 2025-11-16 21:08:35 +0100 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2025-11-16 21:08:35 +0100 |
| commit | 3a9ff92902df508074daa3017d1a71dae7e85248 (patch) | |
| tree | 3ddc5f4dc040ce2aa762c642569ff274f36049e7 /Common/Parsing.lean | |
| parent | 75628f029abfd9829a1259a6e1dd7758d548c13f (diff) | |
Lean 4.25feature/day17
Diffstat (limited to 'Common/Parsing.lean')
| -rw-r--r-- | Common/Parsing.lean | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Common/Parsing.lean b/Common/Parsing.lean index ff54ef0..4fb6767 100644 --- a/Common/Parsing.lean +++ b/Common/Parsing.lean @@ -134,12 +134,12 @@ protected def RectangularGrid.parseSingleLine (parseCharacter : Char → Except termination_by remainingLine.bsize decreasing_by simp only [Substring.isEmpty, Substring.bsize, Nat.sub_eq, beq_iff_eq] at _h₁ - simp only [Substring.drop, Substring.bsize, Substring.nextn, Substring.next, String.Pos.add_byteIdx, Nat.sub_eq] + simp only [Substring.drop, Substring.bsize, Substring.nextn, Substring.next, String.Pos.Raw.byteIdx_offsetBy, Nat.sub_eq] split case isTrue h₂ => - simp[←(congrArg String.Pos.byteIdx h₂)] at _h₁ + simp[←(congrArg String.Pos.Raw.byteIdx h₂)] at _h₁ case isFalse h₂ => - simp[String.next, Char.utf8Size] + simp[String.Pos.Raw.next, Char.utf8Size] split <;> try split <;> try split all_goals omega |