structure Lean.Position : Type

• line : Nat
• column : Nat

instance Lean.instInhabitedPosition : Inhabited Lean.Position

instance Lean.instDecidableEqPosition : DecidableEq Lean.Position

instance Lean.instReprPosition : Repr Lean.Position

def Lean.Position.lt : Lean.Position → Lean.Position → Bool

instance Lean.Position.instToFormatPosition : Lean.ToFormat Lean.Position

instance Lean.Position.instToStringPosition : ToString Lean.Position

instance Lean.Position.instToExprPosition : Lean.ToExpr Lean.Position

structure Lean.FileMap : Type

• source : String
• positions : Array String.Pos
• lines : Array Nat

instance Lean.instInhabitedFileMap : Inhabited Lean.FileMap

class Lean.MonadFileMap (m : Type → Type) : Type

• getFileMap : m Lean.FileMap

def Lean.FileMap.ofString (s : String) : Lean.FileMap

partial def Lean.FileMap.ofString.loop (s : String) (i : String.Pos) (line : Nat) (ps : Array String.Pos) (lines : Array Nat) : Lean.FileMap

def Lean.FileMap.toPosition (fmap : Lean.FileMap) (pos : String.Pos) : Lean.Position

partial def Lean.FileMap.toPosition.toColumn (pos : String.Pos) (str : String) (i : String.Pos) (c : Nat) : Nat

partial def Lean.FileMap.toPosition.loop (pos : String.Pos) (str : String) (ps : Array String.Pos) (lines : Array Nat) (b : Nat) (e : Nat) : Lean.Position

def String.toFileMap (s : String) : Lean.FileMap