type t
= term
type view
=
val view : t -> view
val true_ : t
val false_ : t
val atom : t -> t
val eq : ?loc:location -> t -> t -> t
val neq : ?loc:location -> t -> t -> t
val equiv : ?loc:location -> t -> t -> t
val xor : ?loc:location -> t -> t -> t
val imply : ?loc:location -> t -> t -> t
val and_ : ?loc:location -> t list -> t
val or_ : ?loc:location -> t list -> t
val not_ : ?loc:location -> t -> t
val ite : ?loc:location -> t -> t -> t -> t
val forall : ?loc:location -> t Logtk.Var.t -> t -> t
val exists : ?loc:location -> t Logtk.Var.t -> t -> t
val eq_or_equiv : t -> t -> t
val neq_or_xor : t -> t -> t
val forall_l : ?loc:location -> t Logtk.Var.t list -> t -> t
val exists_l : ?loc:location -> t Logtk.Var.t list -> t -> t
val unfold_binder : Logtk.Binder.t -> t -> t Logtk.Var.t list * t
val unfold_forall : t -> t Logtk.Var.t list * t
val close_forall : ?loc:location -> t -> t
val box_opaque : t -> t
val is_var : view -> bool