# Module `Declarations`

###### Representation of constants (Definition/Axiom)

`type template_arity`

`=`

`{`

`template_level : Sorts.t;`

`}`

`type template_universes`

`=`

`{`

`template_param_levels : Univ.Level.t option list;`

`template_context : Univ.ContextSet.t;`

`}`

`type ('a, 'b) declaration_arity`

`=`

`|`

`RegularArity of 'a`

`|`

`TemplateArity of 'b`

`type ('a, 'opaque) constant_def`

`=`

`|`

`Undef of inline`

a global assumption

`|`

`Def of 'a`

or a transparent global definition

`|`

`OpaqueDef of 'opaque`

or an opaque global definition

`|`

`Primitive of CPrimitives.t`

or a primitive operation

`type universes`

`=`

`|`

`Monomorphic`

`|`

`Polymorphic of UVars.AbstractContext.t`

`type typing_flags`

`=`

`{`

`check_guarded : bool;`

If

`false`

then fixed points and co-fixed points are assumed to be total.`check_positive : bool;`

If

`false`

then inductive types are assumed positive and co-inductive types are assumed productive.`check_universes : bool;`

If

`false`

universe constraints are not checked`conv_oracle : Conv_oracle.oracle;`

Unfolding strategies for conversion

`share_reduction : bool;`

Use by-need reduction algorithm

`enable_VM : bool;`

If

`false`

, all VM conversions fall back to interpreted ones`enable_native_compiler : bool;`

If

`false`

, all native conversions fall back to VM ones`indices_matter : bool;`

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

`impredicative_set : bool;`

Predicativity of the

`Set`

universe.`sprop_allowed : bool;`

If

`false`

, error when encountering`SProp`

.`allow_uip : bool;`

Allow definitional UIP (breaks termination)

`}`

The

`typing_flags`

are instructions to the type-checker which modify its behaviour. The typing flags used in the type-checking of a constant are tracked in their`constant_body`

so that they can be displayed to the user.

###### Representation of definitions/assumptions in the kernel

`type 'opaque pconstant_body`

`=`

`{`

`const_hyps : Constr.named_context;`

younger hyp at top

`const_univ_hyps : UVars.Instance.t;`

`const_body : (Constr.t, 'opaque) constant_def;`

`const_type : Constr.types;`

`const_relevance : Sorts.relevance;`

`const_body_code : Vmemitcodes.body_code option;`

`const_universes : universes;`

`const_inline_code : bool;`

`const_typing_flags : typing_flags;`

The typing options which were used for type-checking.

`}`

`type constant_body`

`= Opaqueproof.opaque pconstant_body`

`type nested_type`

`=`

`|`

`NestedInd of Names.inductive`

`|`

`NestedPrimitive of Names.Constant.t`

###### Representation of mutual inductive types in the kernel

`type recarg`

`=`

`|`

`Norec`

`|`

`Mrec of Names.inductive`

`|`

`Nested of nested_type`

`type wf_paths`

`= recarg Rtree.t`

`type record_info`

`=`

`|`

`NotRecord`

`|`

`FakeRecord`

`|`

`PrimRecord of (Names.Id.t * Names.Label.t array * Sorts.relevance array * Constr.types array) array`

`type regular_inductive_arity`

`=`

`{`

`mind_user_arity : Constr.types;`

`mind_sort : Sorts.t;`

`}`

`type inductive_arity`

`= (regular_inductive_arity, template_arity) declaration_arity`

`type squash_info`

`=`

`|`

`AlwaysSquashed`

`|`

`SometimesSquashed of Sorts.Quality.Set.t`

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.`type one_inductive_body`

`=`

`{`

`mind_typename : Names.Id.t;`

Name of the type:

`Ii`

