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 is considered.

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