Get started

Author: TwoFX

src/Init/Core.lean

@@ -1605,7 +1605,7 @@ gen_injective_theorems% PSigma
 gen_injective_theorems% PSum
 gen_injective_theorems% Sigma
 gen_injective_theorems% String
-gen_injective_theorems% String.Pos
+gen_injective_theorems% String.Pos.Raw
 gen_injective_theorems% Substring
 gen_injective_theorems% Subtype
 gen_injective_theorems% Sum

src/Init/Data/Repr.lean

@@ -411,7 +411,7 @@ def String.quote (s : String) : String :=
 instance : Repr String where
   reprPrec s _ := s.quote
 
-instance : Repr String.Pos where
+instance : Repr String.Pos.Raw where
   reprPrec p _ := "{ byteIdx := " ++ repr p.byteIdx ++ " }"
 
 instance : Repr Substring where

src/Init/Data/String/Basic.lean

@@ -14,7 +14,10 @@ public section
 
 namespace String
 
-instance : OfNat String.Pos (nat_lit 0) where
+@[deprecated Pos.Raw (since := "2025-09-30")]
+abbrev Pos := Pos.Raw
+
+instance : OfNat String.Pos.Raw (nat_lit 0) where
   ofNat := {}
 
 instance : Inhabited String where
@@ -57,13 +60,13 @@ end String
 namespace String.Internal
 
 @[extern "lean_string_posof"]
-opaque posOf (s : String) (c : Char) : Pos
+opaque posOf (s : String) (c : Char) : Pos.Raw
 
 @[extern "lean_string_offsetofpos"]
-opaque offsetOfPos (s : String) (pos : Pos) : Nat
+opaque offsetOfPos (s : String) (pos : Pos.Raw) : Nat
 
 @[extern "lean_string_utf8_extract"]
-opaque extract : (@& String) → (@& Pos) → (@& Pos) → String
+opaque extract : (@& String) → (@& Pos.Raw) → (@& Pos.Raw) → String
 
 @[extern "lean_string_length"]
 opaque length : (@& String) → Nat
@@ -75,7 +78,7 @@ opaque pushn (s : String) (c : Char) (n : Nat) : String
 opaque append : String → (@& String) → String
 
 @[extern "lean_string_utf8_next"]
-opaque next (s : @& String) (p : @& Pos) : Pos
+opaque next (s : @& String) (p : @& Pos.Raw) : Pos.Raw
 
 @[extern "lean_string_isempty"]
 opaque isEmpty (s : String) : Bool
@@ -93,16 +96,16 @@ opaque any (s : String) (p : Char → Bool) : Bool
 opaque contains (s : String) (c : Char) : Bool
 
 @[extern "lean_string_utf8_get"]
-opaque get (s : @& String) (p : @& Pos) : Char
+opaque get (s : @& String) (p : @& Pos.Raw) : Char
 
 @[extern "lean_string_capitalize"]
 opaque capitalize (s : String) : String
 
 @[extern "lean_string_utf8_at_end"]
-opaque atEnd : (@& String) → (@& Pos) → Bool
+opaque atEnd : (@& String) → (@& Pos.Raw) → Bool
 
 @[extern "lean_string_nextwhile"]
-opaque nextWhile (s : String) (p : Char → Bool) (i : String.Pos) : String.Pos
+opaque nextWhile (s : String) (p : Char → Bool) (i : String.Pos.Raw) : String.Pos.Raw
 
 @[extern "lean_string_trim"]
 opaque trim (s : String) : String
@@ -160,7 +163,7 @@ opaque front (s : Substring) : Char
 opaque takeWhile : Substring → (Char → Bool) → Substring
 
 @[extern "lean_substring_extract"]
-opaque extract : Substring → String.Pos → String.Pos → Substring
+opaque extract : Substring → String.Pos.Raw → String.Pos.Raw → Substring
 
 @[extern "lean_substring_all"]
 opaque all (s : Substring) (p : Char → Bool) : Bool
