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

Equations

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

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.

Equations

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

def Lean.Elab.Command.elabDeclaration : CommandElab

Equations

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

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

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 : Name) (ns : List Name) : Name

Equations

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

def Lean.Elab.Command.findCommonPrefix.findCommon (as bs : List Name) : 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 : Macro

Equations

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

def Lean.Elab.Command.expandMutualElement : Macro

Equations

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

def Lean.Elab.Command.expandMutualPreamble : Macro

Equations

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

def Lean.Elab.Command.elabMutual : CommandElab

Equations

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

def Lean.Elab.Command.elabAttr : CommandElab

Equations

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

def Lean.Elab.Command.elabInitialize : CommandElab

Equations

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