logtk

Core types and algorithms for logic
IN THIS PACKAGE
Module Logtk . Literal . Conv

Conversions

type hook_from = term SLiteral.t -> t option
type hook_to = t -> term SLiteral.t option
val of_form : ?hooks:hook_from list -> term SLiteral.t -> t

Conversion from a formula. By default no ordering is considered.

  • raises Invalid_argument

    if the formula is not atomic.

val to_form : ?hooks:hook_to list -> t -> term SLiteral.t
val to_s_form : ?allow_free_db:bool -> ?ctx:Term.Conv.ctx -> ?hooks:hook_to list -> t -> TypedSTerm.Form.t
val lit_to_tst : ?ctx:Term.Conv.ctx -> term SLiteral.t -> TypedSTerm.t