Simple literals, used typically in CNF before being converted to whatever representation the prover prefers.
type form = TypedSTerm.ttype term = TypedSTerm.texception NotALit of formtype 'a lit = 'a tval fold : ('a -> 't -> 'a) -> 'a -> 't t -> 'aval iter : f:('a -> unit) -> 'a t -> unitval to_seq : 'a t -> 'a Iter.tval true_ : _ tval false_ : _ tval eq : 'a -> 'a -> 'a tval neq : 'a -> 'a -> 'a tval atom : 'a -> bool -> 'a tval atom_true : 'a -> 'a tval atom_false : 'a -> 'a tval is_true : _ t -> boolval is_false : _ t -> boolval sign : _ t -> boolval is_pos : _ t -> boolval is_neg : _ t -> boolinclude Interfaces.PRINT1 with type 'a t := 'a tval pp : 'a CCFormat.printer -> 'a t CCFormat.printerval to_string : 'a CCFormat.printer -> 'a t -> stringmodule TPTP : sig ... endmodule ZF : sig ... endval pp_in : Output_format.t -> 'a CCFormat.printer -> 'a t CCFormat.printer