structure Lean.Position : Type

• line : Nat
• column : Nat

instance Lean.instInhabitedPosition : Inhabited Position

instance Lean.instDecidableEqPosition : DecidableEq Position

instance Lean.instReprPosition : Repr Position

instance Lean.instToJsonPosition : ToJson Position

instance Lean.instFromJsonPosition : FromJson Position

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

instance Lean.Position.instToFormat : ToFormat Position

instance Lean.Position.instToString : ToString Position

instance Lean.Position.instToExpr : ToExpr Position

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

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.

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.

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

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

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

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

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

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

Convert a Lean.Position to a String.Pos.

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.

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