Module `TypedSTerm.Form`

type t = term
type view = | True | False | Atom of t | Eq of t * t | Neq of t * t | Equiv of t * t | Xor of t * t | Imply of t * t | And of t list | Or of t list | Not of t | Forall of t Var.t * t | Exists of t Var.t * t

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 Var.t -> t -> t
val exists : ?⁠loc:location -> t Var.t -> t -> t
val eq_or_equiv : t -> t -> t
val neq_or_xor : t -> t -> t
val forall_l : ?⁠loc:location -> t Var.t list -> t -> t
val exists_l : ?⁠loc:location -> t Var.t list -> t -> t
val unfold_binder : Binder.t -> t -> t Var.t list * t
val unfold_forall : t -> t Var.t list * t
val close_forall : ?⁠loc:location -> t -> t
val box_opaque : t -> t
val is_var : view -> bool