Documentation

Lean.Elab.PreDefinition.Structural.RecArgInfo

source
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 fixed parameters 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 : Name

    the name of the recursive function

  • fixedParamPerm : FixedParamPerm

    Information which arguments are fixed

  • recArgPos : Nat

    position of the argument we are recursing on, among all parameters

  • indicesPos : Array Nat

    position of the indices of the inductive datatype we are recursing on, among all parameters

  • indGroupInst : 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

Instances For
source
instance Lean.Elab.Structural.instInhabitedRecArgInfo :
Inhabited RecArgInfo
Equations
  • One or more equations did not get rendered due to their size.
source
instance Lean.Elab.Structural.instReprRecArgInfo :
Repr RecArgInfo
Equations
source
def Lean.Elab.Structural.RecArgInfo.indicesAndRecArgPos (info : RecArgInfo) :
Array Nat

position of the argument and its indices we are recursing on, among all parameters

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

If xs are the varing parameters of the functions, partitions them into indices and major arguments, and other parameters.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Structural.RecArgInfo.indName! (info : RecArgInfo) :
Name

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

Equations