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

Equations

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

def Lean.Elab.Command.expandNamespacedDeclaration : Lean.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.

Equations

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

def Lean.Elab.Command.elabDeclaration : Lean.Elab.Command.CommandElab

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

Find the common namespace for the given names. Example:

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

Equations

• Lean.Elab.Command.findCommonPrefix [] = Lean.Name.anonymous
• Lean.Elab.Command.findCommonPrefix (n' :: ns_2) = Lean.Elab.Command.findCommonPrefix.go n' ns_2

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

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

Equations

• Lean.Elab.Command.findCommonPrefix.findCommon (a :: as_2) (b :: bs_2) = if (a == b) = true then a ++ Lean.Elab.Command.findCommonPrefix.findCommon as_2 bs_2 else Lean.Name.anonymous
• Lean.Elab.Command.findCommonPrefix.findCommon as bs = Lean.Name.anonymous

def Lean.Elab.Command.expandMutualNamespace : Lean.Macro

Equations

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

def Lean.Elab.Command.expandMutualElement : Lean.Macro

Equations

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

def Lean.Elab.Command.expandMutualPreamble : Lean.Macro

def Lean.Elab.Command.elabMutual : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabAttr : Lean.Elab.Command.CommandElab

def Lean.Elab.Command.elabInitialize : Lean.Elab.Command.CommandElab