def
Lean.Elab.Structural.withRecArgInfo
{α : Type}
(numFixed : Nat)
(xs : Array Lean.Expr)
(i : Nat)
(k : Lean.Elab.Structural.RecArgInfo → Lean.Elab.Structural.M α)
:
Pass to k
the RecArgInfo
for the i
th parameter in the parameter list xs
. This performs
various sanity checks on the argument (is it even an inductive type etc).
Also wraps all errors in a common “argument cannot be used” header
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Elab.Structural.findRecArg
{α : Type}
(numFixed : Nat)
(xs : Array Lean.Expr)
(k : Lean.Elab.Structural.RecArgInfo → Lean.Elab.Structural.M α)
:
Try to find an argument that is structurally smaller in every recursive application.
We use this argument to justify termination using the auxiliary brecOn
construction.
We give preference for arguments that are not indices of inductive types of other arguments. See issue #837 for an example where we can show termination using the index of an inductive family, but we don't get the desired definitional equalities.
Equations
- One or more equations did not get rendered due to their size.