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

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

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 :

source : String
positions : Array String.Pos
lines : Array Nat

Instances For

instance Lean.instInhabitedFileMap :

Inhabited Lean.FileMap

Equations

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

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

getFileMap : m Lean.FileMap

Instances

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