Previous  Up  Next

Module TypedSTerm.Form

module Form: sig .. end
type t = TypedSTerm.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

Smart constructors (perform simplifications)
val true_ : t
val false_ : t
val atom : t -> t
val eq : ?loc:TypedSTerm.location ->
       t -> t -> t
val neq : ?loc:TypedSTerm.location ->
       t -> t -> t
val equiv : ?loc:TypedSTerm.location ->
       t -> t -> t
val xor : ?loc:TypedSTerm.location ->
       t -> t -> t
val imply : ?loc:TypedSTerm.location ->
       t -> t -> t
val and_ : ?loc:TypedSTerm.location -> t list -> t
val or_ : ?loc:TypedSTerm.location -> t list -> t
val not_ : ?loc:TypedSTerm.location -> t -> t
val forall : ?loc:TypedSTerm.location ->
       t Var.t -> t -> t
val exists : ?loc:TypedSTerm.location ->
       t Var.t -> t -> t
val forall_l : ?loc:TypedSTerm.location ->
       t Var.t list -> t -> t
val exists_l : ?loc:TypedSTerm.location ->
       t Var.t list -> t -> t
val close_forall : ?loc:TypedSTerm.location -> t -> t