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.
We perform two passes. In the first-pass, we only consider arguments that are not indices. In the second pass, we consider them.
TODO: explore whether there are better solutions, and whether there are other ways to break the heuristic used for creating the smart unfolding auxiliary definition.
Equations
- One or more equations did not get rendered due to their size.
partial def
Lean.Elab.Structural.findRecArg.go
{α : Type}
(numFixed : Nat)
(xs : Array Lean.Expr)
(k : Lean.Elab.Structural.RecArgInfo → Lean.Elab.Structural.M α)
(indices : Lean.FVarIdSet)
(i : Nat)
(firstPass : Bool)
: