Module Ctx_intf.S.Lit

module Lit: sig .. end

val from_hooks : unit -> Literal.Conv.hook_from list

val add_from_hook : Literal.Conv.hook_from -> unit

val to_hooks : unit -> Literal.Conv.hook_to list

val add_to_hook : Literal.Conv.hook_to -> unit

val of_form : Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t -> Literal.t

Raises Invalid_argument if the formula is not atomic

val to_form : Literal.t -> Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t