`mind_arity_ctxt : Constr.rel_context;`

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]`

.`mind_arity : inductive_arity;`

Arity sort and original user arity

`mind_consnames : Names.Id.t array;`

Names of the constructors:

`cij`

`mind_user_lc : Constr.types array;`

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.`mind_nrealargs : int;`

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

`mind_nrealdecls : int;`

Length of realargs context (with let, no params)

`mind_squashed : squash_info option;`

Is elimination restricted to the inductive's sort?

`mind_nf_lc : (Constr.rel_context * Constr.types) array;`

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.`mind_consnrealargs : int array;`

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

`mind_consnrealdecls : int array;`

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

`mind_recargs : wf_paths;`

Signature of recursive arguments in the constructors

`mind_relevance : Sorts.relevance;`

`mind_nb_constant : int;`

number of constant constructor

`mind_nb_args : int;`

number of no constant constructor

`mind_reloc_tbl : Vmvalues.reloc_table;`

`}`

###### Datas specific to a single type of a block of mutually inductive type

###### Datas associated to a full block of mutually inductive types

`type mutual_inductive_body`

`=`

`{`

`mind_packets : one_inductive_body array;`

The component of the mutual inductive block

`mind_record : record_info;`

The record information

`mind_finite : recursivity_kind;`

Whether the type is inductive, coinductive or non-recursive

`mind_ntypes : int;`

Number of types in the block

`mind_hyps : Constr.named_context;`

Section hypotheses on which the block depends

`mind_univ_hyps : UVars.Instance.t;`

Section polymorphic universes.

`mind_nparams : int;`

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

`mind_nparams_rec : int;`

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

`mind_params_ctxt : Constr.rel_context;`

The context of parameters (includes let-in declaration)

`mind_universes : universes;`

Information about monomorphic/polymorphic/cumulative inductives and their universes

`mind_template : template_universes option;`

`mind_variance : UVars.Variance.t array option;`

Variance info,

`None`

when non-cumulative.`mind_sec_variance : UVars.Variance.t array option;`

Variance info for section polymorphic universes.

`None`

outside sections. The final variance once all sections are discharged is`mind_sec_variance ++ mind_variance`

.`mind_private : bool option;`

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

`mind_typing_flags : typing_flags;`

typing flags at the time of the inductive creation

`}`

`type mind_specif`

`= mutual_inductive_body * one_inductive_body`

###### Module declarations

`type ('ty, 'a) functorize`

`=`

`|`

`NoFunctor of 'a`

`|`

`MoreFunctor of Names.MBId.t * 'ty * ('ty, 'a) functorize`

`type 'uconstr with_declaration`

`=`

`|`

`WithMod of Names.Id.t list * Names.ModPath.t`

`|`

`WithDef of Names.Id.t list * 'uconstr`

`type 'uconstr module_alg_expr`

`=`

`|`

`MEident of Names.ModPath.t`

`|`

`MEapply of 'uconstr module_alg_expr * Names.ModPath.t`

`|`

`MEwith of 'uconstr module_alg_expr * 'uconstr with_declaration`

`type 'uconstr functor_alg_expr`

`=`

`|`

`MENoFunctor of 'uconstr module_alg_expr`

`|`

`MEMoreFunctor of 'uconstr functor_alg_expr`

`type module_expression`

`= (Constr.constr * UVars.AbstractContext.t option) functor_alg_expr`

`type structure_field_body`

`=`

`|`

`SFBconst of constant_body`

`|`

`SFBmind of mutual_inductive_body`

`|`

`SFBmodule of module_body`

`|`

`SFBmodtype of module_type_body`

`and structure_body`

`= (Names.Label.t * structure_field_body) list`

`and module_signature`

`= (module_type_body, structure_body) functorize`

`and module_implementation`

`=`

`|`

`Abstract`

no accessible implementation

`|`

`Algebraic of module_expression`

non-interactive algebraic expression

`|`

`Struct of structure_body`

interactive body living in the parameter context of

`mod_type`

`|`

`FullStruct`

special case of

`Struct`

: the body is exactly`mod_type`

`and 'a generic_module_body`

`=`

`{`

`mod_mp : Names.ModPath.t;`

absolute path of the module

`mod_expr : 'a;`

implementation

`mod_type : module_signature;`

expanded type

`mod_type_alg : module_expression option;`

algebraic type

`mod_delta : Mod_subst.delta_resolver;`

quotiented set of equivalent constants and inductive names

`mod_retroknowledge : 'a module_retroknowledge;`

`}`

`and module_body`

`= module_implementation generic_module_body`

`and module_type_body`

`= unit generic_module_body`

`and _ module_retroknowledge`

`=`

`|`

`ModBodyRK : Retroknowledge.action list -> module_implementation module_retroknowledge`

`|`

`ModTypeRK : unit module_retroknowledge`