sig
type type_ = TypedSTerm.t
type term = TypedSTerm.t
type form = TypedSTerm.t
type ctx
val create :
?prefix:string ->
?prop_prefix:string ->
?on_new:(ID.t -> Skolem.type_ -> unit) -> unit -> Skolem.ctx
val fresh_sym : ctx:Skolem.ctx -> ty:Skolem.type_ -> ID.t
val fresh_sym_with : ctx:Skolem.ctx -> ty:Skolem.type_ -> string -> ID.t
val pop_new_symbols : ctx:Skolem.ctx -> (ID.t * Skolem.type_) list
val skolem_form :
ctx:Skolem.ctx ->
(Skolem.type_, Skolem.term) Var.Subst.t ->
Skolem.type_ -> Skolem.form -> Skolem.term
type polarity = [ `Both | `Neg | `Pos ]
val pp_polarity : Skolem.polarity CCFormat.printer
type definition = {
form : Skolem.form;
proxy : Skolem.form;
polarity : Skolem.polarity;
}
val define :
ctx:Skolem.ctx -> polarity:Skolem.polarity -> Skolem.form -> Skolem.form
val pop_new_definitions : ctx:Skolem.ctx -> Skolem.definition list
exception Attr_skolem
val is_skolem : ID.t -> bool
end