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.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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct