TypeopsThey 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_judgmentval infer_hconstr : Environ.env -> HConstr.t -> Environ.unsafe_judgmentval infer_type : Environ.env -> Constr.types -> Environ.unsafe_type_judgmentval check_context : Environ.env -> Constr.rel_context -> Environ.env * Constr.rel_contextIf 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.relevanceval type1 : Constr.typesType of sorts.
val type_of_sort : Sorts.t -> Constr.typesval type_of_relative : Environ.env -> int -> Constr.typesType of a bound variable.
val type_of_variable : Environ.env -> Names.variable -> Constr.typesType of variables
val type_of_constant_in : Environ.env -> Constr.pconstant -> Constr.typestype of a constant
val type_of_projection : Environ.env -> Names.Projection.t -> Constr.constr -> Constr.types -> Sorts.relevance * Constr.typestype of an applied projection
val sort_of_product : Environ.env -> Sorts.t -> Sorts.t -> Sorts.tType of a product.
val check_cast : Environ.env -> Environ.unsafe_judgment -> Constr.cast_kind -> Environ.unsafe_type_judgment -> unitType of a cast.
val type_of_global_in_context : Environ.env -> Names.GlobRef.t -> Constr.types * UVars.AbstractContext.tReturns 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:CClosure.evar_handler -> Names.GlobRef.t -> Constr.named_context -> unitCheck that hyps are included in env and fails with error otherwise
Types for primitives
val type_of_int : Environ.env -> Constr.typesval type_of_float : Environ.env -> Constr.typesval type_of_string : Environ.env -> Constr.typesval type_of_array : Environ.env -> UVars.Instance.t -> Constr.typesval type_of_prim_type : Environ.env -> UVars.Instance.t -> 'a CPrimitives.prim_type -> Constr.typesval type_of_prim : Environ.env -> UVars.Instance.t -> CPrimitives.t -> Constr.typesval type_of_prim_or_type : Environ.env -> UVars.Instance.t -> CPrimitives.op_or_type -> Constr.typesval should_invert_case : Environ.env -> Sorts.relevance -> Constr.case_info -> boolMatches must be annotated with the indices when going from SProp to non SProp (implies 1 or 0 constructors).