structure Lean.Lsp.CompletionOptions : Type

• triggerCharacters? : Option (Array String)
• allCommitCharacters? : Option (Array String)
• resolveProvider : Bool

def Lean.Lsp.instFromJsonCompletionOptions.fromJson : Json → Except String CompletionOptions

Equations

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

instance Lean.Lsp.instFromJsonCompletionOptions : FromJson CompletionOptions

Equations

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

def Lean.Lsp.instToJsonCompletionOptions.toJson : CompletionOptions → Json

Equations

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

instance Lean.Lsp.instToJsonCompletionOptions : ToJson CompletionOptions

Equations

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

inductive Lean.Lsp.CompletionItemKind : Type

• text : CompletionItemKind
• method : CompletionItemKind
• function : CompletionItemKind
• constructor : CompletionItemKind
• field : CompletionItemKind
• variable : CompletionItemKind
• class : CompletionItemKind
• interface : CompletionItemKind
• module : CompletionItemKind
• property : CompletionItemKind
• unit : CompletionItemKind
• value : CompletionItemKind
• enum : CompletionItemKind
• keyword : CompletionItemKind
• snippet : CompletionItemKind
• color : CompletionItemKind
• file : CompletionItemKind
• reference : CompletionItemKind
• folder : CompletionItemKind
• enumMember : CompletionItemKind
• constant : CompletionItemKind
• struct : CompletionItemKind
• event : CompletionItemKind
• operator : CompletionItemKind
• typeParameter : CompletionItemKind

def Lean.Lsp.instInhabitedCompletionItemKind.default : CompletionItemKind

Equations

• Lean.Lsp.instInhabitedCompletionItemKind.default = Lean.Lsp.CompletionItemKind.text

instance Lean.Lsp.instInhabitedCompletionItemKind : Inhabited CompletionItemKind

Equations

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

instance Lean.Lsp.instDecidableEqCompletionItemKind : DecidableEq CompletionItemKind

Equations

• Lean.Lsp.instDecidableEqCompletionItemKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Lean.Lsp.instReprCompletionItemKind.repr : CompletionItemKind → Nat → Format

Equations

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

instance Lean.Lsp.instReprCompletionItemKind : Repr CompletionItemKind

Equations

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

def Lean.Lsp.instHashableCompletionItemKind.hash : CompletionItemKind → UInt64

Equations

• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.text = 0
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.method = 1
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.function = 2
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.constructor = 3
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.field = 4
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.variable = 5
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.class = 6
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.interface = 7
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.module = 8
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.property = 9
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.unit = 10
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.value = 11
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.enum = 12
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.keyword = 13
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.snippet = 14
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.color = 15
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.file = 16
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.reference = 17
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.folder = 18
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.enumMember = 19
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.constant = 20
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.struct = 21
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.event = 22
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.operator = 23
• Lean.Lsp.instHashableCompletionItemKind.hash Lean.Lsp.CompletionItemKind.typeParameter = 24

instance Lean.Lsp.instHashableCompletionItemKind : Hashable CompletionItemKind

Equations

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

instance Lean.Lsp.instToJsonCompletionItemKind : ToJson CompletionItemKind

Equations

• Lean.Lsp.instToJsonCompletionItemKind = { toJson := fun (a : Lean.Lsp.CompletionItemKind) => Lean.toJson (a.ctorIdx + 1) }

instance Lean.Lsp.instFromJsonCompletionItemKind : FromJson CompletionItemKind

Equations

• Lean.Lsp.instFromJsonCompletionItemKind = { fromJson? := fun (v : Lean.Json) => do let i ← Lean.fromJson? v pure (Lean.Lsp.CompletionItemKind.ofNat (i - 1)) }

structure Lean.Lsp.InsertReplaceEdit : Type

• newText : String
• insert : Range
• replace : Range

instance Lean.Lsp.instFromJsonInsertReplaceEdit : FromJson InsertReplaceEdit

Equations

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

def Lean.Lsp.instFromJsonInsertReplaceEdit.fromJson : Json → Except String InsertReplaceEdit

Equations

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

instance Lean.Lsp.instToJsonInsertReplaceEdit : ToJson InsertReplaceEdit

Equations

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

def Lean.Lsp.instToJsonInsertReplaceEdit.toJson : InsertReplaceEdit → Json

Equations

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

def Lean.Lsp.instBEqInsertReplaceEdit.beq : InsertReplaceEdit → InsertReplaceEdit → Bool

Equations

