def Lean.Elab.Structural.withFunTypes {α : Type} (values : Array Expr) (k : Array Expr → MetaM α) : MetaM α

Turns fun a b => x into let funType := fun a b => α (where x : α). The continuation is the called with all funTypes corresponding to the values.

Equations

• Lean.Elab.Structural.withFunTypes values k = Lean.Elab.Structural.withFunTypes.go✝ values k 0 #[]

def Lean.Elab.Structural.mkIndPredBRecOnMotive (recArgInfo : RecArgInfo) (value funType : Expr) : MetaM 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.mkIndPredBRecOnF (recArgInfos : Array RecArgInfo) (positions : Positions) (recArgInfo : RecArgInfo) (value FType : Expr) (params : Array Expr) : MetaM (Expr × Array (MetaM Unit))

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. Returns the functional argument and any matchers that were created as side effects. The matchers are created inside withoutModifyingEnv and need to be replayed afterwards.

Equations

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