# Documentation

Lean.Elab.PreDefinition.Structural.Basic

• fixedParams ++ ys are the arguments of the function we are trying to justify termination using structural recursion.

fixedParams :
• recursion arguments

ys :
• position in ys of the argument we are recursing on

pos : Nat
• position in ys of the inductive datatype indices we are recursing on

indicesPos :
• inductive datatype name of the argument we are recursing on

indName : Lean.Name
• inductive datatype universe levels of the argument we are recursing on

indLevels :
• inductive datatype parameters of the argument we are recursing on

indParams :
• inductive datatype indices of the argument we are recursing on, it is equal to indicesPos.map fun i => ys.get! i

indIndices :
• true if we are recursing over a reflexive inductive datatype

reflexive : Bool
• true if the type is an inductive predicate

indPred : Bool
Instances For
Equations
• As part of the inductive predicates case, we keep adding more and more discriminants from the local context and build up a bigger matcher application until we reach a fixed point. As a side-effect, this creates matchers. Here we capture all these side-effects, because the construction rolls back any changes done to the environment and the side-effects need to be replayed.

Return true iff e contains an application recFnName .. t .. where the term t is the argument we are trying to recurse on, and it contains loose bound variables.
We use this test to decide whether we should process a matcher-application as a regular applicaton or not. That is, whether we should push the below argument should be affected by the matcher or not. If e does not contain an application of the form recFnName .. t .., then we know the recursion doesn't depend on any pattern variable in this matcher.