Documentation

Lean.Data.Position

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 = [anonymous]

instance Lean.instReprPosition:

Repr Lean.Position

Equations

Lean.instReprPosition = { reprPrec := [anonymous] }

def Lean.Position.lt:

Lean.Position → Lean.Position → Bool

Equations

Lean.Position.lt _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { line := l₁, column := c₁ }, { line := l₂, column := c₂ } => decide ((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

Instances

Lean.MonadLog.toMonadFileMap

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

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

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 (pos : String.Pos) (str : String) (ps : Array String.Pos) (lines : Array Nat) (b : Nat) (e : Nat) :

def String.toFileMap (s : String) :

Equations

String.toFileMap s = Lean.FileMap.ofString s