structure Lean.Elab.Structural.RecArgInfo : Type

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

• indGroupInst : Lean.Elab.Structural.IndGroupInst

  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

instance Lean.Elab.Structural.instInhabitedRecArgInfo : Inhabited Lean.Elab.Structural.RecArgInfo

Equations

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

def Lean.Elab.Structural.RecArgInfo.pickIndicesMajor (info : Lean.Elab.Structural.RecArgInfo) (xs : Array Lean.Expr) : Array Lean.Expr × Array Lean.Expr

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.

def Lean.Elab.Structural.RecArgInfo.indName! (info : Lean.Elab.Structural.RecArgInfo) : Lake.Name

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

Equations

• info.indName! = info.indGroupInst.all[info.indIdx]!