Module SLiteral

module SLiteral: sig .. end

Simple Literal

Used for reduction to CNF, this is a basic representation of literals


type form = TypedSTerm.t 
type term = TypedSTerm.t 
exception NotALit of form
type 't t = 
| True
| False
| Atom of 't * bool
| Eq of 't * 't
| Neq of 't * 't
type 'a lit = 'a t 
val of_form : form -> term t
Raises NotALit if the form is not a literal
val to_form : term t -> form
val map : f:('a -> 'b) -> 'a t -> 'b t
val fold : ('a -> 't -> 'a) -> 'a -> 't t -> 'a
val iter : f:('a -> unit) -> 'a t -> unit
val to_seq : 'a t -> 'a Sequence.t
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val true_ : 'a t
val false_ : 'a t
val eq : 'a -> 'a -> 'a t
val neq : 'a -> 'a -> 'a t
val atom : 'a -> bool -> 'a t
val is_true : 'a t -> bool
val is_false : 'a t -> bool
val sign : 'a t -> bool
val is_pos : 'a t -> bool
val is_neg : 'a t -> bool
val negate : 'a t -> 'a t
negation of literal
include Interfaces.PRINT1
module TPTP: sig .. end
module ZF: sig .. end