def Lean.Elab.Command.aux_def : Lean.ParserDescr

Declares an auxiliary definition with an automatically generated name. For example, aux_def foo : Nat := 42 creates a definition with an internal, unused name based on the suggestion foo.

Equations

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

def Lean.Elab.Command.elabAuxDef : Lean.Elab.Command.CommandElab

Equations

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