- pos : Nat
ysof the argument we are recursing on
ysof the inductive datatype indices we are recursing on
- indName : Lake.Name
inductive datatype name of the argument we are recursing on
inductive datatype universe levels of the argument we are recursing on
inductive datatype parameters of the argument we are recursing on
inductive datatype indices of the argument we are recursing on, it is equal to
indicesPos.map fun i => ys.get! i
- reflexive : Bool
true if we are recursing over a reflexive inductive datatype
- indPred : Bool
true if the type is an inductive predicate
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
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.
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.