Module `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 or arith theory 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