module F: sig
.. end
Expressions
include Logic.Term
type
unop = term -> term
type
binop = term -> term -> term
val e_zero : term
val e_one : term
val e_minus_one : term
val e_one_real : term
val e_zero_real : term
val constant : term -> term
val e_fact : int -> term -> term
val e_int64 : int64 -> term
val e_bigint : Integer.t -> term
val e_mthfloat : float -> term
val e_hexfloat : float -> term
val e_setfield : term -> Lang.field -> term -> term
val e_range : term -> term -> term
e_range a b = b+1-a
val is_zero : term -> bool
Predicates
type
pred
type
cmp = term -> term -> pred
val p_true : pred
val p_false : pred
val p_equal : term -> term -> pred
val p_neq : term -> term -> pred
val p_leq : term -> term -> pred
val p_lt : term -> term -> pred
val p_positive : term -> pred
val is_ptrue : pred -> Qed.Logic.maybe
val is_pfalse : pred -> Qed.Logic.maybe
val is_equal : term -> term -> Qed.Logic.maybe
val eqp : pred -> pred -> bool
val comparep : pred -> pred -> int
val p_bool : term -> pred
val e_prop : pred -> term
val p_bools : term list -> pred list
val e_props : pred list -> term list
val lift : (term -> term) -> pred -> pred
val p_not : pred -> pred
val p_and : pred -> pred -> pred
val p_or : pred -> pred -> pred
val p_imply : pred -> pred -> pred
val p_equiv : pred -> pred -> pred
val p_hyps : pred list -> pred -> pred
val p_if : pred -> pred -> pred -> pred
val p_conj : pred list -> pred
val p_disj : pred list -> pred
val p_any : ('a -> pred) -> 'a list -> pred
val p_all : ('a -> pred) -> 'a list -> pred
val p_call : Lang.lfun -> term list -> pred
val p_forall : var list -> pred -> pred
val p_exists : var list -> pred -> pred
val p_bind : Qed.Logic.binder -> var -> pred -> pred
val e_subst : ?sigma:sigma -> (term -> term) -> term -> term
val p_subst : ?sigma:sigma -> (term -> term) -> pred -> pred
val p_close : pred -> pred
val idp : pred -> int
val varsp : pred -> Vars.t
val occurs : var -> term -> bool
val occursp : var -> pred -> bool
val intersect : term -> term -> bool
val intersectp : pred -> pred -> bool
val pp_var : Format.formatter -> var -> unit
val pp_vars : Format.formatter -> Vars.t -> unit
val pp_term : Format.formatter -> term -> unit
val pp_pred : Format.formatter -> pred -> unit
val debugp : Format.formatter -> pred -> unit
type
env
val env : Vars.t -> env
val marker : env -> marks
val mark_e : marks -> term -> unit
val mark_p : marks -> pred -> unit
val define : (env -> string -> term -> unit) -> env -> marks -> env
val pp_eterm : env -> Format.formatter -> term -> unit
val pp_epred : env -> Format.formatter -> pred -> unit
val pred : pred -> pred expression
val epred : pred -> term expression
module Pmap: Qed.Idxmap.S
with type key = pred
module Pset: Qed.Idxset.S
with type elt = pred
Builtins
val release : unit -> unit
val set_builtin_1 : Lang.lfun -> (term -> term) -> unit
val set_builtin_2 : Lang.lfun -> (term -> term -> term) -> unit
val set_builtin_eqp : Lang.lfun -> (term -> term -> pred) -> unit
Internal Checks
val do_checks : bool Pervasives.ref
val iter_checks : (qed:term -> raw:term -> goal:pred -> unit) -> unit