• Lean.Lsp.instBEqInsertReplaceEdit.beq { newText := a, insert := a_1, replace := a_2 } { newText := b, insert := b_1, replace := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lean.Lsp.instBEqInsertReplaceEdit.beq x✝¹ x✝ = false

instance Lean.Lsp.instBEqInsertReplaceEdit : BEq InsertReplaceEdit

Equations

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

def Lean.Lsp.instHashableInsertReplaceEdit.hash : InsertReplaceEdit → UInt64

Equations

• Lean.Lsp.instHashableInsertReplaceEdit.hash { newText := a, insert := a_1, replace := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

instance Lean.Lsp.instHashableInsertReplaceEdit : Hashable InsertReplaceEdit

Equations

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

inductive Lean.Lsp.CompletionItemTag : Type

• deprecated : CompletionItemTag

def Lean.Lsp.instInhabitedCompletionItemTag.default : CompletionItemTag

Equations

• Lean.Lsp.instInhabitedCompletionItemTag.default = Lean.Lsp.CompletionItemTag.deprecated

instance Lean.Lsp.instInhabitedCompletionItemTag : Inhabited CompletionItemTag

Equations

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

instance Lean.Lsp.instDecidableEqCompletionItemTag : DecidableEq CompletionItemTag

Equations

• Lean.Lsp.instDecidableEqCompletionItemTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Lean.Lsp.instReprCompletionItemTag.repr : CompletionItemTag → Nat → Format

Equations

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

instance Lean.Lsp.instReprCompletionItemTag : Repr CompletionItemTag

Equations

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

def Lean.Lsp.instHashableCompletionItemTag.hash : CompletionItemTag → UInt64

Equations

• Lean.Lsp.instHashableCompletionItemTag.hash Lean.Lsp.CompletionItemTag.deprecated = 0

instance Lean.Lsp.instHashableCompletionItemTag : Hashable CompletionItemTag

Equations

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

instance Lean.Lsp.instToJsonCompletionItemTag : ToJson CompletionItemTag

Equations

• Lean.Lsp.instToJsonCompletionItemTag = { toJson := fun (t : Lean.Lsp.CompletionItemTag) => Lean.toJson (t.ctorIdx + 1) }

instance Lean.Lsp.instFromJsonCompletionItemTag : FromJson CompletionItemTag

Equations

• Lean.Lsp.instFromJsonCompletionItemTag = { fromJson? := fun (v : Lean.Json) => do let i ← Lean.fromJson? v pure (Lean.Lsp.CompletionItemTag.ofNat (i - 1)) }

structure Lean.Lsp.CompletionItem : Type

• label : String
• detail? : Option String
• documentation? : Option MarkupContent
• kind? : Option CompletionItemKind
• textEdit? : Option InsertReplaceEdit
• sortText? : Option String
• data? : Option Json
• tags? : Option (Array CompletionItemTag)

def Lean.Lsp.instFromJsonCompletionItem.fromJson : Json → Except String CompletionItem

Equations

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

instance Lean.Lsp.instFromJsonCompletionItem : FromJson CompletionItem

Equations

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

def Lean.Lsp.instToJsonCompletionItem.toJson : CompletionItem → Json

Equations

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

instance Lean.Lsp.instToJsonCompletionItem : ToJson CompletionItem

Equations

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

instance Lean.Lsp.instInhabitedCompletionItem : Inhabited CompletionItem

Equations

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

def Lean.Lsp.instInhabitedCompletionItem.default : CompletionItem

Equations

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

def Lean.Lsp.instBEqCompletionItem.beq : CompletionItem → CompletionItem → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Lsp.instBEqCompletionItem.beq x✝¹ x✝ = false

instance Lean.Lsp.instBEqCompletionItem : BEq CompletionItem

Equations

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

def Lean.Lsp.instHashableCompletionItem.hash : CompletionItem → UInt64

Equations

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

instance Lean.Lsp.instHashableCompletionItem : Hashable CompletionItem

Equations

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

structure Lean.Lsp.CompletionList : Type

• isIncomplete : Bool
• items : Array CompletionItem

def Lean.Lsp.instFromJsonCompletionList.fromJson : Json → Except String CompletionList

Equations

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

instance Lean.Lsp.instFromJsonCompletionList : FromJson CompletionList

Equations

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

def Lean.Lsp.instToJsonCompletionList.toJson : CompletionList → Json

Equations

• Lean.Lsp.instToJsonCompletionList.toJson x✝ = Lean.Json.mkObj [[("isIncomplete", Lean.toJson x✝.isIncomplete)], [("items", Lean.toJson x✝.items)]].flatten

instance Lean.Lsp.instToJsonCompletionList : ToJson CompletionList

Equations

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

inductive Lean.Lsp.CompletionIdentifier : Type

Identifier that is sent from the server to the client as part of the CompletionItem.data? field. Needed to resolve the CompletionItem when the client sends a completionItem/resolve request for that item, again containing the data? field provided by the server.

• const (declName : Name) : CompletionIdentifier
• fvar (id : FVarId) : CompletionIdentifier

instance Lean.Lsp.instBEqCompletionIdentifier : BEq CompletionIdentifier

Equations

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

def Lean.Lsp.instBEqCompletionIdentifier.beq : CompletionIdentifier → CompletionIdentifier → Bool

Equations

• Lean.Lsp.instBEqCompletionIdentifier.beq (Lean.Lsp.CompletionIdentifier.const a) (Lean.Lsp.CompletionIdentifier.const b) = (a == b)
• Lean.Lsp.instBEqCompletionIdentifier.beq (Lean.Lsp.CompletionIdentifier.fvar a) (Lean.Lsp.CompletionIdentifier.fvar b) = (a == b)
• Lean.Lsp.instBEqCompletionIdentifier.beq x✝¹ x✝ = false

instance Lean.Lsp.instHashableCompletionIdentifier : Hashable CompletionIdentifier

Equations

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

def Lean.Lsp.instHashableCompletionIdentifier.hash : CompletionIdentifier → UInt64

Equations

• Lean.Lsp.instHashableCompletionIdentifier.hash (Lean.Lsp.CompletionIdentifier.const a) = mixHash 0 (hash a)
• Lean.Lsp.instHashableCompletionIdentifier.hash (Lean.Lsp.CompletionIdentifier.fvar a) = mixHash 1 (hash a)

instance Lean.Lsp.instToJsonCompletionIdentifier : ToJson CompletionIdentifier

Equations

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

instance Lean.Lsp.instFromJsonCompletionIdentifier : FromJson CompletionIdentifier

Equations

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

structure Lean.Lsp.ResolvableCompletionItemData : Type

• mod : Name
• pos : Position
• cPos? : Option Nat

  Position of the completion info that this completion item was created from.

• id? : Option CompletionIdentifier

instance Lean.Lsp.instBEqResolvableCompletionItemData : BEq ResolvableCompletionItemData

Equations

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

def Lean.Lsp.instBEqResolvableCompletionItemData.beq : ResolvableCompletionItemData → ResolvableCompletionItemData → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Lsp.instBEqResolvableCompletionItemData.beq x✝¹ x✝ = false

instance Lean.Lsp.instHashableResolvableCompletionItemData : Hashable ResolvableCompletionItemData

Equations

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

def Lean.Lsp.instHashableResolvableCompletionItemData.hash : ResolvableCompletionItemData → UInt64

Equations

• Lean.Lsp.instHashableResolvableCompletionItemData.hash { mod := a, pos := a_1, cPos? := a_2, id? := a_3 } = mixHash (mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)) (hash a_3)

instance Lean.Lsp.instToJsonResolvableCompletionItemData : ToJson ResolvableCompletionItemData

Equations

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

instance Lean.Lsp.instFromJsonResolvableCompletionItemData : FromJson ResolvableCompletionItemData

Equations

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

structure Lean.Lsp.ResolvableCompletionItem : Type

• label : String
• detail? : Option String
• documentation? : Option MarkupContent
• kind? : Option CompletionItemKind
• textEdit? : Option InsertReplaceEdit
• sortText? : Option String
• data? : Option ResolvableCompletionItemData
• tags? : Option (Array CompletionItemTag)

instance Lean.Lsp.instFromJsonResolvableCompletionItem : FromJson ResolvableCompletionItem

Equations

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

def Lean.Lsp.instFromJsonResolvableCompletionItem.fromJson : Json → Except String ResolvableCompletionItem

Equations

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

instance Lean.Lsp.instToJsonResolvableCompletionItem : ToJson ResolvableCompletionItem

Equations

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

def Lean.Lsp.instToJsonResolvableCompletionItem.toJson : ResolvableCompletionItem → Json

Equations

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

instance Lean.Lsp.instInhabitedResolvableCompletionItem : Inhabited ResolvableCompletionItem

Equations

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

def Lean.Lsp.instInhabitedResolvableCompletionItem.default : ResolvableCompletionItem

Equations

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

def Lean.Lsp.instBEqResolvableCompletionItem.beq : ResolvableCompletionItem → ResolvableCompletionItem → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Lsp.instBEqResolvableCompletionItem.beq x✝¹ x✝ = false

instance Lean.Lsp.instBEqResolvableCompletionItem : BEq ResolvableCompletionItem

Equations

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

def Lean.Lsp.instHashableResolvableCompletionItem.hash : ResolvableCompletionItem → UInt64

Equations

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

instance Lean.Lsp.instHashableResolvableCompletionItem : Hashable ResolvableCompletionItem

Equations

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

structure Lean.Lsp.ResolvableCompletionList : Type

• isIncomplete : Bool
• items : Array ResolvableCompletionItem

def Lean.Lsp.instFromJsonResolvableCompletionList.fromJson : Json → Except String ResolvableCompletionList

Equations

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

instance Lean.Lsp.instFromJsonResolvableCompletionList : FromJson ResolvableCompletionList

Equations

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

def Lean.Lsp.instToJsonResolvableCompletionList.toJson : ResolvableCompletionList → Json

Equations

• Lean.Lsp.instToJsonResolvableCompletionList.toJson x✝ = Lean.Json.mkObj [[("isIncomplete", Lean.toJson x✝.isIncomplete)], [("items", Lean.toJson x✝.items)]].flatten

instance Lean.Lsp.instToJsonResolvableCompletionList : ToJson ResolvableCompletionList

Equations

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

structure Lean.Lsp.CompletionParamsextends Lean.Lsp.TextDocumentPositionParams : Type

• textDocument : TextDocumentIdentifier
• position : Position

def Lean.Lsp.instFromJsonCompletionParams.fromJson : Json → Except String CompletionParams

Equations

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

instance Lean.Lsp.instFromJsonCompletionParams : FromJson CompletionParams

Equations

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

def Lean.Lsp.instToJsonCompletionParams.toJson : CompletionParams → Json

Equations

• Lean.Lsp.instToJsonCompletionParams.toJson x✝ = Lean.Json.mkObj [[("textDocument", Lean.toJson x✝.textDocument)], [("position", Lean.toJson x✝.position)]].flatten

instance Lean.Lsp.instToJsonCompletionParams : ToJson CompletionParams

Equations

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

structure Lean.Lsp.Hover : Type

• contents : MarkupContent
• range? : Option Range

def Lean.Lsp.instToJsonHover.toJson : Hover → Json

Equations

• Lean.Lsp.instToJsonHover.toJson x✝ = Lean.Json.mkObj [[("contents", Lean.toJson x✝.contents)], Lean.Json.opt "range" x✝.range?].flatten

instance Lean.Lsp.instToJsonHover : ToJson Hover

Equations

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

instance Lean.Lsp.instFromJsonHover : FromJson Hover

Equations

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

def Lean.Lsp.instFromJsonHover.fromJson : Json → Except String Hover

Equations

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

structure Lean.Lsp.HoverParamsextends Lean.Lsp.TextDocumentPositionParams : Type

• textDocument : TextDocumentIdentifier
• position : Position

def Lean.Lsp.instFromJsonHoverParams.fromJson : Json → Except String HoverParams

Equations

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

instance Lean.Lsp.instFromJsonHoverParams : FromJson HoverParams

Equations

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

def Lean.Lsp.instToJsonHoverParams.toJson : HoverParams → Json

Equations

• Lean.Lsp.instToJsonHoverParams.toJson x✝ = Lean.Json.mkObj [[("textDocument", Lean.toJson x✝.textDocument)], [("position", Lean.toJson x✝.position)]].flatten

instance Lean.Lsp.instToJsonHoverParams : ToJson HoverParams

Equations

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

structure Lean.Lsp.DeclarationParamsextends Lean.Lsp.TextDocumentPositionParams : Type

• textDocument : TextDocumentIdentifier
• position : Position

def Lean.Lsp.instFromJsonDeclarationParams.fromJson : Json → Except String DeclarationParams

Equations

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

instance Lean.Lsp.instFromJsonDeclarationParams : FromJson DeclarationParams

Equations

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

instance Lean.Lsp.instToJsonDeclarationParams : ToJson DeclarationParams

Equations

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

def Lean.Lsp.instToJsonDeclarationParams.toJson : DeclarationParams → Json

Equations

• Lean.Lsp.instToJsonDeclarationParams.toJson x✝ = Lean.Json.mkObj [[("textDocument", Lean.toJson x✝.textDocument)], [("position", Lean.toJson x✝.position)]].flatten

structure Lean.Lsp.DefinitionParamsextends Lean.Lsp.TextDocumentPositionParams : Type

• textDocument : TextDocumentIdentifier
• position : Position

def Lean.Lsp.instFromJsonDefinitionParams.fromJson : Json → Except String DefinitionParams

Equations

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

instance Lean.Lsp.instFromJsonDefinitionParams : FromJson DefinitionParams

Equations

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

instance Lean.Lsp.instToJsonDefinitionParams : ToJson DefinitionParams

Equations

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

def Lean.Lsp.instToJsonDefinitionParams.toJson : DefinitionParams → Json

Equations

• Lean.Lsp.instToJsonDefinitionParams.toJson x✝ = Lean.Json.mkObj [[("textDocument", Lean.toJson x✝.textDocument)], [("position", Lean.toJson x✝.position)]].flatten

structure Lean.Lsp.TypeDefinitionParamsextends Lean.Lsp.TextDocumentPositionParams : Type

• textDocument : TextDocumentIdentifier
• position : Position

instance Lean.Lsp.instFromJsonTypeDefinitionParams : FromJson TypeDefinitionParams

Equations

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

def Lean.Lsp.instFromJsonTypeDefinitionParams.fromJson : Json → Except String TypeDefinitionParams

Equations

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

instance Lean.Lsp.instToJsonTypeDefinitionParams : ToJson TypeDefinitionParams

Equations

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

def Lean.Lsp.instToJsonTypeDefinitionParams.toJson : TypeDefinitionParams → Json

Equations

• Lean.Lsp.instToJsonTypeDefinitionParams.toJson x✝ = Lean.Json.mkObj [[("textDocument", Lean.toJson x✝.textDocument)], [("position", Lean.toJson x✝.position)]].flatten

structure Lean.Lsp.ReferenceContext : Type

• includeDeclaration : Bool

instance Lean.Lsp.instFromJsonReferenceContext : FromJson ReferenceContext

Equations

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

def Lean.Lsp.instFromJsonReferenceContext.fromJson : Json → Except String ReferenceContext

Equations

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

instance Lean.Lsp.instToJsonReferenceContext : ToJson ReferenceContext

Equations

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

def Lean.Lsp.instToJsonReferenceContext.toJson : ReferenceContext → Json

Equations

• Lean.Lsp.instToJsonReferenceContext.toJson x✝ = Lean.Json.mkObj [[("includeDeclaration", Lean.toJson x✝.includeDeclaration)]].flatten

structure Lean.Lsp.ReferenceParamsextends Lean.Lsp.TextDocumentPositionParams : Type

• textDocument : TextDocumentIdentifier
• position : Position
• context : ReferenceContext

instance Lean.Lsp.instFromJsonReferenceParams : FromJson ReferenceParams

Equations

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

def Lean.Lsp.instFromJsonReferenceParams.fromJson : Json → Except String ReferenceParams

Equations

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

def Lean.Lsp.instToJsonReferenceParams.toJson : ReferenceParams → Json

Equations

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

instance Lean.Lsp.instToJsonReferenceParams : ToJson ReferenceParams

Equations

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

structure Lean.Lsp.WorkspaceSymbolParams : Type

• query : String

instance Lean.Lsp.instFromJsonWorkspaceSymbolParams : FromJson WorkspaceSymbolParams

Equations

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

def Lean.Lsp.instFromJsonWorkspaceSymbolParams.fromJson : Json → Except String WorkspaceSymbolParams

Equations

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

instance Lean.Lsp.instToJsonWorkspaceSymbolParams : ToJson WorkspaceSymbolParams

Equations

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

def Lean.Lsp.instToJsonWorkspaceSymbolParams.toJson : WorkspaceSymbolParams → Json

Equations

• Lean.Lsp.instToJsonWorkspaceSymbolParams.toJson x✝ = Lean.Json.mkObj [[("query", Lean.toJson x✝.query)]].flatten

structure Lean.Lsp.DocumentHighlightParamsextends Lean.Lsp.TextDocumentPositionParams : Type

• textDocument : TextDocumentIdentifier
• position : Position

def Lean.Lsp.instFromJsonDocumentHighlightParams.fromJson : Json → Except String DocumentHighlightParams

Equations

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

instance Lean.Lsp.instFromJsonDocumentHighlightParams : FromJson DocumentHighlightParams

Equations

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

def Lean.Lsp.instToJsonDocumentHighlightParams.toJson : DocumentHighlightParams → Json

Equations

• Lean.Lsp.instToJsonDocumentHighlightParams.toJson x✝ = Lean.Json.mkObj [[("textDocument", Lean.toJson x✝.textDocument)], [("position", Lean.toJson x✝.position)]].flatten

instance Lean.Lsp.instToJsonDocumentHighlightParams : ToJson DocumentHighlightParams

Equations

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

inductive Lean.Lsp.DocumentHighlightKind : Type

• text : DocumentHighlightKind
• read : DocumentHighlightKind
• write : DocumentHighlightKind

instance Lean.Lsp.instToJsonDocumentHighlightKind : ToJson DocumentHighlightKind

Equations

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

structure Lean.Lsp.DocumentHighlight : Type

• range : Range
• kind? : Option DocumentHighlightKind

def Lean.Lsp.instToJsonDocumentHighlight.toJson : DocumentHighlight → Json

Equations

• Lean.Lsp.instToJsonDocumentHighlight.toJson x✝ = Lean.Json.mkObj [[("range", Lean.toJson x✝.range)], Lean.Json.opt "kind" x✝.kind?].flatten

instance Lean.Lsp.instToJsonDocumentHighlight : ToJson DocumentHighlight

Equations

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

@[reducible, inline]

abbrev Lean.Lsp.DocumentHighlightResult : Type

Equations

• Lean.Lsp.DocumentHighlightResult = Array Lean.Lsp.DocumentHighlight

structure Lean.Lsp.DocumentSymbolParams : Type

• textDocument : TextDocumentIdentifier

def Lean.Lsp.instFromJsonDocumentSymbolParams.fromJson : Json → Except String DocumentSymbolParams

Equations

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

instance Lean.Lsp.instFromJsonDocumentSymbolParams : FromJson DocumentSymbolParams

Equations

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

instance Lean.Lsp.instToJsonDocumentSymbolParams : ToJson DocumentSymbolParams

Equations

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

def Lean.Lsp.instToJsonDocumentSymbolParams.toJson : DocumentSymbolParams → Json

Equations

• Lean.Lsp.instToJsonDocumentSymbolParams.toJson x✝ = Lean.Json.mkObj [[("textDocument", Lean.toJson x✝.textDocument)]].flatten

inductive Lean.Lsp.SymbolKind : Type

• file : SymbolKind
• module : SymbolKind
• namespace : SymbolKind
• package : SymbolKind
• class : SymbolKind
• method : SymbolKind
• property : SymbolKind
• field : SymbolKind
• constructor : SymbolKind
• enum : SymbolKind
• interface : SymbolKind
• function : SymbolKind
• variable : SymbolKind
• constant : SymbolKind
• string : SymbolKind
• number : SymbolKind
• boolean : SymbolKind
• array : SymbolKind
• object : SymbolKind
• key : SymbolKind
• null : SymbolKind
• enumMember : SymbolKind
• struct : SymbolKind
• event : SymbolKind
• operator : SymbolKind
• typeParameter : SymbolKind

instance Lean.Lsp.instBEqSymbolKind : BEq SymbolKind

Equations

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

def Lean.Lsp.instBEqSymbolKind.beq : SymbolKind → SymbolKind → Bool

Equations

• Lean.Lsp.instBEqSymbolKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Lean.Lsp.instHashableSymbolKind.hash : SymbolKind → UInt64

Equations

• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.file = 0
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.module = 1
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.namespace = 2
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.package = 3
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.class = 4
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.method = 5
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.property = 6
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.field = 7
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.constructor = 8
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.enum = 9
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.interface = 10
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.function = 11
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.variable = 12
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.constant = 13
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.string = 14
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.number = 15
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.boolean = 16
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.array = 17
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.object = 18
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.key = 19
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.null = 20
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.enumMember = 21
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.struct = 22
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.event = 23
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.operator = 24
• Lean.Lsp.instHashableSymbolKind.hash Lean.Lsp.SymbolKind.typeParameter = 25

instance Lean.Lsp.instHashableSymbolKind : Hashable SymbolKind

Equations

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

instance Lean.Lsp.instInhabitedSymbolKind : Inhabited SymbolKind

Equations

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

def Lean.Lsp.instInhabitedSymbolKind.default : SymbolKind

Equations

• Lean.Lsp.instInhabitedSymbolKind.default = Lean.Lsp.SymbolKind.file

instance Lean.Lsp.instFromJsonSymbolKind : FromJson SymbolKind

Equations

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

instance Lean.Lsp.instToJsonSymbolKind : ToJson SymbolKind

Equations

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

structure Lean.Lsp.DocumentSymbolAux (Self : Type) : Type

• name : String
• detail? : Option String
• kind : SymbolKind
• range : Range
• selectionRange : Range
• children? : Option (Array Self)

instance Lean.Lsp.instFromJsonDocumentSymbolAux {Self✝ : Type} [FromJson Self✝] : FromJson (DocumentSymbolAux Self✝)

Equations

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

def Lean.Lsp.instFromJsonDocumentSymbolAux.fromJson {Self✝ : Type} [FromJson Self✝] : Json → Except String (DocumentSymbolAux Self✝)

Equations

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

instance Lean.Lsp.instToJsonDocumentSymbolAux {Self✝ : Type} [ToJson Self✝] : ToJson (DocumentSymbolAux Self✝)

Equations

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

def Lean.Lsp.instToJsonDocumentSymbolAux.toJson {Self✝ : Type} [ToJson Self✝] : DocumentSymbolAux Self✝ → Json

Equations

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

inductive Lean.Lsp.DocumentSymbol : Type

• mk (sym : DocumentSymbolAux DocumentSymbol) : DocumentSymbol

instance Lean.Lsp.instToJsonDocumentSymbol : ToJson DocumentSymbol

Equations

• Lean.Lsp.instToJsonDocumentSymbol = { toJson := Lean.Lsp.instToJsonDocumentSymbol.go }

partial def Lean.Lsp.instToJsonDocumentSymbol.go : DocumentSymbol → Json

structure Lean.Lsp.DocumentSymbolResult : Type

• syms : Array DocumentSymbol

instance Lean.Lsp.instToJsonDocumentSymbolResult : ToJson DocumentSymbolResult

Equations

• Lean.Lsp.instToJsonDocumentSymbolResult = { toJson := fun (dsr : Lean.Lsp.DocumentSymbolResult) => Lean.toJson dsr.syms }

inductive Lean.Lsp.SymbolTag : Type

• deprecated : SymbolTag

instance Lean.Lsp.instBEqSymbolTag : BEq SymbolTag

Equations

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

def Lean.Lsp.instBEqSymbolTag.beq : SymbolTag → SymbolTag → Bool

Equations

• Lean.Lsp.instBEqSymbolTag.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Lean.Lsp.instHashableSymbolTag : Hashable SymbolTag

Equations

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

def Lean.Lsp.instHashableSymbolTag.hash : SymbolTag → UInt64

Equations

• Lean.Lsp.instHashableSymbolTag.hash Lean.Lsp.SymbolTag.deprecated = 0

instance Lean.Lsp.instInhabitedSymbolTag : Inhabited SymbolTag

Equations

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

def Lean.Lsp.instInhabitedSymbolTag.default : SymbolTag

Equations

• Lean.Lsp.instInhabitedSymbolTag.default = Lean.Lsp.SymbolTag.deprecated

instance Lean.Lsp.instFromJsonSymbolTag : FromJson SymbolTag

Equations

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

instance Lean.Lsp.instToJsonSymbolTag : ToJson SymbolTag

Equations

• Lean.Lsp.instToJsonSymbolTag = { toJson := fun (x : Lean.Lsp.SymbolTag) => match x with | Lean.Lsp.SymbolTag.deprecated => 1 }

structure Lean.Lsp.SymbolInformation : Type

• name : String
• kind : SymbolKind
• tags : Array SymbolTag
• location : Location
• containerName? : Option String

def Lean.Lsp.instFromJsonSymbolInformation.fromJson : Json → Except String SymbolInformation

Equations

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

instance Lean.Lsp.instFromJsonSymbolInformation : FromJson SymbolInformation

Equations

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

def Lean.Lsp.instToJsonSymbolInformation.toJson : SymbolInformation → Json

Equations

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

instance Lean.Lsp.instToJsonSymbolInformation : ToJson SymbolInformation

Equations

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

structure Lean.Lsp.CallHierarchyPrepareParamsextends Lean.Lsp.TextDocumentPositionParams : Type

• textDocument : TextDocumentIdentifier
• position : Position

instance Lean.Lsp.instFromJsonCallHierarchyPrepareParams : FromJson CallHierarchyPrepareParams

Equations

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

def Lean.Lsp.instFromJsonCallHierarchyPrepareParams.fromJson : Json → Except String CallHierarchyPrepareParams

Equations

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

instance Lean.Lsp.instToJsonCallHierarchyPrepareParams : ToJson CallHierarchyPrepareParams

Equations

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

def Lean.Lsp.instToJsonCallHierarchyPrepareParams.toJson : CallHierarchyPrepareParams → Json

Equations

• Lean.Lsp.instToJsonCallHierarchyPrepareParams.toJson x✝ = Lean.Json.mkObj [[("textDocument", Lean.toJson x✝.textDocument)], [("position", Lean.toJson x✝.position)]].flatten

structure Lean.Lsp.CallHierarchyItem : Type

• name : String
• kind : SymbolKind
• tags? : Option (Array SymbolTag)
• detail? : Option String
• uri : DocumentUri
• range : Range
• selectionRange : Range
• data? : Option Json

def Lean.Lsp.instFromJsonCallHierarchyItem.fromJson : Json → Except String CallHierarchyItem

Equations

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

instance Lean.Lsp.instFromJsonCallHierarchyItem : FromJson CallHierarchyItem

Equations

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

def Lean.Lsp.instToJsonCallHierarchyItem.toJson : CallHierarchyItem → Json

Equations

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

instance Lean.Lsp.instToJsonCallHierarchyItem : ToJson CallHierarchyItem

Equations

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

def Lean.Lsp.instBEqCallHierarchyItem.beq : CallHierarchyItem → CallHierarchyItem → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Lsp.instBEqCallHierarchyItem.beq x✝¹ x✝ = false

instance Lean.Lsp.instBEqCallHierarchyItem : BEq CallHierarchyItem

Equations

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

def Lean.Lsp.instHashableCallHierarchyItem.hash : CallHierarchyItem → UInt64

Equations

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

instance Lean.Lsp.instHashableCallHierarchyItem : Hashable CallHierarchyItem

Equations

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

def Lean.Lsp.instInhabitedCallHierarchyItem.default : CallHierarchyItem

Equations

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

instance Lean.Lsp.instInhabitedCallHierarchyItem : Inhabited CallHierarchyItem

Equations

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

structure Lean.Lsp.CallHierarchyIncomingCallsParams : Type

• item : CallHierarchyItem

instance Lean.Lsp.instFromJsonCallHierarchyIncomingCallsParams : FromJson CallHierarchyIncomingCallsParams

Equations

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

def Lean.Lsp.instFromJsonCallHierarchyIncomingCallsParams.fromJson : Json → Except String CallHierarchyIncomingCallsParams

Equations

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

def Lean.Lsp.instToJsonCallHierarchyIncomingCallsParams.toJson : CallHierarchyIncomingCallsParams → Json

Equations

• Lean.Lsp.instToJsonCallHierarchyIncomingCallsParams.toJson x✝ = Lean.Json.mkObj [[("item", Lean.toJson x✝.item)]].flatten

instance Lean.Lsp.instToJsonCallHierarchyIncomingCallsParams : ToJson CallHierarchyIncomingCallsParams

Equations

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

structure Lean.Lsp.CallHierarchyIncomingCall : Type

• from : CallHierarchyItem
• fromRanges : Array Range

def Lean.Lsp.instFromJsonCallHierarchyIncomingCall.fromJson : Json → Except String CallHierarchyIncomingCall

Equations

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

instance Lean.Lsp.instFromJsonCallHierarchyIncomingCall : FromJson CallHierarchyIncomingCall

Equations

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

def Lean.Lsp.instToJsonCallHierarchyIncomingCall.toJson : CallHierarchyIncomingCall → Json

Equations

• Lean.Lsp.instToJsonCallHierarchyIncomingCall.toJson x✝ = Lean.Json.mkObj [[("from", Lean.toJson x✝.from)], [("fromRanges", Lean.toJson x✝.fromRanges)]].flatten

instance Lean.Lsp.instToJsonCallHierarchyIncomingCall : ToJson CallHierarchyIncomingCall

Equations

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

def Lean.Lsp.instInhabitedCallHierarchyIncomingCall.default : CallHierarchyIncomingCall

Equations

• Lean.Lsp.instInhabitedCallHierarchyIncomingCall.default = { «from» := default, fromRanges := default }

instance Lean.Lsp.instInhabitedCallHierarchyIncomingCall : Inhabited CallHierarchyIncomingCall

Equations

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

structure Lean.Lsp.CallHierarchyOutgoingCallsParams : Type

• item : CallHierarchyItem

instance Lean.Lsp.instFromJsonCallHierarchyOutgoingCallsParams : FromJson CallHierarchyOutgoingCallsParams

Equations

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

def Lean.Lsp.instFromJsonCallHierarchyOutgoingCallsParams.fromJson : Json → Except String CallHierarchyOutgoingCallsParams

Equations

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

def Lean.Lsp.instToJsonCallHierarchyOutgoingCallsParams.toJson : CallHierarchyOutgoingCallsParams → Json

Equations

• Lean.Lsp.instToJsonCallHierarchyOutgoingCallsParams.toJson x✝ = Lean.Json.mkObj [[("item", Lean.toJson x✝.item)]].flatten

instance Lean.Lsp.instToJsonCallHierarchyOutgoingCallsParams : ToJson CallHierarchyOutgoingCallsParams

Equations

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

structure Lean.Lsp.CallHierarchyOutgoingCall : Type

• to : CallHierarchyItem
• fromRanges : Array Range

instance Lean.Lsp.instFromJsonCallHierarchyOutgoingCall : FromJson CallHierarchyOutgoingCall

Equations

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

def Lean.Lsp.instFromJsonCallHierarchyOutgoingCall.fromJson : Json → Except String CallHierarchyOutgoingCall

Equations

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

def Lean.Lsp.instToJsonCallHierarchyOutgoingCall.toJson : CallHierarchyOutgoingCall → Json

Equations

• Lean.Lsp.instToJsonCallHierarchyOutgoingCall.toJson x✝ = Lean.Json.mkObj [[("to", Lean.toJson x✝.to)], [("fromRanges", Lean.toJson x✝.fromRanges)]].flatten

instance Lean.Lsp.instToJsonCallHierarchyOutgoingCall : ToJson CallHierarchyOutgoingCall

Equations

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

instance Lean.Lsp.instInhabitedCallHierarchyOutgoingCall : Inhabited CallHierarchyOutgoingCall

Equations

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

def Lean.Lsp.instInhabitedCallHierarchyOutgoingCall.default : CallHierarchyOutgoingCall

Equations

• Lean.Lsp.instInhabitedCallHierarchyOutgoingCall.default = { to := default, fromRanges := default }

inductive Lean.Lsp.SemanticTokenType : Type

• keyword : SemanticTokenType
• variable : SemanticTokenType
• property : SemanticTokenType
• function : SemanticTokenType
• namespace : SemanticTokenType
• type : SemanticTokenType
• class : SemanticTokenType
• enum : SemanticTokenType
• interface : SemanticTokenType
• struct : SemanticTokenType
• typeParameter : SemanticTokenType
• parameter : SemanticTokenType
• enumMember : SemanticTokenType
• event : SemanticTokenType
• method : SemanticTokenType
• macro : SemanticTokenType
• modifier : SemanticTokenType
• comment : SemanticTokenType
• string : SemanticTokenType
• number : SemanticTokenType
• regexp : SemanticTokenType
• operator : SemanticTokenType
• decorator : SemanticTokenType
• leanSorryLike : SemanticTokenType

def Lean.Lsp.instToJsonSemanticTokenType.toJson : SemanticTokenType → Json

Equations

• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.keyword = Lean.toJson "keyword"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.variable = Lean.toJson "variable"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.property = Lean.toJson "property"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.function = Lean.toJson "function"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.namespace = Lean.toJson "namespace"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.type = Lean.toJson "type"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.class = Lean.toJson "class"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.enum = Lean.toJson "enum"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.interface = Lean.toJson "interface"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.struct = Lean.toJson "struct"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.typeParameter = Lean.toJson "typeParameter"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.parameter = Lean.toJson "parameter"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.enumMember = Lean.toJson "enumMember"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.event = Lean.toJson "event"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.method = Lean.toJson "method"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.macro = Lean.toJson "macro"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.modifier = Lean.toJson "modifier"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.comment = Lean.toJson "comment"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.string = Lean.toJson "string"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.number = Lean.toJson "number"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.regexp = Lean.toJson "regexp"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.operator = Lean.toJson "operator"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.decorator = Lean.toJson "decorator"
• Lean.Lsp.instToJsonSemanticTokenType.toJson Lean.Lsp.SemanticTokenType.leanSorryLike = Lean.toJson "leanSorryLike"

instance Lean.Lsp.instToJsonSemanticTokenType : ToJson SemanticTokenType

Equations

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

def Lean.Lsp.instFromJsonSemanticTokenType.fromJson : Json → Except String SemanticTokenType

Equations

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

instance Lean.Lsp.instFromJsonSemanticTokenType : FromJson SemanticTokenType

Equations

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

def Lean.Lsp.instBEqSemanticTokenType.beq : SemanticTokenType → SemanticTokenType → Bool

Equations

• Lean.Lsp.instBEqSemanticTokenType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Lean.Lsp.instBEqSemanticTokenType : BEq SemanticTokenType

Equations

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

instance Lean.Lsp.instHashableSemanticTokenType : Hashable SemanticTokenType

Equations

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

def Lean.Lsp.instHashableSemanticTokenType.hash : SemanticTokenType → UInt64

Equations

• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.keyword = 0
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.variable = 1
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.property = 2
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.function = 3
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.namespace = 4
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.type = 5
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.class = 6
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.enum = 7
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.interface = 8
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.struct = 9
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.typeParameter = 10
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.parameter = 11
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.enumMember = 12
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.event = 13
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.method = 14
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.macro = 15
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.modifier = 16
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.comment = 17
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.string = 18
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.number = 19
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.regexp = 20
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.operator = 21
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.decorator = 22
• Lean.Lsp.instHashableSemanticTokenType.hash Lean.Lsp.SemanticTokenType.leanSorryLike = 23

def Lean.Lsp.SemanticTokenType.names : Array String

Equations

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

def Lean.Lsp.SemanticTokenType.toNat (tokenType : SemanticTokenType) : Nat

Equations

• tokenType.toNat = tokenType.ctorIdx

inductive Lean.Lsp.SemanticTokenModifier : Type

The semantic token modifiers included by default in the LSP specification. Not used by the Lean core, but implementing them here allows them to be utilized by users extending the Lean server.

• declaration : SemanticTokenModifier
• definition : SemanticTokenModifier
• readonly : SemanticTokenModifier
• static : SemanticTokenModifier
• deprecated : SemanticTokenModifier
• abstract : SemanticTokenModifier
• async : SemanticTokenModifier
• modification : SemanticTokenModifier
• documentation : SemanticTokenModifier
• defaultLibrary : SemanticTokenModifier

def Lean.Lsp.instToJsonSemanticTokenModifier.toJson : SemanticTokenModifier → Json

Equations

• Lean.Lsp.instToJsonSemanticTokenModifier.toJson Lean.Lsp.SemanticTokenModifier.declaration = Lean.toJson "declaration"
• Lean.Lsp.instToJsonSemanticTokenModifier.toJson Lean.Lsp.SemanticTokenModifier.definition = Lean.toJson "definition"
• Lean.Lsp.instToJsonSemanticTokenModifier.toJson Lean.Lsp.SemanticTokenModifier.readonly = Lean.toJson "readonly"
• Lean.Lsp.instToJsonSemanticTokenModifier.toJson Lean.Lsp.SemanticTokenModifier.static = Lean.toJson "static"
• Lean.Lsp.instToJsonSemanticTokenModifier.toJson Lean.Lsp.SemanticTokenModifier.deprecated = Lean.toJson "deprecated"
• Lean.Lsp.instToJsonSemanticTokenModifier.toJson Lean.Lsp.SemanticTokenModifier.abstract = Lean.toJson "abstract"
• Lean.Lsp.instToJsonSemanticTokenModifier.toJson Lean.Lsp.SemanticTokenModifier.async = Lean.toJson "async"
• Lean.Lsp.instToJsonSemanticTokenModifier.toJson Lean.Lsp.SemanticTokenModifier.modification = Lean.toJson "modification"
• Lean.Lsp.instToJsonSemanticTokenModifier.toJson Lean.Lsp.SemanticTokenModifier.documentation = Lean.toJson "documentation"
• Lean.Lsp.instToJsonSemanticTokenModifier.toJson Lean.Lsp.SemanticTokenModifier.defaultLibrary = Lean.toJson "defaultLibrary"

instance Lean.Lsp.instToJsonSemanticTokenModifier : ToJson SemanticTokenModifier

Equations

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

def Lean.Lsp.instFromJsonSemanticTokenModifier.fromJson : Json → Except String SemanticTokenModifier

Equations

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

instance Lean.Lsp.instFromJsonSemanticTokenModifier : FromJson SemanticTokenModifier

Equations

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

def Lean.Lsp.SemanticTokenModifier.names : Array String

Equations

• Lean.Lsp.SemanticTokenModifier.names = #["declaration", "definition", "readonly", "static", "deprecated", "abstract", "async", "modification", "documentation", "defaultLibrary"]

def Lean.Lsp.SemanticTokenModifier.toNat (modifier : SemanticTokenModifier) : Nat

Equations

• modifier.toNat = modifier.ctorIdx

structure Lean.Lsp.SemanticTokensLegend : Type

• tokenTypes : Array String
• tokenModifiers : Array String

def Lean.Lsp.instFromJsonSemanticTokensLegend.fromJson : Json → Except String SemanticTokensLegend

Equations

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

instance Lean.Lsp.instFromJsonSemanticTokensLegend : FromJson SemanticTokensLegend

Equations

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

instance Lean.Lsp.instToJsonSemanticTokensLegend : ToJson SemanticTokensLegend

Equations

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

def Lean.Lsp.instToJsonSemanticTokensLegend.toJson : SemanticTokensLegend → Json

Equations

• Lean.Lsp.instToJsonSemanticTokensLegend.toJson x✝ = Lean.Json.mkObj [[("tokenTypes", Lean.toJson x✝.tokenTypes)], [("tokenModifiers", Lean.toJson x✝.tokenModifiers)]].flatten

structure Lean.Lsp.SemanticTokensOptions : Type

• legend : SemanticTokensLegend
• range : Bool
• full : Bool

instance Lean.Lsp.instFromJsonSemanticTokensOptions : FromJson SemanticTokensOptions

Equations

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

def Lean.Lsp.instFromJsonSemanticTokensOptions.fromJson : Json → Except String SemanticTokensOptions

Equations

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

def Lean.Lsp.instToJsonSemanticTokensOptions.toJson : SemanticTokensOptions → Json

Equations

• Lean.Lsp.instToJsonSemanticTokensOptions.toJson x✝ = Lean.Json.mkObj [[("legend", Lean.toJson x✝.legend)], [("range", Lean.toJson x✝.range)], [("full", Lean.toJson x✝.full)]].flatten

instance Lean.Lsp.instToJsonSemanticTokensOptions : ToJson SemanticTokensOptions

Equations

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

structure Lean.Lsp.SemanticTokensParams : Type

• textDocument : TextDocumentIdentifier

instance Lean.Lsp.instFromJsonSemanticTokensParams : FromJson SemanticTokensParams

Equations

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

def Lean.Lsp.instFromJsonSemanticTokensParams.fromJson : Json → Except String SemanticTokensParams

Equations

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

instance Lean.Lsp.instToJsonSemanticTokensParams : ToJson SemanticTokensParams

Equations

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

def Lean.Lsp.instToJsonSemanticTokensParams.toJson : SemanticTokensParams → Json

Equations

• Lean.Lsp.instToJsonSemanticTokensParams.toJson x✝ = Lean.Json.mkObj [[("textDocument", Lean.toJson x✝.textDocument)]].flatten

structure Lean.Lsp.SemanticTokensRangeParams : Type

• textDocument : TextDocumentIdentifier
• range : Range

def Lean.Lsp.instFromJsonSemanticTokensRangeParams.fromJson : Json → Except String SemanticTokensRangeParams

Equations

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

instance Lean.Lsp.instFromJsonSemanticTokensRangeParams : FromJson SemanticTokensRangeParams

Equations

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

instance Lean.Lsp.instToJsonSemanticTokensRangeParams : ToJson SemanticTokensRangeParams

Equations

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

def Lean.Lsp.instToJsonSemanticTokensRangeParams.toJson : SemanticTokensRangeParams → Json

Equations

• Lean.Lsp.instToJsonSemanticTokensRangeParams.toJson x✝ = Lean.Json.mkObj [[("textDocument", Lean.toJson x✝.textDocument)], [("range", Lean.toJson x✝.range)]].flatten

structure Lean.Lsp.SemanticTokens : Type

• resultId? : Option String
• data : Array Nat

def Lean.Lsp.instFromJsonSemanticTokens.fromJson : Json → Except String SemanticTokens

Equations

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

instance Lean.Lsp.instFromJsonSemanticTokens : FromJson SemanticTokens

Equations

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

instance Lean.Lsp.instToJsonSemanticTokens : ToJson SemanticTokens

Equations

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

def Lean.Lsp.instToJsonSemanticTokens.toJson : SemanticTokens → Json

Equations

• Lean.Lsp.instToJsonSemanticTokens.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "resultId" x✝.resultId?, [("data", Lean.toJson x✝.data)]].flatten

