structure Lean.Position : Type

• line : Nat
• column : Nat

def Lean.instInhabitedPosition.default : Position

Equations

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

instance Lean.instInhabitedPosition : Inhabited Position

Equations

• Lean.instInhabitedPosition = { default := Lean.instInhabitedPosition.default }

instance Lean.instDecidableEqPosition : DecidableEq Position

Equations

• Lean.instDecidableEqPosition = Lean.instDecidableEqPosition.decEq

def Lean.instDecidableEqPosition.decEq (x✝ x✝¹ : Position) : Decidable (x✝ = x✝¹)

Equations

• Lean.instDecidableEqPosition.decEq { line := a, column := a_1 } { line := b, column := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance Lean.instReprPosition : Repr Position

Equations

• Lean.instReprPosition = { reprPrec := Lean.instReprPosition.repr }

def Lean.instReprPosition.repr : Position → Nat → Format

Equations

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

def Lean.instToJsonPosition.toJson : Position → Json

Equations

• Lean.instToJsonPosition.toJson x✝ = Lean.Json.mkObj [[("line", Lean.toJson x✝.line)], [("column", Lean.toJson x✝.column)]].flatten

instance Lean.instToJsonPosition : ToJson Position

Equations

• Lean.instToJsonPosition = { toJson := Lean.instToJsonPosition.toJson }

instance Lean.instFromJsonPosition : FromJson Position

Equations

• Lean.instFromJsonPosition = { fromJson? := Lean.instFromJsonPosition.fromJson }

def Lean.instFromJsonPosition.fromJson : Json → Except String Position

Equations

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

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

Equations

• { line := a, column := a_1 }.lt { line := b, column := b_1 } = decide ((a, a_1).lexLt (b, b_1))

instance Lean.Position.instToFormat : ToFormat Position

Equations

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

instance Lean.Position.instToString : ToString Position

Equations

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

instance Lean.Position.instToExpr : ToExpr 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.

instance Lean.instInhabitedFileMap : Inhabited FileMap

Equations

• Lean.instInhabitedFileMap = { default := Lean.instInhabitedFileMap.default }

def Lean.instInhabitedFileMap.default : FileMap

Equations

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

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

• getFileMap : m FileMap

def Lean.FileMap.getLastLine (fmap : FileMap) : Nat

The last line should always be positions.size - 1.

Equations

• fmap.getLastLine = fmap.positions.size - 1

def Lean.FileMap.getLine (fmap : FileMap) (x : Nat) : Nat

The line numbers associated with the positions of the FileMap. fmap.getLine i is the iᵗʰ entry of #[1, 2, …, n-1, n-1] where n is the size of positions.

Equations

• fmap.getLine x = min (x + 1) fmap.getLastLine

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

Equations

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

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

Equations

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

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

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

Equations

• map.lineStart line = if h : line - 1 < map.positions.size then map.positions[line - 1] else map.positions.back?.getD 0

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

Equations

• s.toFileMap = Lean.FileMap.ofString s