def Lean.Elab.Command.elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit

def Lean.Elab.Command.expandNamespacedDeclaration : Macro

Macro that expands a declaration with a complex name into an explicit namespace block. Implementing this step as a macro means that reuse checking is handled by elabCommand.

def Lean.Elab.Command.elabDeclaration : CommandElab

def Lean.Elab.Command.findCommonPrefix (ns : List Name) : Name

Find the common namespace for the given names. Example:

findCommonPrefix [`Lean.Elab.eval, `Lean.mkConst, `Lean.Elab.Tactic.evalTactic]
-- `Lean

def Lean.Elab.Command.findCommonPrefix.go (n : Name) (ns : List Name) : Name

def Lean.Elab.Command.findCommonPrefix.findCommon (as bs : List Name) : Name

def Lean.Elab.Command.expandMutualNamespace : Macro

def Lean.Elab.Command.expandMutualElement : Macro

def Lean.Elab.Command.expandMutualPreamble : Macro

def Lean.Elab.Command.elabMutual : CommandElab

def Lean.Elab.Command.elabAttr : CommandElab

def Lean.Elab.Command.elabInitialize : CommandElab