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 =

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