structure Lean.Position : Type

• line : Nat
• column : Nat

instance Lean.instInhabitedPosition : Inhabited Lean.Position

Equations

• Lean.instInhabitedPosition = { default := { line := default, column := default } }

instance Lean.instDecidableEqPosition : DecidableEq Lean.Position

Equations

• Lean.instDecidableEqPosition = Lean.decEqPosition✝

instance Lean.instReprPosition : Repr Lean.Position

Equations

• Lean.instReprPosition = { reprPrec := Lean.reprPosition✝ }

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

Equations

• Lean.Position.lt x x = match x, x with | { line := l₁, column := c₁ }, { line := l₂, column := c₂ } => decide (Prod.lexLt (l₁, c₁) (l₂, c₂))

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

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Position.instToStringPosition : ToString Lean.Position

Equations

• Lean.Position.instToStringPosition = { toString := fun x => match x with | { line := l, column := c } => "⟨" ++ toString l ++ ", " ++ toString c ++ "⟩" }

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

Equations

• Lean.Position.instToExprPosition = { toExpr := fun p => Lean.mkAppN (Lean.mkConst `Lean.Position.mk) #[Lean.toExpr p.line, Lean.toExpr p.column], toTypeExpr := Lean.mkConst `Lean.Position }

structure Lean.FileMap : Type

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

instance Lean.instInhabitedFileMap : Inhabited Lean.FileMap

Equations

• Lean.instInhabitedFileMap = { default := { source := default, positions := default, lines := default } }

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

• getFileMap : m Lean.FileMap

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

Equations

• Lean.FileMap.ofString s = Lean.FileMap.ofString.loop s 0 1 #[0] #[1]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• String.toFileMap s = Lean.FileMap.ofString s