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

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

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

def Lean.Elab.Command.getTerminationHints (stx : Lean.Syntax) : Lean.Elab.TerminationHints

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

def Lean.Elab.Command.findCommonPrefix (ns : List Lake.Name) : Lake.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 : Lake.Name) (ns : List Lake.Name) : Lake.Name

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Command.findCommonPrefix.go Lean.Name.anonymous ns = Lean.Name.anonymous
• Lean.Elab.Command.findCommonPrefix.go n [] = n

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

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

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

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

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

def Lean.Elab.Command.expandInitialize : Lean.Macro