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

def Lean.Elab.Structural.mkBRecOnMotive (recArgInfo : Lean.Elab.Structural.RecArgInfo) (value : Lean.Expr) : Lean.Elab.Structural.M Lean.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.

Equations

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

def Lean.Elab.Structural.mkBRecOnF (recArgInfos : Array Lean.Elab.Structural.RecArgInfo) (positions : Lean.Elab.Structural.Positions) (recArgInfo : Lean.Elab.Structural.RecArgInfo) (value : Lean.Expr) (FType : Lean.Expr) : Lean.Elab.Structural.M Lean.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.

Equations

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

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

Given the motives, figures out whether to use .brecOn or .binductionOn, 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.

Equations

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

def Lean.Elab.Structural.inferBRecOnFTypes (recArgInfos : Array Lean.Elab.Structural.RecArgInfo) (positions : Lean.Elab.Structural.Positions) (brecOnConst : Nat → Lean.Expr) : Lean.MetaM (Array Lean.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

Equations

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

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

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

Equations

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