def Lean.Elab.Structural.withRecArgInfo {α : Type} (numFixed : Nat) (xs : Array Lean.Expr) (i : Nat) (k : Lean.Elab.Structural.RecArgInfo → Lean.Elab.Structural.M α) : Lean.Elab.Structural.M α

Pass to k the RecArgInfo for the ith 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.

def Lean.Elab.Structural.findRecArg {α : Type} (numFixed : Nat) (xs : Array Lean.Expr) (k : Lean.Elab.Structural.RecArgInfo → Lean.Elab.Structural.M α) : 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.