package logtk

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t = term
type view =
  1. | True
  2. | False
  3. | Atom of t
  4. | Eq of t * t
  5. | Neq of t * t
  6. | Equiv of t * t
  7. | Xor of t * t
  8. | Imply of t * t
  9. | And of t list
  10. | Or of t list
  11. | Not of t
  12. | Forall of t Var.t * t
  13. | 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