@@ -172,22 +175,22 @@ opaque beq (ss1 ss2 : Substring) : Bool
 opaque isEmpty (ss : Substring) : Bool
 
 @[extern "lean_substring_get"]
-opaque get : Substring → String.Pos → Char
+opaque get : Substring → String.Pos.Raw → Char
 
 @[extern "lean_substring_prev"]
-opaque prev : Substring → String.Pos → String.Pos
+opaque prev : Substring → String.Pos.Raw → String.Pos.Raw
 
 end Substring.Internal
 
-namespace String.Pos.Internal
+namespace String.Pos.Raw.Internal
 
 @[extern "lean_string_pos_sub"]
-opaque sub : String.Pos → String.Pos → String.Pos
+opaque sub : String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
 
 @[extern "lean_string_pos_min"]
-opaque min (p₁ p₂ : Pos) : Pos
+opaque min (p₁ p₂ : Pos.Raw) : Pos.Raw
 
-end String.Pos.Internal
+end String.Pos.Raw.Internal
 
 namespace Char
 

src/Init/Data/String/Bootstrap.lean

@@ -1315,7 +1315,7 @@ public theorem isUtf8FirstByte_getElem_zero_utf8EncodeChar {c : Char} :
   simp
 
 @[expose]
-public def utf8ByteSize (c : UInt8) (_h : c.IsUtf8FirstByte) : String.Pos :=
+public def utf8ByteSize (c : UInt8) (_h : c.IsUtf8FirstByte) : String.Pos.Raw :=
   if c &&& 0x80 = 0 then
     ⟨1⟩
   else if c &&& 0xe0 = 0xc0 then
@@ -1325,7 +1325,7 @@ public def utf8ByteSize (c : UInt8) (_h : c.IsUtf8FirstByte) : String.Pos :=
   else
     ⟨4⟩
 
-def _root_.ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize : FirstByte → String.Pos
+def _root_.ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize : FirstByte → String.Pos.Raw
   | .invalid => ⟨0⟩
   | .done => ⟨1⟩
   | .oneMore => ⟨2⟩

src/Init/Data/String/Decode.lean

@@ -86,7 +86,7 @@ instance : ToString Unit :=
 instance : ToString Nat :=
   ⟨fun n => Nat.repr n⟩
 
-instance : ToString String.Pos :=
+instance : ToString String.Pos.Raw :=
   ⟨fun p => Nat.repr p.byteIdx⟩
 
 instance : ToString Int where

src/Init/Data/ToString/Basic.lean

@@ -560,7 +560,7 @@ Finds the tail position of the trailing whitespace of the first `SourceInfo` fro
 If no `SourceInfo` can be found or the first `SourceInfo` from the back of `stx` contains
 no trailing whitespace and lacks a tail position, the result is `none`.
 -/
-def getTrailingTailPos? (stx : Syntax) (canonicalOnly := false) : Option String.Pos :=
+def getTrailingTailPos? (stx : Syntax) (canonicalOnly := false) : Option String.Pos.Raw :=
   stx.getTailInfo.getTrailingTailPos? canonicalOnly
 
 /--
@@ -818,7 +818,7 @@ def mkNameLit (val : String) (info := SourceInfo.none) : NameLit :=
    in binary, octal, decimal and hexadecimal format. `isNatLit` implements a "decoder"
    for Syntax objects representing these numerals. -/
 
-private partial def decodeBinLitAux (s : String) (i : String.Pos) (val : Nat) : Option Nat :=
+private partial def decodeBinLitAux (s : String) (i : String.Pos.Raw) (val : Nat) : Option Nat :=
   if String.Internal.atEnd s i then some val
   else
     let c := String.Internal.get s i
@@ -827,31 +827,31 @@ private partial def decodeBinLitAux (s : String) (i : String.Pos) (val : Nat) :
     else if c == '_' then decodeBinLitAux s (String.Internal.next s i) val
     else none
 
