Module Typeops

Typing functions (not yet tagged as safe)

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
Basic operations of the typing machine.
val assumption_of_judgment : Environ.env -> Environ.unsafe_judgment -> Sorts.relevance
val type_judgment : Environ.env -> Environ.unsafe_judgment -> Environ.unsafe_type_judgment
val check_binder_annot : Sorts.t -> Names.Name.t Context.binder_annot -> Names.Name.t Context.binder_annot
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.
Type of an abstraction.
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
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 judge_of_case : Environ.env -> Constr.case_info -> Environ.unsafe_judgment -> (Constr.constr, Univ.Instance.t) Constr.case_invert -> Environ.unsafe_judgment -> Environ.unsafe_judgment array -> Environ.unsafe_judgment
Type of Cases.
Type of global references.
val type_of_global_in_context : Environ.env -> Names.GlobRef.t -> Constr.types * Univ.AUContext.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.

Miscellaneous.
val check_hyps_inclusion : Environ.env -> ?⁠evars:(Constr.existential -> Constr.constr option) -> Names.GlobRef.t -> Constr.named_context -> unit

Check that hyps are included in env and fails with error otherwise

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 warn_bad_relevance_name : string

Allow the checker to make this warning into an error.

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.