structure Lean.Lsp.FoldingRangeParams : Type

• textDocument : TextDocumentIdentifier

instance Lean.Lsp.instFromJsonFoldingRangeParams : FromJson FoldingRangeParams

Equations

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

def Lean.Lsp.instFromJsonFoldingRangeParams.fromJson : Json → Except String FoldingRangeParams

Equations

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

def Lean.Lsp.instToJsonFoldingRangeParams.toJson : FoldingRangeParams → Json

Equations

• Lean.Lsp.instToJsonFoldingRangeParams.toJson x✝ = Lean.Json.mkObj [[("textDocument", Lean.toJson x✝.textDocument)]].flatten

instance Lean.Lsp.instToJsonFoldingRangeParams : ToJson FoldingRangeParams

Equations

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

inductive Lean.Lsp.FoldingRangeKind : Type

• comment : FoldingRangeKind
• imports : FoldingRangeKind
• region : FoldingRangeKind

instance Lean.Lsp.instToJsonFoldingRangeKind : ToJson FoldingRangeKind

Equations

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

structure Lean.Lsp.FoldingRange : Type

• startLine : Nat
• endLine : Nat
• kind? : Option FoldingRangeKind

def Lean.Lsp.instToJsonFoldingRange.toJson : FoldingRange → Json

