package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module TypedSTerm.FormSource

Sourcetype t = term
Sourcetype 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
Sourceval view : t -> view

Smart constructors (perform simplifications)

Sourceval true_ : t
Sourceval false_ : t
Sourceval atom : t -> t
Sourceval eq : ?loc:location -> t -> t -> t
Sourceval neq : ?loc:location -> t -> t -> t
Sourceval equiv : ?loc:location -> t -> t -> t
Sourceval xor : ?loc:location -> t -> t -> t
Sourceval imply : ?loc:location -> t -> t -> t
Sourceval and_ : ?loc:location -> t list -> t
Sourceval or_ : ?loc:location -> t list -> t
Sourceval not_ : ?loc:location -> t -> t
Sourceval ite : ?loc:location -> t -> t -> t -> t
Sourceval forall : ?loc:location -> t Var.t -> t -> t
Sourceval exists : ?loc:location -> t Var.t -> t -> t
Sourceval eq_or_equiv : t -> t -> t
Sourceval neq_or_xor : t -> t -> t
Sourceval forall_l : ?loc:location -> t Var.t list -> t -> t
Sourceval exists_l : ?loc:location -> t Var.t list -> t -> t
Sourceval unfold_binder : Binder.t -> t -> t Var.t list * t
Sourceval unfold_forall : t -> t Var.t list * t
Sourceval close_forall : ?loc:location -> t -> t
Sourceval box_opaque : t -> t
Sourceval is_var : view -> bool