@[reducible, inline]

abbrev Lean.Lsp.DocumentUri : Type

Equations

• Lean.Lsp.DocumentUri = String

structure Lean.Lsp.Position : Type

We adopt the convention that zero-based UTF-16 positions as sent by LSP clients are represented by Lsp.Position while internally we mostly use String.Pos UTF-8 offsets. For diagnostics, one-based Lean.Positions are used internally. character is accepted liberally: actual character := min(line length, character)

• line : Nat
• character : Nat

instance Lean.Lsp.instInhabitedPosition : Inhabited Position

Equations

• Lean.Lsp.instInhabitedPosition = { default := { line := default, character := default } }

instance Lean.Lsp.instBEqPosition : BEq Position

Equations

• Lean.Lsp.instBEqPosition = { beq := Lean.Lsp.beqPosition✝ }

instance Lean.Lsp.instOrdPosition : Ord Position

Equations

• Lean.Lsp.instOrdPosition = { compare := Lean.Lsp.ordPosition✝ }

instance Lean.Lsp.instHashablePosition : Hashable Position

Equations

• Lean.Lsp.instHashablePosition = { hash := Lean.Lsp.hashPosition✝ }

instance Lean.Lsp.instToJsonPosition : ToJson Position

Equations

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

instance Lean.Lsp.instFromJsonPosition : FromJson Position

Equations

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

instance Lean.Lsp.instReprPosition : Repr Position

Equations

• Lean.Lsp.instReprPosition = { reprPrec := Lean.Lsp.reprPosition✝ }

instance Lean.Lsp.instToStringPosition : ToString Position

Equations

• Lean.Lsp.instToStringPosition = { toString := fun (p : Lean.Lsp.Position) => "(" ++ toString p.line ++ ", " ++ toString p.character ++ ")" }

instance Lean.Lsp.instLTPosition : LT Position

Equations

• Lean.Lsp.instLTPosition = ltOfOrd

instance Lean.Lsp.instLEPosition : LE Position

Equations

• Lean.Lsp.instLEPosition = leOfOrd

structure Lean.Lsp.Range : Type

• start : Position
• end : Position

instance Lean.Lsp.instInhabitedRange : Inhabited Range

Equations

• Lean.Lsp.instInhabitedRange = { default := { start := default, «end» := default } }

instance Lean.Lsp.instBEqRange : BEq Range

Equations

• Lean.Lsp.instBEqRange = { beq := Lean.Lsp.beqRange✝ }

instance Lean.Lsp.instHashableRange : Hashable Range

Equations

• Lean.Lsp.instHashableRange = { hash := Lean.Lsp.hashRange✝ }

instance Lean.Lsp.instToJsonRange : ToJson Range

Equations

• Lean.Lsp.instToJsonRange = { toJson := Lean.Lsp.toJsonRange✝ }

instance Lean.Lsp.instFromJsonRange : FromJson Range

Equations

• Lean.Lsp.instFromJsonRange = { fromJson? := Lean.Lsp.fromJsonRange✝ }

instance Lean.Lsp.instOrdRange : Ord Range

Equations

• Lean.Lsp.instOrdRange = { compare := Lean.Lsp.ordRange✝ }

instance Lean.Lsp.instReprRange : Repr Range

Equations

• Lean.Lsp.instReprRange = { reprPrec := Lean.Lsp.reprRange✝ }

instance Lean.Lsp.instLTRange : LT Range

Equations

• Lean.Lsp.instLTRange = ltOfOrd

instance Lean.Lsp.instLERange : LE Range

Equations

• Lean.Lsp.instLERange = leOfOrd