-private partial def decodeOctalLitAux (s : String) (i : String.Pos) (val : Nat) : Option Nat :=
+private partial def decodeOctalLitAux (s : String) (i : String.Pos.Raw) (val : Nat) : Option Nat :=
   if String.Internal.atEnd s i then some val
   else
     let c := String.Internal.get s i
     if '0' ≤ c && c ≤ '7' then decodeOctalLitAux s (String.Internal.next s i) (8*val + c.toNat - '0'.toNat)
     else if c == '_' then decodeOctalLitAux s (String.Internal.next s i) val
     else none
 
-private def decodeHexDigit (s : String) (i : String.Pos) : Option (Nat × String.Pos) :=
+private def decodeHexDigit (s : String) (i : String.Pos.Raw) : Option (Nat × String.Pos.Raw) :=
   let c := String.Internal.get s i
   let i := String.Internal.next s i
   if '0' ≤ c && c ≤ '9' then some (c.toNat - '0'.toNat, i)
   else if 'a' ≤ c && c ≤ 'f' then some (10 + c.toNat - 'a'.toNat, i)
   else if 'A' ≤ c && c ≤ 'F' then some (10 + c.toNat - 'A'.toNat, i)
   else none
 
-private partial def decodeHexLitAux (s : String) (i : String.Pos) (val : Nat) : Option Nat :=
+private partial def decodeHexLitAux (s : String) (i : String.Pos.Raw) (val : Nat) : Option Nat :=
   if String.Internal.atEnd s i then some val
   else match decodeHexDigit s i with
     | some (d, i) => decodeHexLitAux s i (16*val + d)
     | none        =>
       if String.Internal.get s i == '_' then decodeHexLitAux s (String.Internal.next s i) val
       else none
 
-private partial def decodeDecimalLitAux (s : String) (i : String.Pos) (val : Nat) : Option Nat :=
+private partial def decodeDecimalLitAux (s : String) (i : String.Pos.Raw) (val : Nat) : Option Nat :=
   if String.Internal.atEnd s i then some val
   else
     let c := String.Internal.get s i
@@ -911,7 +911,7 @@ partial def decodeScientificLitVal? (s : String) : Option (Nat × Bool × Nat) :
       decode 0 0
     else none
 where
-  decodeAfterExp (i : String.Pos) (val : Nat) (e : Nat) (sign : Bool) (exp : Nat) : Option (Nat × Bool × Nat) :=
+  decodeAfterExp (i : String.Pos.Raw) (val : Nat) (e : Nat) (sign : Bool) (exp : Nat) : Option (Nat × Bool × Nat) :=
     if String.Internal.atEnd s i then
       if sign then
         some (val, sign, exp + e)
@@ -928,7 +928,7 @@ where
       else
         none
 
-  decodeExp (i : String.Pos) (val : Nat) (e : Nat) : Option (Nat × Bool × Nat) :=
+  decodeExp (i : String.Pos.Raw) (val : Nat) (e : Nat) : Option (Nat × Bool × Nat) :=
     if String.Internal.atEnd s i then none else
     let c := String.Internal.get s i
     if c == '-' then
@@ -938,7 +938,7 @@ where
     else
        decodeAfterExp i val e false 0
 
-  decodeAfterDot (i : String.Pos) (val : Nat) (e : Nat) : Option (Nat × Bool × Nat) :=
+  decodeAfterDot (i : String.Pos.Raw) (val : Nat) (e : Nat) : Option (Nat × Bool × Nat) :=
     if String.Internal.atEnd s i then
       some (val, true, e)
     else
@@ -952,7 +952,7 @@ where
       else
         none
 
-  decode (i : String.Pos) (val : Nat) : Option (Nat × Bool × Nat) :=
+  decode (i : String.Pos.Raw) (val : Nat) : Option (Nat × Bool × Nat) :=
     if String.Internal.atEnd s i then
       none
     else
@@ -983,7 +983,7 @@ def toNat (stx : Syntax) : Nat :=
   | some val => val
   | none     => 0
 
-def decodeQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos) := do
+def decodeQuotedChar (s : String) (i : String.Pos.Raw) : Option (Char × String.Pos.Raw) := do
   let c := String.Internal.get s i
   let i := String.Internal.next s i
   if c == '\\' then pure ('\\', i)
