sig
  type id = ID.t
  type loc = Location.t
  type 'a var = 'a Var.t
  type 'a printer = Format.formatter -> 'a -> unit
  type 'ty defined = { defined_head : Statement.id; defined_ty : 'ty; }
  type ('t, 'ty) equations =
      Eqn_nested of ('ty Statement.var list * 't list * 't * 't list) list
    | Eqn_single of 'ty Statement.var list * 't
    | Eqn_app of ID.t list * 'ty Statement.var list * 't * 't
  type ('t, 'ty) rec_def = {
    rec_defined : 'ty Statement.defined;
    rec_ty_vars : 'ty Statement.var list;
    rec_eqns : ('t, 'ty) Statement.equations;
  }
  type ('t, 'ty) rec_defs = ('t, 'ty) Statement.rec_def list
  type ('t, 'ty) spec_defs = {
    spec_ty_vars : 'ty Statement.var list;
    spec_defined : 'ty Statement.defined list;
    spec_axioms : 't list;
  }
  type 'ty ty_constructor = {
    cstor_name : Statement.id;
    cstor_args : 'ty list;
    cstor_type : 'ty;
  }
  type 'ty tydef = {
    ty_id : Statement.id;
    ty_vars : 'ty Var.t list;
    ty_type : 'ty;
    ty_cstors : 'ty Statement.ty_constructor ID.Map.t;
  }
  type 'ty mutual_types = 'ty Statement.tydef list
  type ('t, 'ty) axiom =
      Axiom_std of 't list
    | Axiom_spec of ('t, 'ty) Statement.spec_defs
    | Axiom_rec of ('t, 'ty) Statement.rec_defs
  type ('t, 'ty) pred_clause = {
    clause_vars : 'ty Statement.var list;
    clause_guard : 't option;
    clause_concl : 't;
  }
  type ('t, 'ty) pred_def = {
    pred_defined : 'ty Statement.defined;
    pred_tyvars : 'ty Statement.var list;
    pred_clauses : ('t, 'ty) Statement.pred_clause list;
  }
  type 't copy_wrt =
      Wrt_nothing
    | Wrt_subset of 't
    | Wrt_quotient of [ `Partial | `Total ] * 't
  type ('t, 'ty) copy = {
    copy_id : ID.t;
    copy_vars : 'ty Var.t list;
    copy_ty : 'ty;
    copy_of : 'ty;
    copy_to : 'ty;
    copy_wrt : 't Statement.copy_wrt;
    copy_abstract : ID.t;
    copy_abstract_ty : 'ty;
    copy_concrete : ID.t;
    copy_concrete_ty : 'ty;
  }
  type decl_attr =
      Attr_card_max of int
    | Attr_card_min of int
    | Attr_card_hint of Cardinality.t
    | Attr_incomplete
    | Attr_abstract
    | Attr_infinite
    | Attr_finite_approx of ID.t
    | Attr_infinite_upcast
    | Attr_pseudo_prop
    | Attr_pseudo_true
    | Attr_exn of exn
  type ('term, 'ty) view =
      Decl of Statement.id * 'ty * Statement.decl_attr list
    | Axiom of ('term, 'ty) Statement.axiom
    | TyDef of [ `Codata | `Data ] * 'ty Statement.mutual_types
    | Pred of [ `Not_wf | `Wf ] * [ `Copred | `Pred ] *
        ('term, 'ty) Statement.pred_def list
    | Copy of ('term, 'ty) Statement.copy
    | Goal of 'term
  type info = { loc : Statement.loc option; name : string option; }
  type (+'term, +'ty) t = private {
    view : ('term, 'ty) Statement.view;
    info : Statement.info;
  }
  type ('t, 'ty) statement = ('t, 'ty) Statement.t
  val mk_defined : ID.t -> 'ty -> 'ty Statement.defined
  val tydef_vars : 'ty Statement.tydef -> 'ty Var.t list
  val tydef_id : 'a Statement.tydef -> Statement.id
  val tydef_type : 'ty Statement.tydef -> 'ty
  val tydef_cstors :
    'ty Statement.tydef -> 'ty Statement.ty_constructor ID.Map.t
  val info_default : Statement.info
  val info_of_loc : Location.t option -> Statement.info
  val view : ('term, 'ty) Statement.t -> ('term, 'ty) Statement.view
  val loc : ('a, 'b) Statement.t -> Statement.loc option
  val name : ('a, 'b) Statement.t -> string option
  val info : ('a, 'b) Statement.t -> Statement.info
  val mk_axiom :
    info:Statement.info -> ('a, 'ty) Statement.axiom -> ('a, 'ty) Statement.t
  val mk_ty_def :
    info:Statement.info ->
    [ `Codata | `Data ] ->
    'ty Statement.mutual_types -> ('a, 'ty) Statement.t
  val decl :
    info:Statement.info ->
    attrs:Statement.decl_attr list ->
    Statement.id -> 'a -> ('b, 'a) Statement.t
  val axiom : info:Statement.info -> 'a list -> ('a, 'b) Statement.t
  val axiom1 : info:Statement.info -> 'a -> ('a, 'b) Statement.t
  val axiom_spec :
    info:Statement.info ->
    ('a, 'ty) Statement.spec_defs -> ('a, 'ty) Statement.t
  val axiom_rec :
    info:Statement.info ->
    ('a, 'ty) Statement.rec_defs -> ('a, 'ty) Statement.t
  val data :
    info:Statement.info ->
    'ty Statement.mutual_types -> ('a, 'ty) Statement.t
  val codata :
    info:Statement.info ->
    'ty Statement.mutual_types -> ('a, 'ty) Statement.t
  val pred :
    info:Statement.info ->
    wf:[ `Not_wf | `Wf ] ->
    ('t, 'ty) Statement.pred_def list -> ('t, 'ty) Statement.t
  val copred :
    info:Statement.info ->
    wf:[ `Not_wf | `Wf ] ->
    ('t, 'ty) Statement.pred_def list -> ('t, 'ty) Statement.t
  val mk_pred :
    info:Statement.info ->
    wf:[ `Not_wf | `Wf ] ->
    [ `Copred | `Pred ] ->
    ('t, 'ty) Statement.pred_def list -> ('t, 'ty) Statement.t
  val copy :
    info:Statement.info -> ('t, 'ty) Statement.copy -> ('t, 'ty) Statement.t
  val goal : info:Statement.info -> 'a -> ('a, 'b) Statement.t
  val mk_mutual_ty :
    ID.t ->
    ty_vars:'ty Var.t list ->
    cstors:(ID.t * 'ty list * 'ty) list -> ty:'ty -> 'ty Statement.tydef
  val mk_copy :
    wrt:'t Statement.copy_wrt ->
    of_:'ty ->
    to_:'ty ->
    ty:'ty ->
    abstract:ID.t * 'ty ->
    concrete:ID.t * 'ty ->
    vars:'ty Var.t list -> ID.t -> ('t, 'ty) Statement.copy
  val find_rec_def :
    defs:('a, 'b) Statement.rec_def list ->
    ID.t -> ('a, 'b) Statement.rec_def option
  val find_tydef :
    defs:'a Statement.tydef list -> ID.t -> 'a Statement.tydef option
  val find_pred :
    defs:('a, 'b) Statement.pred_def list ->
    ID.t -> ('a, 'b) Statement.pred_def option
  val map_defined :
    f:('ty -> 'ty2) -> 'ty Statement.defined -> 'ty2 Statement.defined
  val map_eqns :
    term:('t -> 't2) ->
    ty:('ty -> 'ty2) ->
    ('t, 'ty) Statement.equations -> ('t2, 'ty2) Statement.equations
  val map_eqns_bind :
    bind:('acc -> 'ty Var.t -> 'acc * 'ty1 Var.t) ->
    term:('acc -> 'term -> 'term1) ->
    'acc ->
    ('term, 'ty) Statement.equations -> ('term1, 'ty1) Statement.equations
  val map_clause :
    term:('t -> 't2) ->
    ty:('ty -> 'ty2) ->
    ('t, 'ty) Statement.pred_clause -> ('t2, 'ty2) Statement.pred_clause
  val map_clause_bind :
    bind:('acc -> 'ty Var.t -> 'acc * 'ty1 Var.t) ->
    term:('acc -> 'term -> 'term1) ->
    'acc ->
    ('term, 'ty) Statement.pred_clause ->
    ('term1, 'ty1) Statement.pred_clause
  val map_rec_def :
    term:('t -> 't2) ->
    ty:('ty -> 'ty2) ->
    ('t, 'ty) Statement.rec_def -> ('t2, 'ty2) Statement.rec_def
  val map_rec_def_bind :
    bind:('a -> 'b Var.t -> 'a * 'c Var.t) ->
    term:('a -> 'd -> 'e) ->
    ty:('a -> 'b -> 'c) ->
    'a -> ('d, 'b) Statement.rec_def -> ('e, 'c) Statement.rec_def
  val map_rec_defs :
    term:('t -> 't2) ->
    ty:('ty -> 'ty2) ->
    ('t, 'ty) Statement.rec_defs -> ('t2, 'ty2) Statement.rec_defs
  val map_ty_def :
    ty:('ty -> 'ty2) -> 'ty Statement.tydef -> 'ty2 Statement.tydef
  val map_ty_defs :
    ty:('ty -> 'ty2) ->
    'ty Statement.mutual_types -> 'ty2 Statement.mutual_types
  val map_spec_defs :
    term:('t -> 't2) ->
    ty:('ty -> 'ty2) ->
    ('t, 'ty) Statement.spec_defs -> ('t2, 'ty2) Statement.spec_defs
  val map_spec_defs_bind :
    bind:('b_acc -> 'ty Var.t -> 'b_acc * 'ty2 Var.t) ->
    term:('b_acc -> 't -> 't2) ->
    ty:('b_acc -> 'ty -> 'ty2) ->
    'b_acc ->
    ('t, 'ty) Statement.spec_defs -> ('t2, 'ty2) Statement.spec_defs
  val map_pred :
    term:('a -> 'a1) ->
    ty:('b -> 'b1) ->
    ('a, 'b) Statement.pred_def -> ('a1, 'b1) Statement.pred_def
  val map_pred_bind :
    bind:('acc -> 'ty Var.t -> 'acc * 'ty2 Var.t) ->
    term:('acc -> 'term -> 'term2) ->
    ty:('acc -> 'ty -> 'ty2) ->
    'acc ->
    ('term, 'ty) Statement.pred_def -> ('term2, 'ty2) Statement.pred_def
  val map_preds :
    term:('a -> 'a1) ->
    ty:('b -> 'b1) ->
    ('a, 'b) Statement.pred_def list -> ('a1, 'b1) Statement.pred_def list
  val map_copy_wrt :
    ('a -> 'b) -> 'a Statement.copy_wrt -> 'b Statement.copy_wrt
  val map_copy_bind :
    bind:('a -> 'b Statement.var -> 'a * 'c Statement.var) ->
    term:('a -> 'd -> 'e) ->
    ty:('a -> 'b -> 'c) ->
    'a -> ('d, 'b) Statement.copy -> ('e, 'c) Statement.copy
  val map_copy :
    term:('t1 -> 't2) ->
    ty:('ty1 -> 'ty2) ->
    ('t1, 'ty1) Statement.copy -> ('t2, 'ty2) Statement.copy
  val map :
    term:('t -> 't2) ->
    ty:('ty -> 'ty2) -> ('t, 'ty) Statement.t -> ('t2, 'ty2) Statement.t
  val map_bind :
    bind:('b_acc -> 'ty Var.t -> 'b_acc * 'ty2 Var.t) ->
    term:('b_acc -> 't -> 't2) ->
    ty:('b_acc -> 'ty -> 'ty2) ->
    'b_acc -> ('t, 'ty) Statement.t -> ('t2, 'ty2) Statement.t
  val fold_bind :
    bind:('b_acc -> 'ty Var.t -> 'b_acc) ->
    term:('b_acc -> 'a -> 't -> 'a) ->
    ty:('b_acc -> 'a -> 'ty -> 'a) ->
    'b_acc -> 'a -> ('t, 'ty) Statement.t -> 'a
  val fold :
    term:('a -> 't -> 'a) ->
    ty:('a -> 'ty -> 'a) -> 'a -> ('t, 'ty) Statement.t -> 'a
  val iter :
    term:('t -> unit) -> ty:('ty -> unit) -> ('t, 'ty) Statement.t -> unit
  val id_of_defined : 'a Statement.defined -> ID.t
  val ty_of_defined : 'ty Statement.defined -> 'ty
  val defined_of_rec : ('a, 'ty) Statement.rec_def -> 'ty Statement.defined
  val defined_of_recs :
    ('a, 'ty) Statement.rec_defs -> 'ty Statement.defined Sequence.t
  val defined_of_spec :
    ('a, 'ty) Statement.spec_defs -> 'ty Statement.defined Sequence.t
  val defined_of_pred : ('a, 'ty) Statement.pred_def -> 'ty Statement.defined
  val defined_of_preds :
    ('a, 'ty) Statement.pred_def list -> 'ty Statement.defined Sequence.t
  val defined_of_cstor :
    'ty Statement.ty_constructor -> 'ty Statement.defined
  val defined_of_data :
    'ty Statement.tydef -> 'ty Statement.defined Sequence.t
  val defined_of_datas :
    'ty Statement.mutual_types -> 'ty Statement.defined Sequence.t
  val defined_of_copy :
    ('a, 'ty) Statement.copy -> 'ty Statement.defined Sequence.t
  val ids_of_copy : ('a, 'b) Statement.copy -> ID.t Sequence.t
  val print_attr : Statement.decl_attr Statement.printer
  val print_attrs : Statement.decl_attr list Statement.printer
  module Print :
    functor (Pt : TermInner.PRINT) (Pty : TermInner.PRINT) ->
      sig
        val print_spec_defs :
          (Pt.t, Pty.t) Statement.spec_defs Statement.printer
        val print_clause :
          (Pt.t, Pty.t) Statement.pred_clause Statement.printer
        val print_clauses :
          (Pt.t, Pty.t) Statement.pred_clause list Statement.printer
        val print_pred_def :
          (Pt.t, Pty.t) Statement.pred_def Statement.printer
        val print_pred_defs :
          (Pt.t, Pty.t) Statement.pred_def list Statement.printer
        val print_eqns :
          ID.t -> (Pt.t, Pty.t) Statement.equations Statement.printer
        val print_rec_def : (Pt.t, Pty.t) Statement.rec_def Statement.printer
        val print_rec_defs :
          (Pt.t, Pty.t) Statement.rec_def list Statement.printer
        val print_tydef : Pty.t Statement.tydef Statement.printer
        val print_tydefs :
          ([ `Codata | `Data ] * Pty.t Statement.tydef list)
          Statement.printer
        val print_copy : (Pt.t, Pty.t) Statement.copy Statement.printer
        val print : (Pt.t, Pty.t) Statement.t Statement.printer
      end
end