Equations
- Lean.instInhabitedPosition = { default := { line := default, column := default } }
Equations
- Lean.instReprPosition = { reprPrec := Lean.reprPosition✝ }
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₂))
Instances For
Equations
- One or more equations did not get rendered due to their size.
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 }
- source : String
- positions : Array String.Pos
Instances For
Equations
- Lean.instInhabitedFileMap = { default := { source := default, positions := default, lines := default } }
Equations
- Lean.FileMap.ofString s = Lean.FileMap.ofString.loop s 0 1 #[0] #[1]
Instances For
partial def
Lean.FileMap.ofString.loop
(s : String)
(i : String.Pos)
(line : Nat)
(ps : Array String.Pos)
(lines : Array Nat)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
: