max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove unused variable in FileMap.ofString (#11986)

Browse source 
Removes the unused `line` variable in `FileMap.ofString`
This commit is contained in:
Eric Paul 2026-02-16 16:49:16 -06:00 • committed by GitHub
parent 0a19fe7d98
commit 76c95a085b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Data/Position.lean
View file

@ -62,14 +62,14 @@ def getLine (fmap : FileMap) (x : Nat) : Nat :=
min (x + 1) fmap.getLastLine
partial def ofString (s : String) : FileMap :=
let rec loop (i : String.Pos.Raw) (line : Nat) (ps : Array String.Pos.Raw) : FileMap :=
let rec loop (i : String.Pos.Raw) (ps : Array String.Pos.Raw) : FileMap :=
if i.atEnd s then { source := s, positions := ps.push i }
else
let c := i.get s
let i := i.next s
if c == '\n' then loop i (line+1) (ps.push i)
else loop i line ps
loop 0 1 #[0]
if c == '\n' then loop i (ps.push i)
else loop i ps
loop 0 #[0]
partial def toPosition (fmap : FileMap) (pos : String.Pos.Raw) : Position :=
match fmap with