coq 8.7.1 · OCaml Package

coq

val whd_betaiotazeta : Environ.env -> Term.constr -> Term.constr

val whd_all : Environ.env -> Term.constr -> Term.constr

val whd_allnolet : Environ.env -> Term.constr -> Term.constr

val whd_betaiota : Environ.env -> Term.constr -> Term.constr

val nf_betaiota : Environ.env -> Term.constr -> Term.constr

exception NotConvertible

exception NotConvertibleVect of int

type !'a kernel_conversion_function = Environ.env -> 'a -> 'a -> unit

type !'a extended_conversion_function =
  ?l2r:bool ->
  ?reds:Names.transparent_state ->
  Environ.env ->
  ?evars:((Term.existential -> Term.constr option) * UGraph.t) ->
  'a ->
  'a ->
  unit

type conv_pb =

| CONV
| CUMUL

type !'a universe_compare = {

compare : Environ.env -> conv_pb -> Term.sorts -> Term.sorts -> 'a -> 'a;
compare_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a;
conv_constructors : (Declarations.mutual_inductive_body * int * int) -> Univ.Instance.t -> int -> Univ.Instance.t -> int -> '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 ->
  UGraph.t ->
  'a ->
  'a ->
  Univ.constraints

val sort_cmp_universes : 
  Environ.env ->
  conv_pb ->
  Term.sorts ->
  Term.sorts ->
  ('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 conv : Term.constr extended_conversion_function

val conv_leq : Term.types extended_conversion_function

val infer_conv : 
  ?l2r:bool ->
  ?evars:(Term.existential -> Term.constr option) ->
  ?ts:Names.transparent_state ->
  Term.constr infer_conversion_function

val infer_conv_leq : 
  ?l2r:bool ->
  ?evars:(Term.existential -> Term.constr option) ->
  ?ts:Names.transparent_state ->
  Term.types infer_conversion_function

val generic_conv : 
  conv_pb ->
  l2r:bool ->
  (Term.existential -> Term.constr option) ->
  Names.transparent_state ->
  (Term.constr, 'a) generic_conversion_function

val set_vm_conv : (conv_pb -> Term.types kernel_conversion_function) -> unit

val vm_conv : conv_pb -> Term.types kernel_conversion_function

val default_conv : 
  conv_pb ->
  ?l2r:bool ->
  Term.types kernel_conversion_function

val default_conv_leq : ?l2r:bool -> Term.types kernel_conversion_function

val beta_applist : Term.constr -> Term.constr list -> Term.constr

val beta_appvect : Term.constr -> Term.constr array -> Term.constr

val beta_app : Term.constr -> Term.constr -> Term.constr

val hnf_prod_applist : 
  Environ.env ->
  Term.types ->
  Term.constr list ->
  Term.types

val betazeta_appvect : int -> Term.constr -> Term.constr array -> Term.constr

val dest_prod : Environ.env -> Term.types -> Context.Rel.t * Term.types

val dest_prod_assum : Environ.env -> Term.types -> Context.Rel.t * Term.types

val dest_lam_assum : Environ.env -> Term.types -> Context.Rel.t * Term.types

exception NotArity

val dest_arity : Environ.env -> Term.types -> Term.arity

val is_arity : Environ.env -> Term.types -> bool

val warn_bytecode_compiler_failed : ?loc:Loc.t -> unit -> unit

package coq