Typeops
They return unsafe judgments that are "in context" of a set of (local) universe variables (the ones that appear in the term) and associated constraints. In case of polymorphic definitions, these variables and constraints will be generalized.
When typechecking a term it may be updated to fix relevance marks. Do not discard the result.
val infer : Environ.env -> Constr.constr -> Environ.unsafe_judgment
val infer_type : Environ.env -> Constr.types -> Environ.unsafe_type_judgment
val check_context :
Environ.env ->
Constr.rel_context ->
Environ.env * Constr.rel_context
If j
is the judgement $
c:t $
, then assumption_of_judgement env j
returns the type $
c $
, checking that $
t $
is a sort.
val assumption_of_judgment :
Environ.env ->
Environ.unsafe_judgment ->
Sorts.relevance
val type_judgment :
Environ.env ->
Environ.unsafe_judgment ->
Environ.unsafe_type_judgment
val type1 : Constr.types
Type of sorts.
val type_of_sort : Sorts.t -> Constr.types
val judge_of_prop : Environ.unsafe_judgment
val judge_of_set : Environ.unsafe_judgment
val judge_of_type : Univ.Universe.t -> Environ.unsafe_judgment
val type_of_relative : Environ.env -> int -> Constr.types
Type of a bound variable.
val judge_of_relative : Environ.env -> int -> Environ.unsafe_judgment
val type_of_variable : Environ.env -> Names.variable -> Constr.types
Type of variables
val judge_of_variable :
Environ.env ->
Names.variable ->
Environ.unsafe_judgment
val type_of_constant_in : Environ.env -> Constr.pconstant -> Constr.types
type of a constant
val judge_of_constant :
Environ.env ->
Constr.pconstant ->
Environ.unsafe_judgment
val judge_of_projection :
Environ.env ->
Names.Projection.t ->
Environ.unsafe_judgment ->
Environ.unsafe_judgment
type of an applied projection
val judge_of_apply :
Environ.env ->
Environ.unsafe_judgment ->
Environ.unsafe_judgment array ->
Environ.unsafe_judgment
Type of application.
val sort_of_product : Environ.env -> Sorts.t -> Sorts.t -> Sorts.t
Type of a product.
val type_of_product :
Environ.env ->
Names.Name.t Context.binder_annot ->
Sorts.t ->
Sorts.t ->
Constr.types
s Type of a let in.
val judge_of_cast :
Environ.env ->
Environ.unsafe_judgment ->
Constr.cast_kind ->
Environ.unsafe_type_judgment ->
Environ.unsafe_judgment
Type of a cast.
val judge_of_inductive :
Environ.env ->
Names.inductive Univ.puniverses ->
Environ.unsafe_judgment
Inductive types.
val judge_of_constructor :
Environ.env ->
Names.constructor Univ.puniverses ->
Environ.unsafe_judgment
val type_of_global_in_context :
Environ.env ->
Names.GlobRef.t ->
Constr.types * Univ.AbstractContext.t
Returns the type of the global reference, by creating a fresh instance of polymorphic references and computing their instantiated universe context. The type should not be used without pushing it's universe context in the environmnent of usage. For non-universe-polymorphic constants, it does not matter.
val check_hyps_inclusion :
Environ.env ->
?evars:Constr.constr Constr.evar_handler ->
Names.GlobRef.t ->
Constr.named_context ->
unit
Check that hyps are included in env and fails with error otherwise
Types for primitives
val type_of_int : Environ.env -> Constr.types
val judge_of_int : Environ.env -> Uint63.t -> Environ.unsafe_judgment
val type_of_float : Environ.env -> Constr.types
val judge_of_float : Environ.env -> Float64.t -> Environ.unsafe_judgment
val type_of_array : Environ.env -> Univ.Instance.t -> Constr.types
val judge_of_array :
Environ.env ->
Univ.Instance.t ->
Environ.unsafe_judgment array ->
Environ.unsafe_judgment ->
Environ.unsafe_judgment
val type_of_prim_type :
Environ.env ->
Univ.Instance.t ->
'a CPrimitives.prim_type ->
Constr.types
val type_of_prim :
Environ.env ->
Univ.Instance.t ->
CPrimitives.t ->
Constr.types
val type_of_prim_or_type :
Environ.env ->
Univ.Instance.t ->
CPrimitives.op_or_type ->
Constr.types
val bad_relevance_warning : CWarnings.warning
Also used by the pretyper to define a message which uses the evar map.
type ('constr, 'types) bad_relevance =
| BadRelevanceBinder of Sorts.relevance
* ( 'constr, 'types ) Context.Rel.Declaration.pt |
| BadRelevanceCase of Sorts.relevance * 'constr |
val bad_relevance_msg :
(Environ.env * ( Constr.constr, Constr.types ) bad_relevance) CWarnings.msg
Used by the higher layers to register a nicer printer than the default.
val should_invert_case : Environ.env -> Constr.case_info -> bool
We have case inversion exactly when going from irrelevant nonempty (ie 1 constructor) inductive to relevant type.