module Formula: sig .. end
type 'a t = 'a Syntax.formula
val equal : 'a Syntax.formula -> 'a Syntax.formula -> bool
val compare : 'a Syntax.formula -> 'a Syntax.formula -> int
val hash : 'a Syntax.formula -> int
val pp : ?env:string Syntax.Env.t ->
'a Syntax.context -> Format.formatter -> 'a Syntax.formula -> unit
val show : ?env:string Syntax.Env.t -> 'a Syntax.context -> 'a Syntax.formula -> string
val destruct : 'a Syntax.context ->
'a Syntax.formula -> ('a Syntax.formula, 'a) Syntax.open_formula
val eval : 'a Syntax.context ->
(('b, 'a) Syntax.open_formula -> 'b) -> 'a Syntax.formula -> 'b
val eval_memo : 'a Syntax.context ->
(('b, 'a) Syntax.open_formula -> 'b) -> 'a Syntax.formula -> 'b
val existential_closure : 'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
val universal_closure : 'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
val skolemize_free : 'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
val prenex : 'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula