package logtk

  1. Overview
  2. Docs
On This Page
  1. Simple Literal

Module Logtk.SLiteral

Simple Literal

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

type form = TypedSTerm.t
type term = TypedSTerm.t
exception NotALit of form
type +'t t =
  1. | True
  2. | False
  3. | Atom of 't * bool
  4. | Eq of 't * 't
  5. | 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_iter : 'a t -> 'a Iter.t
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val true_ : _ t
val false_ : _ t
val eq : 'a -> 'a -> 'a t
val neq : 'a -> 'a -> 'a t
val atom : 'a -> bool -> 'a t
val atom_true : 'a -> 'a t
val atom_false : 'a -> 'a t
val is_true : _ t -> bool
val is_false : _ t -> bool
val sign : _ t -> bool
val is_pos : _ t -> bool
val is_neg : _ t -> bool
val negate : 'a t -> 'a t

negation of literal

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