module F: sig
.. end
module ZInteger: sig
.. end
module T: Qed.Term.Make
(
ZInteger
)
(
Lang.ADT
)
(
Lang.Field
)
(
Lang.Fun
)
module TT: T
module DATA: Datatype.Make
(
sig
type
t = Lang.F.T.state
val name : string
val rehash : 'a -> 'a
val structural_descr : Structural_descr.t
val reprs : Lang.F.T.state list
val equal : 'a -> 'b
val compare : 'a -> 'b
val hash : 'a -> 'b
val copy : 'a -> Lang.F.T.state
val varname : 'a -> 'b
val pretty : 'a -> 'b
val internal_pretty_code : 'a -> 'b
val mem_project : 'a -> 'b -> bool
end
)
module STATE: State_builder.Register
(
DATA
)
(
sig
type
t = Lang.F.T.state
val create : unit -> Lang.F.T.state
val clear : Lang.F.T.state -> unit
val get : unit -> Lang.F.T.state
val set : Lang.F.T.state -> unit
val clear_some_projects : 'a -> 'b -> bool
end
)
(
sig
val name : string
val dependencies : 'a list
val unique_name : string
end
)
module Pretty: Qed.Pretty.Make
(
T
)
include TT
val do_checks : bool Pervasives.ref
val iter_checks : (qed:T.term -> raw:T.term -> goal:T.term -> unit) ->
unit
val e_add : T.term -> T.term -> T.term
val e_sum : T.term list -> T.term
val e_times : T.Z.t -> T.term -> T.term
val e_opp : T.term -> T.term
val e_leq : T.term -> T.term -> T.term
val e_lt : T.term -> T.term -> T.term
val e_eq : T.term -> T.term -> T.term
val e_neq : T.term -> T.term -> T.term
val e_fun : T.Fun.t -> T.term list -> T.term
type
unop = term -> term
type
binop = term -> term -> term
val e_zero : T.term
val e_one : T.term
val e_minus_one : T.term
val e_one_real : T.term
val e_zero_real : T.term
val hex_of_float : float -> string
val e_int64 : int64 -> term
val e_fact : int -> T.term -> T.term
val e_bigint : Integer.t -> term
val e_range : T.term -> T.term -> T.term
e_range a b = b+1-a
val e_mthfloat : float -> T.term
val e_hexfloat : float -> T.term
val e_setfield : term -> Lang.Field.t -> term -> term
type
pred = term
type
cmp = term -> term -> pred
val p_bool : 'a -> 'a
val e_prop : 'a -> 'a
val p_bools : 'a -> 'a
val e_props : 'a -> 'a
val lift : ('a -> 'b) -> 'a -> 'b
val is_zero : T.term -> bool
val eqp : t -> t -> bool
val comparep : t -> t -> int
val is_ptrue : term -> Qed.Logic.maybe
val is_pfalse : term -> Qed.Logic.maybe
val is_equal : T.term -> T.term -> Qed.Logic.maybe
val p_equal : T.term -> T.term -> T.term
val p_neq : T.term -> T.term -> T.term
val p_leq : T.term -> T.term -> T.term
val p_lt : T.term -> T.term -> T.term
val p_positive : T.term -> T.term
val p_true : term
val p_false : term
val p_not : term -> term
val p_bind : Qed.Logic.binder -> var -> term -> term
val p_forall : var list -> term -> term
val p_exists : var list -> term -> term
val p_subst : ?sigma:sigma -> (term -> term) -> term -> term
val p_and : term -> term -> term
val p_or : term -> term -> term
val p_imply : term -> term -> term
val p_hyps : term list -> term -> term
val p_equiv : term -> term -> term
val p_if : term -> term -> term -> term
val p_conj : term list -> term
val p_disj : term list -> term
val p_all : ('a -> term) -> 'a list -> term
val p_any : ('a -> term) -> 'a list -> term
val p_call : T.Fun.t -> T.term list -> T.term
val p_close : term -> term
val occurs : Vars.elt -> term -> bool
val intersect : term -> term -> bool
val occursp : Vars.elt -> term -> bool
val intersectp : term -> term -> bool
val varsp : term -> Vars.t
val pred : term -> repr
val idp : t -> int
val pp_term : Format.formatter -> T.term -> unit
val pp_pred : Format.formatter -> T.term -> unit
val pp_var : Format.formatter -> var -> unit
val pp_vars : Format.formatter -> Vars.t -> unit
val debugp : Format.formatter -> T.term -> unit
type
env = Pretty.env
val env : T.Vars.t -> Pretty.env
val marker : Pretty.env -> T.marks
val mark_vars : Pretty.env -> T.Vars.t -> Pretty.env
val mark_e : T.marks -> T.term -> unit
val mark_p : T.marks -> T.term -> unit
val define : (Pretty.env -> string -> T.term -> 'a) ->
Pretty.env -> T.marks -> Pretty.env
val pp_eterm : Pretty.env -> Format.formatter -> T.term -> unit
val pp_epred : Pretty.env -> Format.formatter -> T.term -> unit
module Pmap: Tmap
module Pset: Tset
val set_builtin_1 : Lang.Fun.t -> (term -> term) -> unit
val set_builtin_2 : Lang.Fun.t -> (term -> term -> term) -> unit
val set_builtin_eqp : Lang.Fun.t -> (term -> term -> term) -> unit