sig
  type 'a or_error = [ `Error of string | `Ok of 'a ]
  type default_types = {
    default_i : LogtkType.t;
    default_prop : LogtkType.t;
    default_int : LogtkType.t;
    default_rat : LogtkType.t;
  }
  val tptp_default : LogtkTypeInference.default_types
  module Ctx :
    sig
      type t
      val create :
        ?default:LogtkTypeInference.default_types ->
        LogtkSignature.t -> LogtkTypeInference.Ctx.t
      val clear : LogtkTypeInference.Ctx.t -> unit
      val copy : LogtkTypeInference.Ctx.t -> LogtkTypeInference.Ctx.t
      val exit_scope : LogtkTypeInference.Ctx.t -> unit
      val add_signature :
        LogtkTypeInference.Ctx.t -> LogtkSignature.t -> unit
      val declare :
        LogtkTypeInference.Ctx.t -> LogtkSymbol.t -> LogtkType.t -> unit
      val ty_of_prolog :
        LogtkTypeInference.Ctx.t -> LogtkPrologTerm.t -> LogtkType.t option
      val bind_to_default : LogtkTypeInference.Ctx.t -> unit
      val generalize : LogtkTypeInference.Ctx.t -> unit
      val to_signature : LogtkTypeInference.Ctx.t -> LogtkSignature.t
      val constrain_type_type :
        LogtkTypeInference.Ctx.t -> LogtkType.t -> LogtkType.t -> unit
    end
  module Closure :
    sig
      type 'a t = LogtkTypeInference.Ctx.t -> 'a
      val return : '-> 'LogtkTypeInference.Closure.t
      val map :
        'LogtkTypeInference.Closure.t ->
        ('-> 'b) -> 'LogtkTypeInference.Closure.t
      val ( >>= ) :
        'LogtkTypeInference.Closure.t ->
        ('-> 'LogtkTypeInference.Closure.t) ->
        'LogtkTypeInference.Closure.t
      type 'a monad = 'LogtkTypeInference.Closure.t
      val fold :
        'Sequence.t ->
        'LogtkTypeInference.Closure.monad ->
        ('-> '-> 'LogtkTypeInference.Closure.monad) ->
        'LogtkTypeInference.Closure.monad
      val fold_l :
        'a list ->
        'LogtkTypeInference.Closure.monad ->
        ('-> '-> 'LogtkTypeInference.Closure.monad) ->
        'LogtkTypeInference.Closure.monad
      val map_l :
        'a list ->
        ('-> 'LogtkTypeInference.Closure.monad) ->
        'b list LogtkTypeInference.Closure.monad
      val seq :
        'LogtkTypeInference.Closure.monad list ->
        'a list LogtkTypeInference.Closure.monad
    end
  module type S =
    sig
      type untyped
      type typed
      val infer_exn :
        LogtkTypeInference.Ctx.t ->
        LogtkTypeInference.S.untyped ->
        LogtkType.t * LogtkTypeInference.S.typed LogtkTypeInference.Closure.t
      val infer :
        LogtkTypeInference.Ctx.t ->
        LogtkTypeInference.S.untyped ->
        (LogtkType.t *
         LogtkTypeInference.S.typed LogtkTypeInference.Closure.t)
        LogtkTypeInference.or_error
      val constrain_term_term_exn :
        LogtkTypeInference.Ctx.t ->
        LogtkTypeInference.S.untyped -> LogtkTypeInference.S.untyped -> unit
      val constrain_term_type_exn :
        LogtkTypeInference.Ctx.t ->
        LogtkTypeInference.S.untyped -> LogtkType.t -> unit
      val constrain_term_term :
        LogtkTypeInference.Ctx.t ->
        LogtkTypeInference.S.untyped ->
        LogtkTypeInference.S.untyped -> unit LogtkTypeInference.or_error
      val constrain_term_type :
        LogtkTypeInference.Ctx.t ->
        LogtkTypeInference.S.untyped ->
        LogtkType.t -> unit LogtkTypeInference.or_error
    end
  val map_error_seq :
    ('-> 'LogtkTypeInference.or_error) ->
    'Sequence.t -> 'Sequence.t LogtkTypeInference.or_error
  module FO :
    sig
      type untyped = LogtkPrologTerm.t
      type typed = LogtkFOTerm.t
      val infer_exn : Ctx.t -> untyped -> LogtkType.t * typed Closure.t
      val infer :
        Ctx.t -> untyped -> (LogtkType.t * typed Closure.t) or_error
      val constrain_term_term_exn : Ctx.t -> untyped -> untyped -> unit
      val constrain_term_type_exn : Ctx.t -> untyped -> LogtkType.t -> unit
      val constrain_term_term : Ctx.t -> untyped -> untyped -> unit or_error
      val constrain_term_type :
        Ctx.t -> untyped -> LogtkType.t -> unit or_error
      type typed_form = LogtkFormula.FO.t
      val constrain_form :
        LogtkTypeInference.Ctx.t ->
        untyped -> unit LogtkTypeInference.or_error
      val infer_form :
        LogtkTypeInference.Ctx.t ->
        untyped ->
        LogtkTypeInference.FO.typed_form LogtkTypeInference.Closure.t
        LogtkTypeInference.or_error
      val signature_forms :
        LogtkSignature.t ->
        untyped Sequence.t -> LogtkSignature.t LogtkTypeInference.or_error
      val convert :
        ?generalize:bool ->
        ctx:LogtkTypeInference.Ctx.t ->
        untyped -> typed LogtkTypeInference.or_error
      val convert_form :
        ?generalize:bool ->
        ctx:LogtkTypeInference.Ctx.t ->
        untyped -> LogtkFormula.FO.t LogtkTypeInference.or_error
      val convert_clause :
        ?generalize:bool ->
        ctx:LogtkTypeInference.Ctx.t ->
        untyped list -> LogtkFormula.FO.t list LogtkTypeInference.or_error
      val convert_seq :
        ?generalize:bool ->
        [ `ctx of LogtkTypeInference.Ctx.t | `sign of LogtkSignature.t ] ->
        untyped Sequence.t ->
        LogtkFormula.FO.t list LogtkTypeInference.or_error
      val infer_form_exn :
        LogtkTypeInference.Ctx.t ->
        untyped ->
        LogtkTypeInference.FO.typed_form LogtkTypeInference.Closure.t
      val constrain_form_exn : LogtkTypeInference.Ctx.t -> untyped -> unit
      val signature_forms_exn :
        LogtkSignature.t -> untyped Sequence.t -> LogtkSignature.t
      val convert_exn :
        ?generalize:bool -> ctx:LogtkTypeInference.Ctx.t -> untyped -> typed
      val convert_form_exn :
        ?generalize:bool ->
        ctx:LogtkTypeInference.Ctx.t -> untyped -> LogtkFormula.FO.t
      val convert_clause_exn :
        ?generalize:bool ->
        ctx:LogtkTypeInference.Ctx.t ->
        untyped list -> LogtkFormula.FO.t list
      val convert_seq_exn :
        ?generalize:bool ->
        [ `ctx of LogtkTypeInference.Ctx.t | `sign of LogtkSignature.t ] ->
        untyped Sequence.t -> LogtkFormula.FO.t list
    end
  module HO :
    sig
      type untyped = LogtkPrologTerm.t
      type typed = LogtkHOTerm.t
      val infer_exn : Ctx.t -> untyped -> LogtkType.t * typed Closure.t
      val infer :
        Ctx.t -> untyped -> (LogtkType.t * typed Closure.t) or_error
      val constrain_term_term_exn : Ctx.t -> untyped -> untyped -> unit
      val constrain_term_type_exn : Ctx.t -> untyped -> LogtkType.t -> unit
      val constrain_term_term : Ctx.t -> untyped -> untyped -> unit or_error
      val constrain_term_type :
        Ctx.t -> untyped -> LogtkType.t -> unit or_error
      val constrain :
        ctx:LogtkTypeInference.Ctx.t ->
        untyped -> unit LogtkTypeInference.or_error
      val convert :
        ?generalize:bool ->
        ?ret:LogtkType.t ->
        ctx:LogtkTypeInference.Ctx.t ->
        untyped -> typed LogtkTypeInference.or_error
      val convert_seq :
        ?generalize:bool ->
        ctx:LogtkTypeInference.Ctx.t ->
        untyped Sequence.t -> typed list LogtkTypeInference.or_error
      val constrain_exn : ctx:LogtkTypeInference.Ctx.t -> untyped -> unit
      val convert_exn :
        ?generalize:bool ->
        ?ret:LogtkType.t -> ctx:LogtkTypeInference.Ctx.t -> untyped -> typed
      val convert_seq_exn :
        ?generalize:bool ->
        ctx:LogtkTypeInference.Ctx.t -> untyped Sequence.t -> typed list
    end
end