From 3a9ff92902df508074daa3017d1a71dae7e85248 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 16 Nov 2025 21:08:35 +0100
Subject: Lean 4.25

---
 Common/Parsing.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'Common/Parsing.lean')

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
 
-- 
cgit v1.2.3

