package coq

  1. Overview
  2. Docs
package coq
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
val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare
val infer_conv : ?l2r:bool -> ?evars:(Constr.existential -> Constr.constr option) -> ?ts:TransparentState.t -> Constr.constr infer_conversion_function
val infer_conv_leq : ?l2r:bool -> ?evars:(Constr.existential -> Constr.constr option) -> ?ts:TransparentState.t -> Constr.types infer_conversion_function
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
val beta_appvect : Constr.constr -> Constr.constr array -> Constr.constr
val hnf_prod_applist : Environ.env -> Constr.types -> Constr.constr list -> Constr.types
val hnf_prod_applist_assum : Environ.env -> int -> Constr.types -> Constr.constr list -> Constr.types
val betazeta_appvect : int -> Constr.constr -> Constr.constr array -> Constr.constr
exception NotArity
val dest_arity : Environ.env -> Constr.types -> Term.arity
val is_arity : Environ.env -> Constr.types -> bool