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/Substring.lean | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'Common/Substring.lean')

diff --git a/Common/Substring.lean b/Common/Substring.lean
index f51b088..d38c97d 100644
--- a/Common/Substring.lean
+++ b/Common/Substring.lean
@@ -2,7 +2,7 @@ import Common.Nat
 
 namespace Substring
 
-theorem nextn_ge (s : Substring) (n : Nat) (p : String.Pos) : s.nextn n p ≥ p := by
+theorem nextn_ge (s : Substring) (n : Nat) (p : String.Pos.Raw) : s.nextn n p ≥ p := by
   unfold Substring.nextn
   cases n
   case zero => simp
@@ -10,16 +10,16 @@ theorem nextn_ge (s : Substring) (n : Nat) (p : String.Pos) : s.nextn n p ≥ p
     simp
     unfold Substring.next
     simp
-    if h₁ :s.startPos + p = s.stopPos then
+    if h₁ : p.offsetBy s.startPos = s.stopPos then
       simp[h₁]
       exact nextn_ge s nn p
     else
       simp[h₁]
-      have h₂ : { byteIdx := (s.str.next (s.startPos + p)).byteIdx - s.startPos.byteIdx  : String.Pos} ≤ s.nextn nn { byteIdx := (s.str.next (s.startPos + p)).byteIdx - s.startPos.byteIdx } :=
+      have h₂ : { byteIdx := (String.Pos.Raw.next s.str (p.offsetBy s.startPos)).byteIdx - s.startPos.byteIdx  : String.Pos.Raw} ≤ s.nextn nn { byteIdx := (String.Pos.Raw.next s.str (p.offsetBy s.startPos)).byteIdx - s.startPos.byteIdx } :=
         nextn_ge _ nn _
-      simp[String.Pos.le_iff]
+      simp[String.Pos.Raw.le_iff]
       apply Nat.le_trans  _ h₂
-      unfold String.next
+      unfold String.Pos.Raw.next
       simp[Char.utf8Size]
       split <;> try split <;> try split
       all_goals
@@ -28,15 +28,15 @@ theorem nextn_ge (s : Substring) (n : Nat) (p : String.Pos) : s.nextn n p ≥ p
 theorem drop_bsize_dec (s : Substring) (n : Nat) (h₁ : ¬s.isEmpty) (h₂ : n ≠ 0) : (s.drop n).bsize < s.bsize := by
   cases n ; contradiction
   case succ nn =>
-    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]
     simp only [Substring.isEmpty, Substring.bsize, Nat.sub_eq, beq_iff_eq] at h₁
-    if h₃ : (s.startPos.byteIdx + ({ str := s.str, startPos := s.startPos, stopPos := s.stopPos : Substring}.nextn nn (if s.startPos + 0 = s.stopPos then 0 else { byteIdx := (s.str.next (s.startPos + 0)).byteIdx - s.startPos.byteIdx })).byteIdx) ≤ s.stopPos.byteIdx then
+    if h₃ : (s.startPos.byteIdx + ({ str := s.str, startPos := s.startPos, stopPos := s.stopPos : Substring}.nextn nn (if String.Pos.Raw.offsetBy 0 s.startPos = s.stopPos then 0 else {byteIdx := (String.Pos.Raw.next s.str (String.Pos.Raw.offsetBy 0 s.startPos)).byteIdx - s.startPos.byteIdx })).byteIdx) ≤ s.stopPos.byteIdx then
       apply Nat.sub_lt_of_gt; exact h₃
       split
       case h₂.isTrue hx =>
         simp[←hx] at h₁
       case h₂.isFalse h₄ =>
-        unfold String.next
+        unfold String.Pos.Raw.next
         simp
         unfold Char.utf8Size
         simp
@@ -45,7 +45,7 @@ theorem drop_bsize_dec (s : Substring) (n : Nat) (h₁ : ¬s.isEmpty) (h₂ : n
         all_goals
           simp
     else
-      have h₄ : s.stopPos.byteIdx - (s.startPos.byteIdx + ({ str := s.str, startPos := s.startPos, stopPos := s.stopPos : Substring}.nextn nn (if s.startPos + 0 = s.stopPos then 0 else { byteIdx := (s.str.next (s.startPos + 0)).byteIdx - s.startPos.byteIdx })).byteIdx)  = 0 := by
+      have h₄ : s.stopPos.byteIdx - (s.startPos.byteIdx + ({ str := s.str, startPos := s.startPos, stopPos := s.stopPos : Substring }.nextn nn (if String.Pos.Raw.offsetBy 0 s.startPos = s.stopPos then 0 else {byteIdx := (String.Pos.Raw.next s.str (String.Pos.Raw.offsetBy 0 s.startPos)).byteIdx - s.startPos.byteIdx })).byteIdx) = 0 := by
         omega
       rw[h₄]
       omega
-- 
cgit v1.2.3

