module SLiteral:sig
..end
Used for reduction to CNF, this is a basic representation of literals
typeform =
TypedSTerm.t
typeterm =
TypedSTerm.t
exception NotALit of form
type 't
t =
| |
True |
| |
False |
| |
Atom of |
| |
Eq of |
| |
Neq of |
type'a
lit ='a t
val of_form : form -> term t
NotALit
if the form is not a literalval 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
include Interfaces.PRINT1
module TPTP:sig
..end
module ZF:sig
..end