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