Previous  Up  

Module Literal.Conv

module Conv: sig .. end

Conversions


type hook_from = Literal.term Libzipperposition.SLiteral.t -> Literal.t option 
type hook_to = Literal.t -> Literal.term Libzipperposition.SLiteral.t option 
val arith_hook_from : hook_from
val of_form : ?hooks:hook_from list ->
       Literal.term Libzipperposition.SLiteral.t -> Literal.t
Conversion from a formula. By default no ordering or arith theory is considered.
Raises Invalid_argument if the formula is not atomic.
val to_form : ?hooks:hook_to list ->
       Literal.t -> Literal.term Libzipperposition.SLiteral.t