Module Inductive

Fetching information in the environment about an inductive type. Raises an anomaly if the inductive type is not found.

Functions to build standard types related to inductive

The constr array is the types of the arguments to a template polymorphic inductive.

Return constructor types in normal form

Return constructor types in user form

Turns a constructor type recursively referring to inductive types into the same constructor type referring instead to a context made from the abstract declaration of the inductive types (e.g. turns nat->nat into mkArrowR (Rel 1) (Rel 2)); takes as arguments the number of inductive types in the block and the name of the block

Given a pattern-matching represented compactly, expands it so as to produce lambda and let abstractions in front of the return clause and the pattern branches.

Dual operation of the above. Fails if the return clause or branch has not the expected form.

instantiate_context u subst nas ctx applies both u and subst to ctx while replacing names using nas (order reversed). In particular, assumes that ctx and nas have the same length.

type_case_branches env (I,args) (p:A) c computes useful types about the following Cases expression: <p>Cases (c :: (I args)) of b1..bn end It computes the type of every branch (pattern variables are introduced by products), the type for the whole expression, and the universe constraints generated.

Return the arity of an inductive type

Check a case_info actually correspond to a Case expression on the given inductive type.

is_primitive_positive_container env c tells if the constant c is registered as a primitive type that can be seen as a container where the occurrences of its parameters are positive, in which case the positivity and guard conditions are extended to allow inductive types to nest their subterms in these containers.

When chk is false, the guard condition is not actually checked.