Module Reduction

Builds an application node, reducing beta redexes it may produce.

Builds an application node, reducing beta redexes it may produce.

Builds an application node, reducing beta redexe it may produce.

Pseudo-reduction rule Prod(x,A,B) a --> Bx\a

In hnf_prod_applist_decls n c args, c is supposed to (whd-)reduce to the form ∀Γ.t with Γ of length n and possibly with let-ins; it returns t with the assumptions of Γ instantiated by args and the local definitions of Γ expanded.

Compatibility alias for Term.lambda_appvect_decls

This is typically the function to use to extract the context of a Fix not already in normal form up to and including the decreasing argument, counting as many lambda's as given by the decreasing index + 1