package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val whd_betaiotazeta : 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 =
  1. | CONV
  2. | CUMUL
type '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;
}
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

These two functions can only raise NotConvertible

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

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.

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

exception NotArity
val dest_arity : Environ.env -> Constr.types -> Term.arity
val is_arity : Environ.env -> Constr.types -> bool
OCaml

Innovation. Community. Security.