package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b

doc/coq-core.kernel/Reduction/index.html

Module ReductionSource

Sourceval whd_betaiotazeta : Environ.env -> Constr.constr -> Constr.constr
Sourceexception NotConvertible
Sourcetype 'a kernel_conversion_function = Environ.env -> 'a -> 'a -> unit
Sourcetype 'a extended_conversion_function = ?l2r:bool -> ?reds:TransparentState.t -> Environ.env -> ?evars:Constr.constr Constr.evar_handler -> 'a -> 'a -> unit
Sourcetype conv_pb =
  1. | CONV
  2. | CUMUL
Sourcetype 'a universe_compare = {
  1. compare_sorts : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
  2. compare_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
  3. compare_cumul_instances : conv_pb -> Univ.Variance.t array -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
}
Sourcetype 'a universe_state = 'a * 'a universe_compare
Sourcetype ('a, 'b) generic_conversion_function = Environ.env -> 'b universe_state -> 'a -> 'a -> 'b
Sourcetype 'a infer_conversion_function = Environ.env -> 'a -> 'a -> Univ.Constraints.t
Sourceval get_cumulativity_constraints : conv_pb -> Univ.Variance.t array -> Univ.Instance.t -> Univ.Instance.t -> Univ.Constraints.t
Sourceval inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int
Sourceval constructor_cumulativity_arguments : (Declarations.mutual_inductive_body * int * int) -> int
Sourceval sort_cmp_universes : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> ('a * 'a universe_compare) -> 'a * 'a universe_compare
Sourceval convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> ('a * 'a universe_compare) -> 'a * 'a universe_compare
Sourceval checked_universes : UGraph.t universe_compare

This function never raise UnivInconsistency.

These two functions can only raise NotConvertible

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

Sourceval beta_applist : Constr.constr -> Constr.constr list -> Constr.constr

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

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

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

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

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

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

Sourceval 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.

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

Compatibility alias for Term.lambda_appvect_assum

Sourceval dest_lam_n_assum : Environ.env -> int -> Constr.constr -> Constr.rel_context * Constr.constr
Sourceexception NotArity
Sourceval is_arity : Environ.env -> Constr.types -> bool