Reduction
val whd_all : Environ.env -> Constr.constr -> Constr.constr
val whd_allnolet : Environ.env -> Constr.constr -> Constr.constr
type 'a kernel_conversion_function = Environ.env -> 'a -> 'a -> unit
type 'a extended_conversion_function =
?l2r:bool ->
?reds:TransparentState.t ->
Environ.env ->
?evars:Constr.constr Constr.evar_handler ->
'a ->
'a ->
unit
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.Constraints.t
val get_cumulativity_constraints :
conv_pb ->
Univ.Variance.t array ->
Univ.Instance.t ->
Univ.Instance.t ->
Univ.Constraints.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
This function never raise UnivInconsistency.
val conv : Constr.constr extended_conversion_function
These two functions can only raise NotConvertible
val conv_leq : Constr.types extended_conversion_function
val generic_conv :
conv_pb ->
l2r:bool ->
Constr.constr Constr.evar_handler ->
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 -> Constr.types kernel_conversion_function
val default_conv_leq : 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_decls :
Environ.env ->
int ->
Constr.types ->
Constr.constr list ->
Constr.types
In hnf_prod_applist_decls 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_decls
val hnf_decompose_prod :
Environ.env ->
Constr.types ->
Constr.rel_context * Constr.types
val hnf_decompose_prod_decls :
Environ.env ->
Constr.types ->
Constr.rel_context * Constr.types
val hnf_decompose_lambda :
Environ.env ->
Constr.constr ->
Constr.rel_context * Constr.constr
val hnf_decompose_lambda_decls :
Environ.env ->
Constr.constr ->
Constr.rel_context * Constr.constr
val hnf_decompose_lambda_n_decls :
Environ.env ->
int ->
Constr.constr ->
Constr.rel_context * Constr.constr
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
Deprecated
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