structure Lean.Lsp.CompletionOptions : Type

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCompletionOptions : FromJson CompletionOptions

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonCompletionOptions : ToJson CompletionOptions

Equations

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

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

Equations

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

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

@[implicit_reducible]

instance Lean.Lsp.instInhabitedCompletionItemKind : Inhabited CompletionItemKind

Equations

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

def Lean.Lsp.instInhabitedCompletionItemKind.default : CompletionItemKind

Equations

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

@[implicit_reducible]

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.

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instHashableCompletionItemKind : Hashable CompletionItemKind

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonCompletionItemKind : ToJson CompletionItemKind

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

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.

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonInsertReplaceEdit : ToJson InsertReplaceEdit

Equations

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

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

@[implicit_reducible]

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)

@[implicit_reducible]

instance Lean.Lsp.instHashableInsertReplaceEdit : Hashable InsertReplaceEdit

Equations

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

inductive Lean.Lsp.CompletionItemTag : Type

• deprecated : CompletionItemTag

@[implicit_reducible]

instance Lean.Lsp.instInhabitedCompletionItemTag : Inhabited CompletionItemTag

Equations

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

def Lean.Lsp.instInhabitedCompletionItemTag.default : CompletionItemTag

Equations

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

@[implicit_reducible]

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.

@[implicit_reducible]

instance Lean.Lsp.instReprCompletionItemTag : Repr CompletionItemTag

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instHashableCompletionItemTag : Hashable CompletionItemTag

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonCompletionItemTag : ToJson CompletionItemTag

Equations

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

@[implicit_reducible]

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.

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCompletionItem : FromJson CompletionItem

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonCompletionItem : ToJson CompletionItem

Equations

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

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

Equations

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

def Lean.Lsp.instInhabitedCompletionItem.default : CompletionItem

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instInhabitedCompletionItem : Inhabited CompletionItem

Equations

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

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

@[implicit_reducible]

instance Lean.Lsp.instBEqCompletionItem : BEq CompletionItem

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instHashableCompletionItem : Hashable CompletionItem

Equations

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

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

Equations

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

structure Lean.Lsp.CompletionList : Type

• isIncomplete : Bool
• items : Array CompletionItem

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCompletionList : FromJson CompletionList

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonCompletionList : ToJson CompletionList

Equations

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

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

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

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

@[implicit_reducible]

instance Lean.Lsp.instBEqCompletionIdentifier : BEq CompletionIdentifier

Equations

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

@[implicit_reducible]

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)

@[implicit_reducible]

instance Lean.Lsp.instToJsonCompletionIdentifier : ToJson CompletionIdentifier

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCompletionIdentifier : FromJson CompletionIdentifier

Equations

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

structure Lean.Lsp.ResolvableCompletionItemData : Type

• uri : DocumentUri
• pos : Position
• cPos? : Option Nat

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

• id? : Option CompletionIdentifier

@[implicit_reducible]

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

@[implicit_reducible]

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 { uri := 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)

@[implicit_reducible]

instance Lean.Lsp.instToJsonResolvableCompletionItemData : ToJson ResolvableCompletionItemData

Equations

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

@[implicit_reducible]

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)

@[implicit_reducible]

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.

@[implicit_reducible]

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.

@[implicit_reducible]

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.

@[implicit_reducible]

instance Lean.Lsp.instBEqResolvableCompletionItem : BEq ResolvableCompletionItem

Equations

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

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

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

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonResolvableCompletionList : FromJson ResolvableCompletionList

Equations

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

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

Equations

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

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

@[implicit_reducible]

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.

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonHover : ToJson Hover

Equations

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

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonHover : FromJson Hover

Equations

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

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

• textDocument : TextDocumentIdentifier
• position : Position

@[implicit_reducible]

instance Lean.Lsp.instFromJsonHoverParams : FromJson HoverParams

Equations

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

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

Equations

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

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

@[implicit_reducible]

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.

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDeclarationParams : FromJson DeclarationParams

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDefinitionParams : FromJson DefinitionParams

Equations

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

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

Equations

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

@[implicit_reducible]

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonTypeDefinitionParams : FromJson TypeDefinitionParams

Equations

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

@[implicit_reducible]

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonReferenceContext : FromJson ReferenceContext

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

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.

@[implicit_reducible]

instance Lean.Lsp.instToJsonReferenceParams : ToJson ReferenceParams

Equations

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

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

Equations

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

structure Lean.Lsp.WorkspaceSymbolParams : Type

• query : String

@[implicit_reducible]

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.

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDocumentHighlightParams : FromJson DocumentHighlightParams

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonDocumentHighlightParams : ToJson DocumentHighlightParams

Equations

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

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

