Module Reductionops

Machinery to customize the behavior of the reduction

Same as (strong whd_beta[delta][iota]), but much faster on big terms

Removes cast and put into applicative form

Decompose a type into a sequence of products and a non-product conclusion in head normal form, using head-reduction to expose the products

Decompose a term into a sequence of lambdas and a non-lambda conclusion in head normal form, using head-reduction to expose the lambdas

Decompose a type into a context and a conclusion not starting with a product or let-in, using head-reduction without zeta to expose the products and let-ins

Like whd_decompose_prod but limited at n products; raises Invalid_argument if not enough products

Like whd_decompose_lambda but limited at n lambdas; raises Invalid_argument if not enough lambdas

Decompose an arity reducing let-ins; Raises Reduction.NotArity

Decompose an arity preserving let-ins; Raises Reduction.NotArity

Raises Reduction.NotArity

Extract the n first products of a type, preserving let-ins (but not counting them); Raises Invalid_argument if not enough products

Extract the n first products of a type, counting and preserving let-ins; Raises Invalid_argument if not enough products or let-ins

Extract the n first lambdas of a term, preserving let-ins (but not counting them); Raises Invalid_argument if not enough lambdas

Querying the kernel conversion oracle: opaque/transparent constants

check_conv Checks universe constraints only. pb defaults to CUMUL and ts to a full transparent state.

infer_conv Adds necessary universe constraints to the evar map. pb defaults to CUMUL and ts to a full transparent state.

• raises UniverseInconsistency

  iff catch_incon is set to false, otherwise returns false in that case.

Conversion with inference of universe constraints

infer_conv_gen behaves like infer_conv but is parametrized by a conversion function. Used to pretype vm and native casts.

Typeops.check_hyps_inclusion but handles evars in the environment.