@@ -1011,11 +1011,11 @@ Note that this function matches `"\" whitespace+` rather than
 the more restrictive `"\" newline whitespace*` since this simplifies the implementation.
 Justification: this does not overlap with any other sequences beginning with `\`.
 -/
-def decodeStringGap (s : String) (i : String.Pos) : Option String.Pos := do
+def decodeStringGap (s : String) (i : String.Pos.Raw) : Option String.Pos.Raw := do
   guard <| (String.Internal.get s i).isWhitespace
   some <| String.Internal.nextWhile s Char.isWhitespace (String.Internal.next s i)
 
-partial def decodeStrLitAux (s : String) (i : String.Pos) (acc : String) : Option String := do
+partial def decodeStrLitAux (s : String) (i : String.Pos.Raw) (acc : String) : Option String := do
   let c := String.Internal.get s i
   let i := String.Internal.next s i
   if c == '\"' then
@@ -1038,7 +1038,7 @@ The position `i` should start at `1`, which is the character after the leading `
 The algorithm is simple: we are given `r##...#"...string..."##...#` with zero or more `#`s.
 By counting the number of leading `#`'s, we can extract the `...string...`.
 -/
-partial def decodeRawStrLitAux (s : String) (i : String.Pos) (num : Nat) : String :=
+partial def decodeRawStrLitAux (s : String) (i : String.Pos.Raw) (num : Nat) : String :=
   let c := String.Internal.get s i
   let i := String.Internal.next s i
   if c == '#' then
@@ -1097,7 +1097,7 @@ private partial def splitNameLitAux (ss : Substring) (acc : List Substring) : Li
     let curr := Substring.Internal.front ss
     if isIdBeginEscape curr then
       let escapedPart := Substring.Internal.takeWhile ss (!isIdEndEscape ·)
-      let escapedPart := { escapedPart with stopPos := String.Pos.Internal.min ss.stopPos (String.Internal.next escapedPart.str escapedPart.stopPos) }
+      let escapedPart := { escapedPart with stopPos := String.Pos.Raw.Internal.min ss.stopPos (String.Internal.next escapedPart.str escapedPart.stopPos) }
       if !isIdEndEscape (Substring.Internal.get escapedPart <| Substring.Internal.prev escapedPart ⟨escapedPart.bsize⟩) then []
       else splitRest (Substring.Internal.extract ss ⟨escapedPart.bsize⟩ ⟨ss.bsize⟩) (escapedPart :: acc)
     else if isIdFirst curr then
@@ -1462,7 +1462,7 @@ end Lean.Syntax
 
 namespace Lean.Syntax
 
-private def decodeInterpStrQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos) := do
+private def decodeInterpStrQuotedChar (s : String) (i : String.Pos.Raw) : Option (Char × String.Pos.Raw) := do
   match decodeQuotedChar s i with
   | some r => some r
   | none   =>
@@ -1472,7 +1472,7 @@ private def decodeInterpStrQuotedChar (s : String) (i : String.Pos) : Option (Ch
     else none
 
 private partial def decodeInterpStrLit (s : String) : Option String :=
-  let rec loop (i : String.Pos) (acc : String) : Option String :=
+  let rec loop (i : String.Pos.Raw) (acc : String) : Option String :=
     let c := String.Internal.get s i
     let i := String.Internal.next s i
     if c == '\"' || c == '{' then
@@ -1533,7 +1533,7 @@ def expandInterpolatedStr (interpStr : TSyntax interpolatedStrKind) (type : Term
 
 def getDocString (stx : TSyntax `Lean.Parser.Command.docComment) : String :=
   match stx.raw[1] with
-  | Syntax.atom _ val => String.Internal.extract val 0 (String.Pos.Internal.sub val.endPos ⟨2⟩)
+  | Syntax.atom _ val => String.Internal.extract val 0 (String.Pos.Raw.Internal.sub val.endPos ⟨2⟩)
   | _                 => ""
 
 end TSyntax