Module Logtk.SLiteralSource

Simple Literal

Simple literals, used typically in CNF before being converted to whatever representation the prover prefers.

Sourcetype form = TypedSTerm.t
Sourcetype term = TypedSTerm.t
Sourceexception NotALit of form
Sourcetype +'t t =
  1. | True
  2. | False
  3. | Atom of 't * bool
  4. | Eq of 't * 't
  5. | Neq of 't * 't
Sourcetype 'a lit = 'a t
Sourceval of_form : form -> term t
  • raises NotALit

    if the form is not a literal

Sourceval to_form : term t -> form
Sourceval map : f:('a -> 'b) -> 'a t -> 'b t
Sourceval fold : ('a -> 't -> 'a) -> 'a -> 't t -> 'a
Sourceval iter : f:('a -> unit) -> 'a t -> unit
Sourceval to_seq : 'a t -> 'a Iter.t
Sourceval equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
Sourceval true_ : _ t
Sourceval false_ : _ t
Sourceval eq : 'a -> 'a -> 'a t
Sourceval neq : 'a -> 'a -> 'a t
Sourceval atom : 'a -> bool -> 'a t
Sourceval atom_true : 'a -> 'a t
Sourceval atom_false : 'a -> 'a t
Sourceval is_true : _ t -> bool
Sourceval is_false : _ t -> bool
Sourceval sign : _ t -> bool
Sourceval is_pos : _ t -> bool
Sourceval is_neg : _ t -> bool
Sourceval negate : 'a t -> 'a t

negation of literal

include Interfaces.PRINT1 with type 'a t := 'a t
Sourceval to_string : 'a CCFormat.printer -> 'a t -> string
Sourcemodule TPTP : sig ... end
Sourcemodule ZF : sig ... end