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 : Lean.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 (counted including fixed prefix) of the argument we are recursing on

• indicesPos : Array Nat

  position (counted including fixed prefix) of the indices of the inductive datatype 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

instance Lean.Elab.Structural.instReprRecArgInfo : Repr Lean.Elab.Structural.RecArgInfo

Equations

• Lean.Elab.Structural.instReprRecArgInfo = { reprPrec := Lean.Elab.Structural.reprRecArgInfo✝ }

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.

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

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