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

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

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

Equations

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

structure Lean.FileMap : Type

Content of a file together with precalculated positions of newlines.

• source : String

  The content of the file.

• positions : Array String.Pos

  The positions of newline characters. The first entry is always 0 and the last always the index of the last character. In particular, if the last character is a newline, that index will appear twice.

• lines : Array Nat

  The line numbers associated with the positions. Has the same length as positions and is always of the form #[1, 2, …, n-1, n-1].

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 Lean.FileMap.ofPosition (text : Lean.FileMap) (pos : Lean.Position) : String.Pos

Convert a Lean.Position to a String.Pos.

Equations

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

def Lean.FileMap.lineStart (map : Lean.FileMap) (line : Nat) : String.Pos

Returns the position of the start of (1-based) line line. This gives the stame result as map.ofPosition ⟨line, 0⟩, but is more efficient.

Equations

• Lean.FileMap.lineStart map line = if h : line - 1 < Array.size map.positions then Array.get map.positions { val := line - 1, isLt := h } else Option.getD (Array.back? map.positions) 0

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

Equations

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