Equations

• Lean.Lsp.instToJsonFoldingRange.toJson x✝ = Lean.Json.mkObj [[("startLine", Lean.toJson x✝.startLine)], [("endLine", Lean.toJson x✝.endLine)], Lean.Json.opt "kind" x✝.kind?].flatten

instance Lean.Lsp.instToJsonFoldingRange : ToJson FoldingRange

Equations

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

structure Lean.Lsp.RenameOptions : Type

• prepareProvider : Bool

def Lean.Lsp.instFromJsonRenameOptions.fromJson : Json → Except String RenameOptions

Equations

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

instance Lean.Lsp.instFromJsonRenameOptions : FromJson RenameOptions

Equations

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

instance Lean.Lsp.instToJsonRenameOptions : ToJson RenameOptions

Equations

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

def Lean.Lsp.instToJsonRenameOptions.toJson : RenameOptions → Json

Equations

• Lean.Lsp.instToJsonRenameOptions.toJson x✝ = Lean.Json.mkObj [[("prepareProvider", Lean.toJson x✝.prepareProvider)]].flatten

structure Lean.Lsp.RenameParamsextends Lean.Lsp.TextDocumentPositionParams : Type

• textDocument : TextDocumentIdentifier
• position : Position
• newName : String

instance Lean.Lsp.instFromJsonRenameParams : FromJson RenameParams