inductive Lean.Lsp.DocumentHighlightKind : Type

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDocumentSymbolParams : FromJson DocumentSymbolParams

Equations

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

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

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonDocumentSymbolParams : ToJson DocumentSymbolParams

Equations

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

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instBEqSymbolKind : BEq SymbolKind

Equations

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

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

@[implicit_reducible]

instance Lean.Lsp.instHashableSymbolKind : Hashable SymbolKind

Equations

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

def Lean.Lsp.instInhabitedSymbolKind.default : SymbolKind

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instInhabitedSymbolKind : Inhabited SymbolKind

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSymbolKind : FromJson SymbolKind

Equations

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

@[implicit_reducible]

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)

@[implicit_reducible]

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.

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.

@[implicit_reducible]

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

Equations

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

inductive Lean.Lsp.DocumentSymbol : Type

• mk (sym : DocumentSymbolAux DocumentSymbol) : DocumentSymbol

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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)

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instHashableSymbolTag : Hashable SymbolTag

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSymbolTag : FromJson SymbolTag

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSymbolInformation : FromJson SymbolInformation

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonSymbolInformation : ToJson SymbolInformation

Equations

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

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

Equations

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

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

• textDocument : TextDocumentIdentifier
• position : Position

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCallHierarchyPrepareParams : FromJson CallHierarchyPrepareParams

Equations

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

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonCallHierarchyPrepareParams : ToJson CallHierarchyPrepareParams

Equations

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

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.

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCallHierarchyItem : FromJson CallHierarchyItem

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonCallHierarchyItem : ToJson CallHierarchyItem

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instBEqCallHierarchyItem : BEq CallHierarchyItem

Equations

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

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

@[implicit_reducible]

instance Lean.Lsp.instHashableCallHierarchyItem : Hashable CallHierarchyItem

Equations

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

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

Equations

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

def Lean.Lsp.instInhabitedCallHierarchyItem.default : CallHierarchyItem

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instInhabitedCallHierarchyItem : Inhabited CallHierarchyItem

Equations

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

structure Lean.Lsp.CallHierarchyIncomingCallsParams : Type

• item : CallHierarchyItem

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCallHierarchyIncomingCallsParams : FromJson CallHierarchyIncomingCallsParams

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonCallHierarchyIncomingCallsParams : ToJson CallHierarchyIncomingCallsParams

Equations

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

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

Equations

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

structure Lean.Lsp.CallHierarchyIncomingCall : Type

• from : CallHierarchyItem
• fromRanges : Array Range

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCallHierarchyIncomingCall : FromJson CallHierarchyIncomingCall

Equations

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

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

Equations

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

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonCallHierarchyIncomingCall : ToJson CallHierarchyIncomingCall

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instInhabitedCallHierarchyIncomingCall : Inhabited CallHierarchyIncomingCall

Equations

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

def Lean.Lsp.instInhabitedCallHierarchyIncomingCall.default : CallHierarchyIncomingCall

Equations

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

structure Lean.Lsp.CallHierarchyOutgoingCallsParams : Type

• item : CallHierarchyItem

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCallHierarchyOutgoingCallsParams : FromJson CallHierarchyOutgoingCallsParams

Equations

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

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

Equations

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

@[implicit_reducible]

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCallHierarchyOutgoingCall : FromJson CallHierarchyOutgoingCall

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonCallHierarchyOutgoingCall : ToJson CallHierarchyOutgoingCall

Equations

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

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonSemanticTokenType : ToJson SemanticTokenType

Equations

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

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"

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

Equations

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

@[implicit_reducible]

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)

@[implicit_reducible]

instance Lean.Lsp.instBEqSemanticTokenType : BEq SemanticTokenType

Equations

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

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

@[implicit_reducible]

instance Lean.Lsp.instHashableSemanticTokenType : Hashable SemanticTokenType

Equations

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

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"

@[implicit_reducible]

instance Lean.Lsp.instToJsonSemanticTokenModifier : ToJson SemanticTokenModifier

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSemanticTokenModifier : FromJson SemanticTokenModifier

Equations

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

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

Equations

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

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.

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSemanticTokensLegend : FromJson SemanticTokensLegend

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

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.

@[implicit_reducible]

instance Lean.Lsp.instToJsonSemanticTokensOptions : ToJson SemanticTokensOptions

Equations

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

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

structure Lean.Lsp.SemanticTokensParams : Type

• textDocument : TextDocumentIdentifier

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSemanticTokensParams : FromJson SemanticTokensParams

Equations

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

@[implicit_reducible]

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.

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSemanticTokensRangeParams : FromJson SemanticTokensRangeParams

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSemanticTokens : FromJson SemanticTokens

Equations

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

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

Equations

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

@[implicit_reducible]

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonFoldingRangeParams : FromJson FoldingRangeParams

