partial def Lean.Elab.Structural.searchPProd {α : Type} (e F : Expr) (k : Expr → Expr → MetaM α) : MetaM α

def Lean.Elab.Structural.toBelow (below : Expr) (numIndParams : Nat) (positions : Positions) (fnIndex : Nat) (recArg : Expr) : MetaM Expr

below is a free variable with type of the form I.below indParams motive indices major, where I is the name of an inductive datatype.

For example, when trying to show that the following function terminates using structural recursion

def addAdjacent : List Nat → List Nat
| []       => []
| [a]      => [a]
| a::b::as => (a+b) :: addAdjacent as

when we are visiting addAdjacent as at replaceRecApps, below has type @List.below Nat (fun (x : List Nat) => List Nat) (a::b::as) The motive fun (x : List Nat) => List Nat depends on the actual function we are trying to compute. So, we first replace it with a fresh variable C at withBelowDict. Recall that brecOn implements course-of-values recursion, and below can be viewed as a dictionary of the "previous values". We search this dictionary using the auxiliary function toBelowAux. The dictionary is built using the PProd (And for inductive predicates). We keep searching it until we find C recArg, where C is the auxiliary fresh variable created at withBelowDict.

def Lean.Elab.Structural.mkBRecOnMotive (recArgInfo : RecArgInfo) (value : Expr) : M Expr

Calculates the .brecOn motive corresponding to one structural recursive function. The value is the function with (only) the fixed parameters moved into the context.

def Lean.Elab.Structural.mkBRecOnF (recArgInfos : Array RecArgInfo) (positions : Positions) (recArgInfo : RecArgInfo) (value FType : Expr) : M Expr

Calculates the .brecOn functional argument corresponding to one structural recursive function. The value is the function with (only) the fixed parameters moved into the context, The FType is the expected type of the argument. The recArgInfos is used to transform the body of the function to replace recursive calls with uses of the below induction hypothesis.

def Lean.Elab.Structural.mkBRecOnConst (recArgInfos : Array RecArgInfo) (positions : Positions) (motives : Array Expr) (isIndPred : Bool) : MetaM (Nat → Expr)

Given the motives, pass the right universe levels, the parameters, and the motives. It was already checked earlier in checkCodomainsLevel that the functions live in the same universe.

def Lean.Elab.Structural.inferBRecOnFTypes (recArgInfos : Array RecArgInfo) (positions : Positions) (brecOnConst : Nat → Expr) : MetaM (Array Expr)

Given the recArgInfos and the motives, infer the types of the F arguments to the .brecOn combinators. This assumes that all .brecOn functions of a mutual inductive have the same structure.

It also undoes the permutation and packing done by packMotives

def Lean.Elab.Structural.mkBRecOnApp (positions : Positions) (fnIdx : Nat) (brecOnConst : Nat → Expr) (packedFArgs funTypes : Array Expr) (recArgInfo : RecArgInfo) (value : Expr) : MetaM Expr

Completes the .brecOn for the given function. The value is the function with (only) the fixed parameters moved into the context.