Module LogtkFormula.S.Base

module Base: sig .. end

val true_ : LogtkFormula.S.t
val false_ : LogtkFormula.S.t
val atom : LogtkFormula.S.term -> LogtkFormula.S.t
val not_ : LogtkFormula.S.t -> LogtkFormula.S.t
val and_ : LogtkFormula.S.t list -> LogtkFormula.S.t
val or_ : LogtkFormula.S.t list -> LogtkFormula.S.t
val imply : LogtkFormula.S.t -> LogtkFormula.S.t -> LogtkFormula.S.t
val equiv : LogtkFormula.S.t -> LogtkFormula.S.t -> LogtkFormula.S.t
val xor : LogtkFormula.S.t -> LogtkFormula.S.t -> LogtkFormula.S.t
val eq : LogtkFormula.S.term -> LogtkFormula.S.term -> LogtkFormula.S.t
val neq : LogtkFormula.S.term -> LogtkFormula.S.term -> LogtkFormula.S.t
val mk_eq : bool -> LogtkFormula.S.term -> LogtkFormula.S.term -> LogtkFormula.S.t
val mk_atom : bool -> LogtkFormula.S.term -> LogtkFormula.S.t

Quantifiers: the term list must be a list of free variables.
val forall : LogtkFormula.S.term list -> LogtkFormula.S.t -> LogtkFormula.S.t
val exists : LogtkFormula.S.term list -> LogtkFormula.S.t -> LogtkFormula.S.t
val forall_ty : LogtkFormula.type_ list -> LogtkFormula.S.t -> LogtkFormula.S.t
val __mk_forall : varty:LogtkFormula.type_ -> LogtkFormula.S.t -> LogtkFormula.S.t
val __mk_exists : varty:LogtkFormula.type_ -> LogtkFormula.S.t -> LogtkFormula.S.t
val __mk_forall_ty : LogtkFormula.S.t -> LogtkFormula.S.t