@[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

def Lean.Lsp.instInhabitedPosition.default : Position

Equations

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

instance Lean.Lsp.instInhabitedPosition : Inhabited Position

Equations

• Lean.Lsp.instInhabitedPosition = { default := Lean.Lsp.instInhabitedPosition.default }

def Lean.Lsp.instBEqPosition.beq : Position → Position → Bool

Equations

• Lean.Lsp.instBEqPosition.beq { line := a, character := a_1 } { line := b, character := b_1 } = (a == b && a_1 == b_1)
• Lean.Lsp.instBEqPosition.beq x✝¹ x✝ = false

instance Lean.Lsp.instBEqPosition : BEq Position

Equations

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

instance Lean.Lsp.instOrdPosition : Ord Position

Equations

• Lean.Lsp.instOrdPosition = { compare := Lean.Lsp.instOrdPosition.ord }

def Lean.Lsp.instOrdPosition.ord : Position → Position → Ordering

Equations

• Lean.Lsp.instOrdPosition.ord { line := a, character := a_1 } { line := b, character := b_1 } = (compare a b).then ((compare a_1 b_1).then Ordering.eq)

def Lean.Lsp.instHashablePosition.hash : Position → UInt64

Equations

• Lean.Lsp.instHashablePosition.hash { line := a, character := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

instance Lean.Lsp.instHashablePosition : Hashable Position

Equations

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

instance Lean.Lsp.instToJsonPosition : ToJson Position

Equations

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

def Lean.Lsp.instToJsonPosition.toJson : Position → Json

Equations

• Lean.Lsp.instToJsonPosition.toJson x✝ = Lean.Json.mkObj [[("line", Lean.toJson x✝.line)], [("character", Lean.toJson x✝.character)]].flatten

def Lean.Lsp.instFromJsonPosition.fromJson : Json → Except String Position

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Lsp.instFromJsonPosition : FromJson Position

Equations

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

def Lean.Lsp.instReprPosition.repr : Position → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Lsp.instReprPosition : Repr Position

Equations

• Lean.Lsp.instReprPosition = { reprPrec := Lean.Lsp.instReprPosition.repr }

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

def Lean.Lsp.instInhabitedRange.default : Range

Equations

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

instance Lean.Lsp.instInhabitedRange : Inhabited Range

Equations

• Lean.Lsp.instInhabitedRange = { default := Lean.Lsp.instInhabitedRange.default }

def Lean.Lsp.instBEqRange.beq : Range → Range → Bool

Equations

• Lean.Lsp.instBEqRange.beq { start := a, «end» := a_1 } { start := b, «end» := b_1 } = (a == b && a_1 == b_1)
• Lean.Lsp.instBEqRange.beq x✝¹ x✝ = false

instance Lean.Lsp.instBEqRange : BEq Range

Equations

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

def Lean.Lsp.instHashableRange.hash : Range → UInt64

Equations

• Lean.Lsp.instHashableRange.hash { start := a, «end» := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

instance Lean.Lsp.instHashableRange : Hashable Range

Equations

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

instance Lean.Lsp.instToJsonRange : ToJson Range

Equations

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

def Lean.Lsp.instToJsonRange.toJson : Range → Json

Equations

• Lean.Lsp.instToJsonRange.toJson x✝ = Lean.Json.mkObj [[("start", Lean.toJson x✝.start)], [("end", Lean.toJson x✝.end)]].flatten

instance Lean.Lsp.instFromJsonRange : FromJson Range

Equations

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

def Lean.Lsp.instFromJsonRange.fromJson : Json → Except String Range

Equations

• One or more equations did not get rendered due to their size.

def Lean.Lsp.instOrdRange.ord : Range → Range → Ordering

Equations

• Lean.Lsp.instOrdRange.ord { start := a, «end» := a_1 } { start := b, «end» := b_1 } = (compare a b).then ((compare a_1 b_1).then Ordering.eq)

instance Lean.Lsp.instOrdRange : Ord Range

Equations

• Lean.Lsp.instOrdRange = { compare := Lean.Lsp.instOrdRange.ord }

def Lean.Lsp.instReprRange.repr : Range → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Lsp.instReprRange : Repr Range

Equations

• Lean.Lsp.instReprRange = { reprPrec := Lean.Lsp.instReprRange.repr }

instance Lean.Lsp.instLTRange : LT Range

Equations

• Lean.Lsp.instLTRange = ltOfOrd

instance Lean.Lsp.instLERange : LE Range

Equations

• Lean.Lsp.instLERange = leOfOrd