package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.15.2.tar.gz
sha256=13a67c0a4559ae22e9765c8fdb88957b16c2b335a2d5f47e4d6d9b4b8b299926

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.existential -> Constr.constr option) -> '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

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

These two functions can only raise NotConvertible

Sourceval 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

Sourceval infer_conv_leq : ?l2r:bool -> ?evars:(Constr.existential -> Constr.constr option) -> ?ts:TransparentState.t -> Constr.types infer_conversion_function

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

Sourceexception NotArity
Sourceval is_arity : Environ.env -> Constr.types -> bool