logtk

Core types and algorithms for logic
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library logtk
Module Logtk . 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

Smart constructors (perform simplifications)

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