Equations

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

def Lean.Lsp.instFromJsonRenameParams.fromJson : Json → Except String RenameParams

Equations

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

def Lean.Lsp.instToJsonRenameParams.toJson : RenameParams → Json

Equations

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

instance Lean.Lsp.instToJsonRenameParams : ToJson RenameParams

Equations

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

structure Lean.Lsp.PrepareRenameParamsextends Lean.Lsp.TextDocumentPositionParams : Type

• textDocument : TextDocumentIdentifier
• position : Position

def Lean.Lsp.instFromJsonPrepareRenameParams.fromJson : Json → Except String PrepareRenameParams

Equations

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

instance Lean.Lsp.instFromJsonPrepareRenameParams : FromJson PrepareRenameParams

Equations

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

instance Lean.Lsp.instToJsonPrepareRenameParams : ToJson PrepareRenameParams

Equations

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

def Lean.Lsp.instToJsonPrepareRenameParams.toJson : PrepareRenameParams → Json

Equations

• Lean.Lsp.instToJsonPrepareRenameParams.toJson x✝ = Lean.Json.mkObj [[("textDocument", Lean.toJson x✝.textDocument)], [("position", Lean.toJson x✝.position)]].flatten

structure Lean.Lsp.InlayHintParamsextends Lean.Lsp.WorkDoneProgressParams : Type

