package logtk

  1. Overview
  2. Docs
On This Page
  1. Simple Literal
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

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_seq : '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