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

    fixedParams : Array Lean.Expr
  • recursion arguments

  • 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 : Array Nat
  • 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 : List Lean.Level
  • inductive datatype parameters of the argument we are recursing on

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

    indIndices : Array Lean.Expr
  • true if we are recursing over a reflexive inductive datatype

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

    indPred : Bool
Instances For
    • 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.

      addMatchers : Array (Lean.MetaM Unit)
    Instances For

      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.

      • One or more equations did not get rendered due to their size.