Documentation

Lean.Server.GoTo

inductive Lean.Server.GoToKind:

Type

instance Lean.Server.instBEqGoToKind:

BEq Lean.Server.GoToKind

Equations

Lean.Server.instBEqGoToKind = { beq := [anonymous] }

instance Lean.Server.instToJsonGoToKind:

Lean.ToJson Lean.Server.GoToKind

Equations

Lean.Server.instToJsonGoToKind = { toJson := [anonymous] }

instance Lean.Server.instFromJsonGoToKind:

Lean.FromJson Lean.Server.GoToKind

Equations

Lean.Server.instFromJsonGoToKind = { fromJson? := [anonymous] }

def Lean.Server.documentUriFromModule (srcSearchPath : Lean.SearchPath) (modName : Lean.Name) :

IO (Option Lean.Lsp.DocumentUri)

Equations

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

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