• workDoneToken? : Option ProgressToken
• textDocument : TextDocumentIdentifier
• range : Range

instance Lean.Lsp.instFromJsonInlayHintParams : FromJson InlayHintParams

Equations

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

def Lean.Lsp.instFromJsonInlayHintParams.fromJson : Json → Except String InlayHintParams

Equations

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

def Lean.Lsp.instToJsonInlayHintParams.toJson : InlayHintParams → Json

Equations

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

instance Lean.Lsp.instToJsonInlayHintParams : ToJson InlayHintParams

Equations

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

inductive Lean.Lsp.InlayHintTooltip : Type

• plaintext (text : String) : InlayHintTooltip
• markdown (markup : MarkupContent) : InlayHintTooltip

instance Lean.Lsp.instFromJsonInlayHintTooltip : FromJson InlayHintTooltip

Equations

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

instance Lean.Lsp.instToJsonInlayHintTooltip : ToJson InlayHintTooltip

Equations

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

structure Lean.Lsp.InlayHintLabelPart : Type

• value : String
• tooltip? : Option InlayHintTooltip
• location? : Option Location
• command? : Option Command

instance Lean.Lsp.instFromJsonInlayHintLabelPart : FromJson InlayHintLabelPart

Equations

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

def Lean.Lsp.instFromJsonInlayHintLabelPart.fromJson : Json → Except String InlayHintLabelPart

