sig
type t = TypedSTerm.term
type view =
True
| False
| Atom of TypedSTerm.Form.t
| Eq of TypedSTerm.Form.t * TypedSTerm.Form.t
| Neq of TypedSTerm.Form.t * TypedSTerm.Form.t
| Equiv of TypedSTerm.Form.t * TypedSTerm.Form.t
| Xor of TypedSTerm.Form.t * TypedSTerm.Form.t
| Imply of TypedSTerm.Form.t * TypedSTerm.Form.t
| And of TypedSTerm.Form.t list
| Or of TypedSTerm.Form.t list
| Not of TypedSTerm.Form.t
| Forall of TypedSTerm.Form.t Var.t * TypedSTerm.Form.t
| Exists of TypedSTerm.Form.t Var.t * TypedSTerm.Form.t
val view : TypedSTerm.Form.t -> TypedSTerm.Form.view
val true_ : TypedSTerm.Form.t
val false_ : TypedSTerm.Form.t
val atom : TypedSTerm.Form.t -> TypedSTerm.Form.t
val eq :
?loc:TypedSTerm.location ->
TypedSTerm.Form.t -> TypedSTerm.Form.t -> TypedSTerm.Form.t
val neq :
?loc:TypedSTerm.location ->
TypedSTerm.Form.t -> TypedSTerm.Form.t -> TypedSTerm.Form.t
val equiv :
?loc:TypedSTerm.location ->
TypedSTerm.Form.t -> TypedSTerm.Form.t -> TypedSTerm.Form.t
val xor :
?loc:TypedSTerm.location ->
TypedSTerm.Form.t -> TypedSTerm.Form.t -> TypedSTerm.Form.t
val imply :
?loc:TypedSTerm.location ->
TypedSTerm.Form.t -> TypedSTerm.Form.t -> TypedSTerm.Form.t
val and_ :
?loc:TypedSTerm.location -> TypedSTerm.Form.t list -> TypedSTerm.Form.t
val or_ :
?loc:TypedSTerm.location -> TypedSTerm.Form.t list -> TypedSTerm.Form.t
val not_ :
?loc:TypedSTerm.location -> TypedSTerm.Form.t -> TypedSTerm.Form.t
val forall :
?loc:TypedSTerm.location ->
TypedSTerm.Form.t Var.t -> TypedSTerm.Form.t -> TypedSTerm.Form.t
val exists :
?loc:TypedSTerm.location ->
TypedSTerm.Form.t Var.t -> TypedSTerm.Form.t -> TypedSTerm.Form.t
val forall_l :
?loc:TypedSTerm.location ->
TypedSTerm.Form.t Var.t list -> TypedSTerm.Form.t -> TypedSTerm.Form.t
val exists_l :
?loc:TypedSTerm.location ->
TypedSTerm.Form.t Var.t list -> TypedSTerm.Form.t -> TypedSTerm.Form.t
val close_forall :
?loc:TypedSTerm.location -> TypedSTerm.Form.t -> TypedSTerm.Form.t
end