Module Reduction

val whd_betaiotazeta : Environ.env -> Constr.constr -> Constr.constr
val whd_all : Environ.env -> Constr.constr -> Constr.constr
val whd_allnolet : Environ.env -> Constr.constr -> Constr.constr
val whd_betaiota : Environ.env -> Constr.constr -> Constr.constr
val nf_betaiota : Environ.env -> Constr.constr -> Constr.constr
exception NotConvertible
type 'a kernel_conversion_function = Environ.env -> 'a -> 'a -> unit
type 'a extended_conversion_function = ?⁠l2r:bool -> ?⁠reds:TransparentState.t -> Environ.env -> ?⁠evars:(Constr.existential -> Constr.constr option) -> 'a -> 'a -> unit
type conv_pb =
| CONV
| CUMUL
type 'a universe_compare = {
compare_sorts : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
compare_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
compare_cumul_instances : conv_pb -> Univ.Variance.t array -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
}
type 'a universe_state = 'a * 'a universe_compare
type ('a, 'b) generic_conversion_function = Environ.env -> 'b universe_state -> 'a -> 'a -> 'b
type 'a infer_conversion_function = Environ.env -> 'a -> 'a -> Univ.Constraint.t
val get_cumulativity_constraints : conv_pb -> Univ.Variance.t array -> Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t
val inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int
val constructor_cumulativity_arguments : (Declarations.mutual_inductive_body * int * int) -> int
val sort_cmp_universes : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> ('a * 'a universe_compare) -> 'a * 'a universe_compare
val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> ('a * 'a universe_compare) -> 'a * 'a universe_compare
val checked_universes : UGraph.t universe_compare

These two never raise UnivInconsistency, inferred_universes just gathers the constraints.

val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare
val conv : Constr.constr extended_conversion_function

These two functions can only raise NotConvertible

val conv_leq : Constr.types extended_conversion_function
val infer_conv : ?⁠l2r:bool -> ?⁠evars:(Constr.existential -> Constr.constr option) -> ?⁠ts:TransparentState.t -> Constr.constr infer_conversion_function

These conversion functions are used by module subtyping, which needs to infer universe constraints inside the kernel

val infer_conv_leq : ?⁠l2r:bool -> ?⁠evars:(Constr.existential -> Constr.constr option) -> ?⁠ts:TransparentState.t -> Constr.types infer_conversion_function
val generic_conv : conv_pb -> l2r:bool -> (Constr.existential -> Constr.constr option) -> TransparentState.t -> (Constr.constr, 'a) generic_conversion_function

Depending on the universe state functions, this might raise UniverseInconsistency in addition to NotConvertible (for better error messages).

val default_conv : conv_pb -> ?⁠l2r:bool -> Constr.types kernel_conversion_function
val default_conv_leq : ?⁠l2r:bool -> Constr.types kernel_conversion_function
val beta_applist : Constr.constr -> Constr.constr list -> Constr.constr

Builds an application node, reducing beta redexes it may produce.

val beta_appvect : Constr.constr -> Constr.constr array -> Constr.constr

Builds an application node, reducing beta redexes it may produce.

val beta_app : Constr.constr -> Constr.constr -> Constr.constr

Builds an application node, reducing beta redexe it may produce.

val hnf_prod_applist : Environ.env -> Constr.types -> Constr.constr list -> Constr.types

Pseudo-reduction rule Prod(x,A,B) a --> Bx\a

val hnf_prod_applist_assum : Environ.env -> int -> Constr.types -> Constr.constr list -> Constr.types

In hnf_prod_applist_assum n c args, c is supposed to (whd-)reduce to the form ∀Γ.t with Γ of length n and possibly with let-ins; it returns t with the assumptions of Γ instantiated by args and the local definitions of Γ expanded.

val betazeta_appvect : int -> Constr.constr -> Constr.constr array -> Constr.constr

Compatibility alias for Term.lambda_appvect_assum

val dest_prod : Environ.env -> Constr.types -> Constr.rel_context * Constr.types
val dest_prod_assum : Environ.env -> Constr.types -> Constr.rel_context * Constr.types
val dest_lam : Environ.env -> Constr.constr -> Constr.rel_context * Constr.constr
val dest_lam_assum : Environ.env -> Constr.constr -> Constr.rel_context * Constr.constr
exception NotArity
val dest_arity : Environ.env -> Constr.types -> Term.arity
val is_arity : Environ.env -> Constr.types -> bool
val eta_expand : Environ.env -> Constr.constr -> Constr.types -> Constr.constr