@[reducible, inline]

abbrev Lean.Lsp.DocumentUri : Type

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

def Lean.Lsp.instInhabitedPosition.default : Position

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

instance Lean.Lsp.instBEqPosition : BEq Position

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

instance Lean.Lsp.instOrdPosition : Ord Position

instance Lean.Lsp.instHashablePosition : Hashable Position

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

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

instance Lean.Lsp.instToJsonPosition : ToJson Position

instance Lean.Lsp.instFromJsonPosition : FromJson Position

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

instance Lean.Lsp.instReprPosition : Repr Position

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

instance Lean.Lsp.instToStringPosition : ToString Position

instance Lean.Lsp.instLTPosition : LT Position

instance Lean.Lsp.instLEPosition : LE Position

structure Lean.Lsp.Range : Type

• start : Position
• end : Position

instance Lean.Lsp.instInhabitedRange : Inhabited Range

def Lean.Lsp.instInhabitedRange.default : Range

instance Lean.Lsp.instBEqRange : BEq Range

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

instance Lean.Lsp.instHashableRange : Hashable Range

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

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

instance Lean.Lsp.instToJsonRange : ToJson Range

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

instance Lean.Lsp.instFromJsonRange : FromJson Range

instance Lean.Lsp.instOrdRange : Ord Range

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

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

instance Lean.Lsp.instReprRange : Repr Range

instance Lean.Lsp.instLTRange : LT Range

instance Lean.Lsp.instLERange : LE Range