inductive Lean.Server.GoToKind : Type

• declaration : GoToKind
• definition : GoToKind
• type : GoToKind

instance Lean.Server.instBEqGoToKind : BEq GoToKind

Equations

• Lean.Server.instBEqGoToKind = { beq := Lean.Server.beqGoToKind✝ }

instance Lean.Server.instToJsonGoToKind : ToJson GoToKind

Equations

• Lean.Server.instToJsonGoToKind = { toJson := Lean.Server.toJsonGoToKind✝ }

instance Lean.Server.instFromJsonGoToKind : FromJson GoToKind

Equations

• Lean.Server.instFromJsonGoToKind = { fromJson? := Lean.Server.fromJsonGoToKind✝ }

def Lean.Server.locationLinksFromDecl (uri : Lsp.DocumentUri) (n : Name) (originRange? : Option Lsp.Range) : MetaM (Array Lsp.LocationLink)

Equations

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