Documentation

Lean.Data.Position

structure Lean.Position :

line : Nat
column : Nat

Instances For

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✝ }

instance Lean.instToJsonPosition :

Lean.ToJson Lean.Position

Equations

Lean.instToJsonPosition = { toJson := Lean.toJsonPosition✝ }

instance Lean.instFromJsonPosition :

Lean.FromJson Lean.Position

Equations

Lean.instFromJsonPosition = { fromJson? := Lean.fromJsonPosition✝ }

def Lean.Position.lt :

Lean.Position → Lean.Position → Bool

Equations

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

instance Lean.Position.instToFormat :

Lean.ToFormat Lean.Position

Equations

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

instance Lean.Position.instToString :

ToString Lean.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 :

Lean.ToExpr Lean.Position

Equations

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

structure Lean.FileMap :

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.

Instances For

Lean.instInhabitedFileMap

instance Lean.instInhabitedFileMap :

Inhabited Lean.FileMap

Equations

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

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

getFileMap : m Lean.FileMap

Instances

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

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

Equations

fmap.getLastLine = fmap.positions.size - 1

def Lean.FileMap.getLine (fmap : Lean.FileMap) (x : 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) :

Equations

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

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

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

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) :

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

def Lean.FileMap.ofPosition (text : Lean.FileMap) (pos : Lean.Position) :

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) :

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.get ⟨line - 1, h⟩ else map.positions.back?.getD 0

def String.toFileMap (s : String) :

Equations

s.toFileMap = Lean.FileMap.ofString s