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.documentUriFromModule (srcSearchPath : SearchPath) (modName : Name) : IO (Option Lsp.DocumentUri)

Finds the URI corresponding to modName in searchSearchPath.

Equations

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

def Lean.Server.moduleFromDocumentUri (srcSearchPath : SearchPath) (uri : Lsp.DocumentUri) : IO (Option Name)

Finds the module name corresponding to uri in srcSearchPath.

def Lean.Server.locationLinksFromDecl (srcSearchPath : SearchPath) (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.