sig
  type 'a printer = Format.formatter -> 'a -> unit
  type 'a prec_printer = TermInner.prec -> 'a Model.printer
  type 'a to_sexp = 'a -> Sexp_lib.t
  module DT :
    sig
      type (+'t, +'ty) t = private
          Yield of 't
        | Cases of ('t, 'ty) Model.DT.cases
      and ('t, 'ty) cases = {
        var : 'ty Var.t;
        tests : ('t, 'ty) Model.DT.case list;
        default : ('t, 'ty) Model.DT.t option;
      }
      and ('t, 'ty) case = 't * ('t, 'ty) Model.DT.t
      val yield : 't -> ('t, 'a) Model.DT.t
      val const :
        'ty Var.t list -> ('t, 'ty) Model.DT.t -> ('t, 'ty) Model.DT.t
      val cases :
        'ty Var.t ->
        tests:('t, 'ty) Model.DT.case list ->
        default:('t, 'ty) Model.DT.t option -> ('t, 'ty) Model.DT.t
      val map :
        term:('t1 -> 't2) ->
        ty:('ty1 -> 'ty2) -> ('t1, 'ty1) Model.DT.t -> ('t2, 'ty2) Model.DT.t
      val filter_map :
        test:('ty Var.t -> 't1 -> 't2 option) ->
        yield:('t1 -> 't2) -> ('t1, 'ty) Model.DT.t -> ('t2, 'ty) Model.DT.t
      val ty_args : ('a, 'ty) Model.DT.t -> 'ty list
      val vars : ('a, 'ty) Model.DT.t -> 'ty Var.t list
      val num_vars : ('a, 'b) Model.DT.t -> int
      val add_default : 't -> ('t, 'ty) Model.DT.t -> ('t, 'ty) Model.DT.t
      type ('t, 'ty) flat_test = { ft_var : 'ty Var.t; ft_term : 't; }
      type ('t, 'ty) flat_dt = {
        fdt_vars : 'ty Var.t list;
        fdt_cases : (('t, 'ty) Model.DT.flat_test list * 't) list;
        fdt_default : 't option;
      }
      val mk_flat_test : 'ty Var.t -> 't -> ('t, 'ty) Model.DT.flat_test
      val of_flat :
        equal:('t -> 't -> bool) ->
        hash:('t -> int) ->
        ('t, 'ty) Model.DT.flat_dt -> ('t, 'ty) Model.DT.t
      val flatten : ('t, 'ty) Model.DT.t -> ('t, 'ty) Model.DT.flat_dt
      val check_ : ('a, 'b) Model.DT.t -> unit
      val print :
        't Model.prec_printer ->
        'ty Model.printer -> ('t, 'ty) Model.DT.t Model.printer
      val print_flat_test :
        't Model.prec_printer -> ('t, 'a) Model.DT.flat_test Model.printer
      val print_flat :
        't Model.prec_printer -> ('t, 'a) Model.DT.flat_dt Model.printer
      val to_sexp :
        't Model.to_sexp ->
        'ty Model.to_sexp -> ('t, 'ty) Model.DT.t Model.to_sexp
    end
  module DT_util :
    sig
      type term = TermInner.Default.t
      type dt = (Model.DT_util.term, Model.DT_util.term) Model.DT.t
      type subst = (Model.DT_util.term, Model.DT_util.term) Var.Subst.t
      val ite :
        Model.DT_util.term Var.t ->
        then_:Model.DT_util.dt -> else_:Model.DT_util.dt -> Model.DT_util.dt
      val eval_subst :
        subst:Model.DT_util.subst -> Model.DT_util.dt -> Model.DT_util.dt
      val map_vars :
        subst:(Model.DT_util.term, Model.DT_util.term Var.t) Var.Subst.t ->
        Model.DT_util.dt -> Model.DT_util.dt
      val rename_vars : Model.DT_util.dt -> Model.DT_util.dt
      val apply : Model.DT_util.dt -> Model.DT_util.term -> Model.DT_util.dt
      val apply_l :
        Model.DT_util.dt -> Model.DT_util.term list -> Model.DT_util.dt
      val join : Model.DT_util.dt -> Model.DT_util.dt -> Model.DT_util.dt
      val merge : Model.DT_util.dt -> Model.DT_util.dt -> Model.DT_util.dt
      val merge_l : Model.DT_util.dt list -> Model.DT_util.dt
      val reorder :
        Model.DT_util.term Var.t list -> Model.DT_util.dt -> Model.DT_util.dt
      val remove_vars :
        Model.DT_util.term Var.t list -> Model.DT_util.dt -> Model.DT_util.dt
      val remove_first_var : Model.DT_util.dt -> Model.DT_util.dt
      exception Case_not_found of Model.DT_util.term
      val find_cases :
        ?subst:Model.DT_util.subst ->
        Model.DT_util.term ->
        (Model.DT_util.term, Model.DT_util.term) Model.DT.cases ->
        Model.DT_util.subst * Model.DT_util.dt
      val to_term : Model.DT_util.dt -> Model.DT_util.term
      val print : Model.DT_util.dt Model.printer
    end
  type symbol_kind =
      Symbol_prop
    | Symbol_fun
    | Symbol_utype
    | Symbol_data
    | Symbol_codata
  type ('t, 'ty) value_def = 't * ('t, 'ty) Model.DT.t * Model.symbol_kind
  type ('t, 'ty) t = {
    values : ('t, 'ty) Model.value_def list;
    finite_types : ('ty * ID.t list) list;
    potentially_spurious : bool;
  }
  type ('a, 'b) model = ('a, 'b) Model.t
  val empty : ('a, 'b) Model.t
  val empty_copy : ('t, 'ty) Model.t -> ('t, 'ty) Model.t
  val add_const :
    ('t, 'ty) Model.t -> 't * 't * Model.symbol_kind -> ('t, 'ty) Model.t
  val add_value :
    ('t, 'ty) Model.t ->
    't * ('t, 'ty) Model.DT.t * Model.symbol_kind -> ('t, 'ty) Model.t
  val add_finite_type :
    ('t, 'ty) Model.t -> 'ty -> ID.t list -> ('t, 'ty) Model.t
  val values :
    ('t, 'ty) Model.t ->
    ('t * ('t, 'ty) Model.DT.t * Model.symbol_kind) Sequence.t
  val finite_types : ('a, 'ty) Model.t -> ('ty * ID.t list) Sequence.t
  val fold :
    ?values:('acc -> 'a * ('a, 'b) Model.DT.t * Model.symbol_kind -> 'acc) ->
    ?finite_types:('acc -> 'b * ID.t list -> 'acc) ->
    'acc -> ('a, 'b) Model.t -> 'acc
  val iter :
    ?values:('a * ('a, 'b) Model.DT.t * Model.symbol_kind -> unit) ->
    ?finite_types:('b * ID.t list -> unit) -> ('a, 'b) Model.t -> unit
  val filter_map :
    values:('t1 * ('t1, 'ty1) Model.DT.t * Model.symbol_kind ->
            ('t2 * ('t2, 'ty2) Model.DT.t * Model.symbol_kind) option) ->
    finite_types:('ty1 * ID.t list -> ('ty2 * ID.t list) option) ->
    ('t1, 'ty1) Model.t -> ('t2, 'ty2) Model.t
  val map :
    term:('t1 -> 't2) ->
    ty:('ty1 -> 'ty2) -> ('t1, 'ty1) Model.t -> ('t2, 'ty2) Model.t
  val filter :
    ?values:('t * ('t, 'ty) Model.DT.t * Model.symbol_kind -> bool) ->
    ?finite_types:('ty * ID.t list -> bool) ->
    ('t, 'ty) Model.t -> ('t, 'ty) Model.t
  val print :
    't Model.prec_printer ->
    'ty Model.printer -> ('t, 'ty) Model.t Model.printer
  val to_sexp :
    't Model.to_sexp -> 'ty Model.to_sexp -> ('t, 'ty) Model.t Model.to_sexp
  module Default :
    sig
      type term = TermInner.Default.t
      type t = (Model.Default.term, Model.Default.term) Model.model
      val to_sexp : Model.Default.t Model.to_sexp
      val print_standard : Model.Default.t Model.printer
    end
end