From 2dfde4637f87c07593f5184a04e32a08a51dee3a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 12 Aug 2021 05:37:13 -0700
Subject: [PATCH] fix: index out of bounds

---
 src/Lean/Data/Position.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Lean/Data/Position.lean b/src/Lean/Data/Position.lean
index 2d235f945c..3e1a0106e8 100644
--- a/src/Lean/Data/Position.lean
+++ b/src/Lean/Data/Position.lean
@@ -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.