inductive Lean.Server.GoToKind : Type

• declaration: Lean.Server.GoToKind
• definition: Lean.Server.GoToKind
• type: Lean.Server.GoToKind

instance Lean.Server.instBEqGoToKind : BEq Lean.Server.GoToKind

Equations

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

instance Lean.Server.instToJsonGoToKind : Lean.ToJson Lean.Server.GoToKind

Equations

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

instance Lean.Server.instFromJsonGoToKind : Lean.FromJson Lean.Server.GoToKind

Equations

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

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

Finds the module name corresponding to uri in srcSearchPath.

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

Equations

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