Documentation

Lean.Elab.PreDefinition.Structural.RecArgInfo

Information about the argument of interest of a structurally recursive function.

The Exprs in this data structure expect the fixedParams to be in scope, but not the other parameters of the function. This ensures that this data structure makes sense in the other functions of a mutually recursive group.

  • fnName : Lake.Name

    the name of the recursive function

  • numFixed : Nat

    the fixed prefix of arguments of the function we are trying to justify termination using structural recursion.

  • recArgPos : Nat

    position of the argument (counted including fixed prefix) we are recursing on

  • indicesPos : Array Nat

    position of the indices (counted including fixed prefix) of the inductive datatype indices we are recursing on

  • The inductive group (with parameters) of the argument's type

  • indIdx : Nat

    index of the inductive datatype of the argument we are recursing on. If < indAll.all, a normal data type, else an auxiliary data type due to nested recursion

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

    If xs are the parameters of the functions (excluding fixed prefix), partitions them into indices and major arguments, and other parameters.

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

      Name of the recursive data type. Assumes that it is not one of the auxiliary ones.

      Equations
      • info.indName! = info.indGroupInst.all[info.indIdx]!
      Instances For