fix: index out of bounds

This commit is contained in:
Leonardo de Moura 2021-08-12 05:37:13 -07:00
parent accf198a88
commit 2dfde4637f

View file

@ -63,6 +63,8 @@ partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
else if pos > posM then loop m e
else loop b m
loop 0 (ps.size -1)
else if lines.isEmpty then
⟨0, 0⟩
else
-- Some systems like the delaborator use synthetic positions without an input file,
-- which would violate `toPositionAux`'s invariant.