From 7f4d5412725cd4a7b93d72bfbd6f7b77ff38661f Mon Sep 17 00:00:00 2001 From: Eric Paul Date: Mon, 12 Jan 2026 19:42:57 -0800 Subject: [PATCH] chore: remove unused variable in FileMap.ofString --- src/Lean/Data/Position.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Lean/Data/Position.lean b/src/Lean/Data/Position.lean index 439e34b86fa8..f5eae212ed37 100644 --- a/src/Lean/Data/Position.lean +++ b/src/Lean/Data/Position.lean @@ -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