fix: FileMap out of bounds

This commit is contained in:
Sebastian Ullrich 2021-03-13 17:51:37 +01:00 committed by Leonardo de Moura
parent 12aa5cc461
commit 048d592fe8

View file

@ -60,8 +60,9 @@ partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
loop 0 (ps.size -1)
else
-- Some systems like the delaborator use synthetic positions without an input file,
-- which would violate `toPositionAux`'s invariant
⟨1, pos⟩
-- which would violate `toPositionAux`'s invariant.
-- Can also happen with EOF errors, which are not strictly inside the file.
⟨lines.back, pos - ps.back⟩
end FileMap
end Lean