Equations

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

instance Lean.Lsp.instToJsonInlayHintLabelPart : ToJson InlayHintLabelPart

Equations

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

def Lean.Lsp.instToJsonInlayHintLabelPart.toJson : InlayHintLabelPart → Json

Equations

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

inductive Lean.Lsp.InlayHintLabel : Type

• name (n : String) : InlayHintLabel
• parts (p : Array InlayHintLabelPart) : InlayHintLabel

instance Lean.Lsp.instFromJsonInlayHintLabel : FromJson InlayHintLabel

Equations

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

instance Lean.Lsp.instToJsonInlayHintLabel : ToJson InlayHintLabel

Equations

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

inductive Lean.Lsp.InlayHintKind : Type

• type : InlayHintKind
• parameter : InlayHintKind

instance Lean.Lsp.instFromJsonInlayHintKind : FromJson InlayHintKind

Equations

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

instance Lean.Lsp.instToJsonInlayHintKind : ToJson InlayHintKind

Equations

• Lean.Lsp.instToJsonInlayHintKind = { toJson := fun (x : Lean.Lsp.InlayHintKind) => match x with | Lean.Lsp.InlayHintKind.type => 1 | Lean.Lsp.InlayHintKind.parameter => 2 }

structure Lean.Lsp.InlayHint : Type

