ink

def Lean.Meta.collectPrivateIn {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (n : Lean.Name) (set : optParam Lean.NameSet Lean.NameSet.empty) : m Lean.NameSet

Collects the names of private declarations referenced in definition n.

Equations

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

ink

def Lean.Environment.moduleIdxForModule? (env : Lean.Environment) (mod : Lean.Name) : Option Lean.ModuleIdx

Get the module index given a module name.

Equations

• Lean.Environment.moduleIdxForModule? env mod = Option.map (fun idx => idx.val) (Array.indexOf? (Lean.Environment.allImportedModuleNames env) mod)

ink

instance Lean.instDecidableEqModuleIdx : DecidableEq Lean.ModuleIdx

Equations

• Lean.instDecidableEqModuleIdx = instDecidableEqNat

ink

def Lean.Environment.declsInModuleIdx (env : Lean.Environment) (idx : Lean.ModuleIdx) : List Lean.Name

Get the list of declarations in a module (referenced by index).

Equations

• Lean.Environment.declsInModuleIdx env idx = Lean.HashMap.fold (fun acc n i => if i = idx then n :: acc else acc) [] env.const2ModIdx

ink

def Lean.Elab.addModuleInfo {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] (stx : Lean.Ident) : m Unit

Add info to the info tree corresponding to a module name.

Equations

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

ink

def Lean.Elab.Command.elabOpenPrivateLike (ids : Array Lean.Ident) (tgts : Option (Array Lean.Ident)) (mods : Option (Array Lean.Ident)) (f : Lean.Name → Lean.Name → Lean.Name → Lean.Elab.Command.CommandElabM Lean.Name) : Lean.Elab.Command.CommandElabM Unit

Core elaborator for open private and export private.

Equations

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

ink

def Lean.Elab.Command.openPrivate : Lean.ParserDescr

The command open private a b c in foo bar will look for private definitions named a, b, c in declarations foo and bar and open them in the current scope. This does not make the definitions public, but rather makes them accessible in the current section by the short name a instead of the (unnameable) internal name for the private declaration, something like _private.Other.Module.0.Other.Namespace.foo.a, which cannot be typed directly because of the 0 name component.

It is also possible to specify the module instead with open private a b c from Other.Module.

Equations

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

ink

def Lean.Elab.Command.elabOpenPrivate : Lean.Elab.Command.CommandElab

Elaborator for open private.

Equations

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

ink

def Lean.Elab.Command.exportPrivate : Lean.ParserDescr

The command export private a b c in foo bar is similar to open private, but instead of opening them in the current scope it will create public aliases to the private definition. The definition will exist at exactly the original location and name, as if the private keyword was not used originally.

It will also open the newly created alias definition under the provided short name, like open private. It is also possible to specify the module instead with export private a b c from Other.Module.

Equations

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

ink

def Lean.Elab.Command.elabExportPrivate : Lean.Elab.Command.CommandElab

Elaborator for export private.

Equations

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