package logtk

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

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