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.elabInductive (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) : Lean.Elab.Command.CommandElabM Unit

Equations

• Lean.Elab.Command.elabInductive modifiers stx = do let v ← Lean.Elab.Command.inductiveSyntaxToView modifiers stx Lean.Elab.Command.elabInductiveViews #[v]

def Lean.Elab.Command.elabClassInductive (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

Equations

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

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

Equations

• Lean.Elab.Command.findCommonPrefix ns = match ns with | [] => Lean.Name.anonymous | n :: ns => Lean.Elab.Command.findCommonPrefix.go n ns

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

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

Equations

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

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

Equations

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

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

Equations

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