def Lean.Name.findHome (n : Name) (env : Option Environment) : CoreM NameSet

Find locations as high as possible in the import hierarchy where the named declaration could live.

def getModuleUri (modName : Lean.Name) : Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.DocumentUri)

Tries to resolve the module modName to a source file URI. This has to be done in the Lean server since the Environment does not keep track of source URIs.

Equations

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

structure GoToModuleLinkProps : Type

• modName : Lean.Name

instance instRpcEncodableGoToModuleLinkProps : Lean.Server.RpcEncodable GoToModuleLinkProps

Equations

• instRpcEncodableGoToModuleLinkProps = { rpcEncode := instRpcEncodableGoToModuleLinkProps.enc✝, rpcDecode := instRpcEncodableGoToModuleLinkProps.dec✝ }

def GoToModuleLink : Lean.Widget.Module

When clicked, this widget component jumps to the source of the module modName, assuming a source URI can be found for the module.

Equations

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

def «command#find_home!_» : Lean.ParserDescr

Find locations as high as possible in the import hierarchy where the named declaration could live. Using #find_home! will forcefully remove the current file. Note that this works best if used in a file with import Mathlib.

The current file could still be the only suggestion, even using #find_home! lemma. The reason is that #find_home! scans the import graph below the current file, selects all the files containing declarations appearing in lemma, excluding the current file itself and looks for all least upper bounds of such files.

For a simple example, if lemma is in a file importing only A.lean and B.lean and uses one lemma from each, then #find_home! lemma returns the current file.

Equations

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