Equations

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

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

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonFoldingRange : ToJson FoldingRange

Equations

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

structure Lean.Lsp.RenameOptions : Type

• prepareProvider : Bool

@[implicit_reducible]

instance Lean.Lsp.instFromJsonRenameOptions : FromJson RenameOptions

Equations

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

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

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonRenameOptions : ToJson RenameOptions

Equations

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

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

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

@[implicit_reducible]

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.

@[implicit_reducible]

instance Lean.Lsp.instToJsonRenameParams : ToJson RenameParams

Equations

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

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

Equations

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

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

• textDocument : TextDocumentIdentifier
• position : Position

@[implicit_reducible]

instance Lean.Lsp.instFromJsonPrepareRenameParams : FromJson PrepareRenameParams

Equations

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

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

Equations

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

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonPrepareRenameParams : ToJson PrepareRenameParams

Equations

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

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

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

@[implicit_reducible]

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.

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInlayHintTooltip : FromJson InlayHintTooltip

Equations

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

@[implicit_reducible]

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInlayHintLabelPart : FromJson InlayHintLabelPart

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonInlayHintLabelPart : ToJson InlayHintLabelPart

Equations

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

inductive Lean.Lsp.InlayHintLabel : Type

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInlayHintLabel : FromJson InlayHintLabel

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInlayHintKind : FromJson InlayHintKind

Equations

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

@[implicit_reducible]

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInlayHint : FromJson InlayHint

Equations

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

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

Equations

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

@[implicit_reducible]

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.

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInlayHintClientCapabilities : FromJson InlayHintClientCapabilities

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonInlayHintClientCapabilities : ToJson InlayHintClientCapabilities

Equations

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

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

• workDoneProgress : Bool
• resolveProvider? : Option Bool

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInlayHintOptions : FromJson InlayHintOptions

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonInlayHintOptions : ToJson InlayHintOptions

Equations

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

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

inductive Lean.Lsp.ParameterInformationLabel : Type

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonParameterInformationLabel : FromJson ParameterInformationLabel

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonParameterInformation : FromJson ParameterInformation

Equations

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

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

Equations

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

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSignatureInformation : FromJson SignatureInformation

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonSignatureInformation : ToJson SignatureInformation

Equations

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

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

Equations

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

structure Lean.Lsp.SignatureHelp : Type

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSignatureHelp : FromJson SignatureHelp

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonSignatureHelp : ToJson SignatureHelp

Equations

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

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

Equations

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

inductive Lean.Lsp.SignatureHelpTriggerKind : Type

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSignatureHelpTriggerKind : FromJson SignatureHelpTriggerKind

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

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.

@[implicit_reducible]

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.

@[implicit_reducible]

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.

@[implicit_reducible]

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)

@[implicit_reducible]

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.

@[implicit_reducible]

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.

structure Lean.Lsp.DocumentColorParamsextends Lean.Lsp.WorkDoneProgressParams, Lean.Lsp.PartialResultParams : Type

• workDoneToken? : Option ProgressToken
• partialResultToken? : Option ProgressToken
• textDocument : TextDocumentIdentifier

def Lean.Lsp.instFromJsonDocumentColorParams.fromJson : Json → Except String DocumentColorParams

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDocumentColorParams : FromJson DocumentColorParams

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonDocumentColorParams : ToJson DocumentColorParams

Equations

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

def Lean.Lsp.instToJsonDocumentColorParams.toJson : DocumentColorParams → Json

Equations

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

structure Lean.Lsp.Color : Type

• red : Float
• green : Float
• blue : Float
• alpha : Float

def Lean.Lsp.instFromJsonColor.fromJson : Json → Except String Color

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonColor : FromJson Color

Equations

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

def Lean.Lsp.instToJsonColor.toJson : Color → Json

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonColor : ToJson Color

Equations

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

structure Lean.Lsp.ColorInformation : Type

• range : Range
• color : Color

def Lean.Lsp.instFromJsonColorInformation.fromJson : Json → Except String ColorInformation

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonColorInformation : FromJson ColorInformation

Equations

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

def Lean.Lsp.instToJsonColorInformation.toJson : ColorInformation → Json

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonColorInformation : ToJson ColorInformation

Equations

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

structure Lean.Lsp.DocumentColorOptionsextends Lean.Lsp.WorkDoneProgressOptions : Type

• workDoneProgress : Bool

def Lean.Lsp.instFromJsonDocumentColorOptions.fromJson : Json → Except String DocumentColorOptions

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDocumentColorOptions : FromJson DocumentColorOptions

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonDocumentColorOptions : ToJson DocumentColorOptions

Equations

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

def Lean.Lsp.instToJsonDocumentColorOptions.toJson : DocumentColorOptions → Json

Equations

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