A (potentially recursive) definition. The elaborator converts it into Kernel definitions using many different strategies.
- ref : Lean.Syntax
- kind : Lean.Elab.DefKind
- modifiers : Lean.Elab.Modifiers
- declName : Lake.Name
- type : Lean.Expr
- value : Lean.Expr
Eliminate recursive application annotations containing syntax. These annotations are used by the well-founded recursion module to produce better error messages.
- One or more equations did not get rendered due to their size.