Module Declarations

Inductive sort with abstracted universes.

Template_defaults qualities are all QType. Also the universes are all levels so we can use Instance.

a global assumption

or a transparent global definition

or an opaque global definition

or a primitive operation

or a symbol

If false then fixed points and co-fixed points are assumed to be total.

If false then inductive types are assumed positive and co-inductive types are assumed productive.

If false universe constraints are not checked

Unfolding strategies for conversion

Use by-need reduction algorithm

If false, all VM conversions fall back to interpreted ones

If false, all native conversions fall back to VM ones

The universe of an inductive type must be above that of its indices.

Predicativity of the Set universe.

If false, error when encountering SProp.

Allow definitional UIP (breaks termination)

younger hyp at top

bool is for unfold_fix in symbols

The typing options which were used for type-checking.

A sort polymorphic inductive I@{...|...|...} : ... -> Type@{ s|...} is squashed at a given instantiation if any quality in the list is not smaller than s.

NB: if s is a variable SometimesSquashed contains SProp ie non ground instantiations are squashed.

Name of the type: Ii

Arity context of Ii. It includes the context of parameters, that is, it has the form paramdecls, realdecls_i such that Ui (see above) is forall realdecls_i, si for some sort si and such that Ii has thus type forall paramdecls, forall realdecls_i, si. The context itself is represented internally as a list in reverse order [realdecl_i{r_i};...;realdecl_i1;paramdecl_m;...;paramdecl_1].

Arity sort

Original user arity, convertible to mkArity (mind_arity_ctxt, mind_sort). As such it contains the parameters. (not necessarily a syntactic arity, eg relation A instead of A -> A -> Prop)

Names of the constructors: cij

Types of the constructors with parameters: forall params, Tij, where the recursive occurrences of the inductive types in Tij (i.e. in the type of the j-th constructor of the i-th types of the block a shown above) have the form Ind ((mind,0),u), ..., Ind ((mind,n-1),u) for u the canonical abstract instance associated to mind_universes and mind the name to which the inductive block is bound in the environment.

Number of expected real arguments of the type (no let, no params)

Length of realargs context (with let, no params)

Is elimination restricted to the inductive's sort?

Head normalized constructor types so that their conclusion exposes the inductive type. It includes the parameters, i.e. each component of the array has the form (decls_ij, Ii params realargs_ij) where decls_ij is the concatenation of the context of parameters (possibly with let-ins) and of the arguments of the constructor (possibly with let-ins). This context is internally represented as a list [cstrdecl_ij{q_ij};...;cstrdecl_ij1;paramdecl_m;...;paramdecl_1] such that the constructor in fine has type forall paramdecls, forall cstrdecls_ij, Ii params realargs_ij with params referring to the assumptions of paramdecls and realargs_ij being the "indices" specific to the constructor.

Number of expected proper arguments of the constructors (w/o params)

Length of the signature of the constructors (with let, w/o params)

Signature of recursive arguments in the constructors

number of constant constructor

number of no constant constructor

= inductive

= coinductive

= non-recursive, like in "Record" definitions

The component of the mutual inductive block

The record information

Whether the type is inductive, coinductive or non-recursive

Number of types in the block

Section hypotheses on which the block depends

Section polymorphic universes.

Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in)

Number of recursively uniform (i.e. ordinary) parameters

The context of parameters (includes let-in declaration)

Information about monomorphic/polymorphic/cumulative inductives and their universes

Variance info, None when non-cumulative.

Variance info for section polymorphic universes. None outside sections. The final variance once all sections are discharged is mind_sec_variance ++ mind_variance.

allow pattern-matching: Some true ok, Some false blocked

typing flags at the time of the inductive creation