Module Typing

This module provides the typing machine with existential variables and universes.

val unsafe_type_of : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.types

Typecheck a term and return its type. May trigger an evarmap leak.

val type_of : ?⁠refresh:bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.types

Typecheck a term and return its type + updated evars, optionally refreshing universes

val sort_of : Environ.env -> Evd.evar_map -> EConstr.types -> Evd.evar_map * Sorts.t

Typecheck a type and return its sort

val check : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.types -> Evd.evar_map

Typecheck a term has a given type (assuming the type is OK)

val meta_type : Evd.evar_map -> Constr.metavariable -> EConstr.types

Returns the instantiated type of a metavariable

val solve_evars : Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr

Solve existential variables using typing

val check_allowed_sort : Environ.env -> Evd.evar_map -> Constr.pinductive -> EConstr.constr -> EConstr.constr -> Sorts.relevance

Raise an error message if incorrect elimination for this inductive (first constr is term to match, second is return predicate)

val check_type_fixpoint : ?⁠loc:Loc.t -> Environ.env -> Evd.evar_map -> Names.Name.t Context.binder_annot array -> EConstr.types array -> EConstr.unsafe_judgment array -> Evd.evar_map

Raise an error message if bodies have types not unifiable with the expected ones

val judge_of_sprop : EConstr.unsafe_judgment
val judge_of_prop : EConstr.unsafe_judgment
val judge_of_set : EConstr.unsafe_judgment
val judge_of_apply : Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> Evd.evar_map * EConstr.unsafe_judgment
val judge_of_abstraction : Environ.env -> Names.Name.t -> EConstr.unsafe_type_judgment -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment
val judge_of_product : Environ.env -> Names.Name.t -> EConstr.unsafe_type_judgment -> EConstr.unsafe_type_judgment -> EConstr.unsafe_judgment
val judge_of_projection : Environ.env -> Evd.evar_map -> Names.Projection.t -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment
val judge_of_int : Environ.env -> Uint63.t -> EConstr.unsafe_judgment