• position : Position
• label : InlayHintLabel
• kind? : Option InlayHintKind
• textEdits? : Option (Array TextEdit)
• tooltip? : Option InlayHintTooltip
• paddingLeft? : Option Bool
• paddingRight? : Option Bool
• data? : Option Json

instance Lean.Lsp.instFromJsonInlayHint : FromJson InlayHint

Equations

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

def Lean.Lsp.instFromJsonInlayHint.fromJson : Json → Except String InlayHint

Equations

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

def Lean.Lsp.instToJsonInlayHint.toJson : InlayHint → Json

Equations

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

instance Lean.Lsp.instToJsonInlayHint : ToJson InlayHint

Equations

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

structure Lean.Lsp.InlayHintClientCapabilities : Type

• dynamicRegistration? : Option Bool
• resolveSupport? : Option ResolveSupport

def Lean.Lsp.instFromJsonInlayHintClientCapabilities.fromJson : Json → Except String InlayHintClientCapabilities

Equations

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

instance Lean.Lsp.instFromJsonInlayHintClientCapabilities : FromJson InlayHintClientCapabilities

Equations

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

instance Lean.Lsp.instToJsonInlayHintClientCapabilities : ToJson InlayHintClientCapabilities

Equations

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

def Lean.Lsp.instToJsonInlayHintClientCapabilities.toJson : InlayHintClientCapabilities → Json

Equations

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

structure Lean.Lsp.InlayHintOptionsextends Lean.Lsp.WorkDoneProgressOptions : Type

• workDoneProgress : Bool
• resolveProvider? : Option Bool

instance Lean.Lsp.instFromJsonInlayHintOptions : FromJson InlayHintOptions

Equations

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

def Lean.Lsp.instFromJsonInlayHintOptions.fromJson : Json → Except String InlayHintOptions

Equations

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

def Lean.Lsp.instToJsonInlayHintOptions.toJson : InlayHintOptions → Json

Equations

• Lean.Lsp.instToJsonInlayHintOptions.toJson x✝ = Lean.Json.mkObj [[("workDoneProgress", Lean.toJson x✝.workDoneProgress)], Lean.Json.opt "resolveProvider" x✝.resolveProvider?].flatten

instance Lean.Lsp.instToJsonInlayHintOptions : ToJson InlayHintOptions

Equations

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

inductive Lean.Lsp.ParameterInformationLabel : Type

• name (name : String) : ParameterInformationLabel
• range (startUtf16Offset endUtf16Offset : Nat) : ParameterInformationLabel

instance Lean.Lsp.instFromJsonParameterInformationLabel : FromJson ParameterInformationLabel

Equations

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

instance Lean.Lsp.instToJsonParameterInformationLabel : ToJson ParameterInformationLabel

Equations

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

structure Lean.Lsp.ParameterInformation : Type

• label : ParameterInformationLabel
• documentation? : Option MarkupContent

def Lean.Lsp.instFromJsonParameterInformation.fromJson : Json → Except String ParameterInformation

Equations

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

instance Lean.Lsp.instFromJsonParameterInformation : FromJson ParameterInformation

Equations

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

def Lean.Lsp.instToJsonParameterInformation.toJson : ParameterInformation → Json

Equations

• Lean.Lsp.instToJsonParameterInformation.toJson x✝ = Lean.Json.mkObj [[("label", Lean.toJson x✝.label)], Lean.Json.opt "documentation" x✝.documentation?].flatten

instance Lean.Lsp.instToJsonParameterInformation : ToJson ParameterInformation

Equations

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

structure Lean.Lsp.SignatureInformation : Type

• label : String
• documentation? : Option MarkupContent
• parameters? : Option (Array ParameterInformation)
• activeParameter? : Option Nat

def Lean.Lsp.instFromJsonSignatureInformation.fromJson : Json → Except String SignatureInformation

Equations

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

instance Lean.Lsp.instFromJsonSignatureInformation : FromJson SignatureInformation

Equations

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

def Lean.Lsp.instToJsonSignatureInformation.toJson : SignatureInformation → Json

Equations

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

instance Lean.Lsp.instToJsonSignatureInformation : ToJson SignatureInformation

Equations

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

structure Lean.Lsp.SignatureHelp : Type

• signatures : Array SignatureInformation
• activeSignature? : Option Nat
• activeParameter? : Option Nat

def Lean.Lsp.instFromJsonSignatureHelp.fromJson : Json → Except String SignatureHelp

Equations

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

instance Lean.Lsp.instFromJsonSignatureHelp : FromJson SignatureHelp

Equations

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

def Lean.Lsp.instToJsonSignatureHelp.toJson : SignatureHelp → Json

Equations

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

instance Lean.Lsp.instToJsonSignatureHelp : ToJson SignatureHelp

Equations

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

inductive Lean.Lsp.SignatureHelpTriggerKind : Type

• invoked : SignatureHelpTriggerKind
• triggerCharacter : SignatureHelpTriggerKind
• contentChange : SignatureHelpTriggerKind

instance Lean.Lsp.instFromJsonSignatureHelpTriggerKind : FromJson SignatureHelpTriggerKind

Equations

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

instance Lean.Lsp.instToJsonSignatureHelpTriggerKind : ToJson SignatureHelpTriggerKind

Equations

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

structure Lean.Lsp.SignatureHelpContext : Type

• triggerKind : SignatureHelpTriggerKind
• triggerCharacter? : Option String
• isRetrigger : Bool
• activeSignatureHelp? : Option SignatureHelp

instance Lean.Lsp.instFromJsonSignatureHelpContext : FromJson SignatureHelpContext

Equations

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

def Lean.Lsp.instFromJsonSignatureHelpContext.fromJson : Json → Except String SignatureHelpContext

Equations

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

def Lean.Lsp.instToJsonSignatureHelpContext.toJson : SignatureHelpContext → Json

Equations

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

instance Lean.Lsp.instToJsonSignatureHelpContext : ToJson SignatureHelpContext

Equations

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

structure Lean.Lsp.SignatureHelpParamsextends Lean.Lsp.TextDocumentPositionParams, Lean.Lsp.WorkDoneProgressParams : Type

• textDocument : TextDocumentIdentifier
• position : Position
• workDoneToken? : Option ProgressToken
• context? : Option SignatureHelpContext

def Lean.Lsp.instFromJsonSignatureHelpParams.fromJson : Json → Except String SignatureHelpParams

Equations

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

instance Lean.Lsp.instFromJsonSignatureHelpParams : FromJson SignatureHelpParams

Equations

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

def Lean.Lsp.instToJsonSignatureHelpParams.toJson : SignatureHelpParams → Json

Equations

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

instance Lean.Lsp.instToJsonSignatureHelpParams : ToJson SignatureHelpParams

Equations

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

structure Lean.Lsp.SignatureHelpOptionsextends Lean.Lsp.WorkDoneProgressOptions : Type

• workDoneProgress : Bool
• triggerCharacters? : Option (Array String)
• retriggerCharacters? : Option (Array String)

instance Lean.Lsp.instFromJsonSignatureHelpOptions : FromJson SignatureHelpOptions

Equations

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

def Lean.Lsp.instFromJsonSignatureHelpOptions.fromJson : Json → Except String SignatureHelpOptions

Equations

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

instance Lean.Lsp.instToJsonSignatureHelpOptions : ToJson SignatureHelpOptions

Equations

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

def Lean.Lsp.instToJsonSignatureHelpOptions.toJson : SignatureHelpOptions → Json

Equations

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