• fixedParams : Array Lean.Expr

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

  • recursion arguments

  • pos : Nat

    position in ys of the argument we are recursing on

  • indicesPos : Array Nat

    position in ys of the inductive datatype indices we are recursing on

  • indName : Lake.Name

    inductive datatype name of the argument we are recursing on

  • indLevels : List Lean.Level

    inductive datatype universe levels of the argument we are recursing on

  • indParams : Array Lean.Expr

    inductive datatype parameters of the argument we are recursing on

  • indIndices : Array Lean.Expr

    inductive datatype indices of the argument we are recursing on, it is equal to 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

Instances For
    • addMatchers : Array (Lean.MetaM Unit)

      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.

    Instances For
      @[inline, reducible]
      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.

        Instances For