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.