sig
  type id = ID.t
  type loc = Location.t
  type 'a printer = Format.formatter -> 'a -> unit
  type ('t, 'ty) def =
      Fun_def of ('t, 'ty) Statement.rec_defs * ('t, 'ty) Statement.rec_def *
        Env.loc option
    | Fun_spec of ('t, 'ty) Statement.spec_defs * Env.loc option
    | Data of [ `Codata | `Data ] * 'ty Statement.mutual_types *
        'ty Statement.tydef
    | Cstor of [ `Codata | `Data ] * 'ty Statement.mutual_types *
        'ty Statement.tydef * 'ty Statement.ty_constructor
    | Pred of [ `Not_wf | `Wf ] * [ `Copred | `Pred ] *
        ('t, 'ty) Statement.pred_def * ('t, 'ty) Statement.pred_def list *
        Env.loc option
    | Copy_ty of ('t, 'ty) Statement.copy
    | Copy_abstract of ('t, 'ty) Statement.copy
    | Copy_concrete of ('t, 'ty) Statement.copy
    | NoDef
  type ('t, 'ty) info = {
    ty : 'ty;
    decl_attrs : Statement.decl_attr list;
    loc : Env.loc option;
    def : ('t, 'ty) Env.def;
  }
  type ('t, 'ty) t = private { infos : ('t, 'ty) Env.info ID.PerTbl.t; }
  exception InvalidDef of Env.id * string
  val pp_invalid_def_ : exn Env.printer
  val create : ?size:int -> unit -> ('a, 'b) Env.t
  val loc : ('a, 'b) Env.info -> Env.loc option
  val def : ('t, 'ty) Env.info -> ('t, 'ty) Env.def
  val ty : ('a, 'ty) Env.info -> 'ty
  val is_fun : ('a, 'b) Env.info -> bool
  val is_rec : ('a, 'b) Env.info -> bool
  val is_data : ('a, 'b) Env.info -> bool
  val is_cstor : ('a, 'b) Env.info -> bool
  val is_not_def : ('a, 'b) Env.info -> bool
  val is_incomplete : ('a, 'b) Env.info -> bool
  val is_abstract : ('a, 'b) Env.info -> bool
  val declare :
    ?loc:Env.loc ->
    attrs:Statement.decl_attr list ->
    env:('t, 'ty) Env.t -> Env.id -> 'ty -> ('t, 'ty) Env.t
  val rec_funs :
    ?loc:Env.loc ->
    env:('t, 'ty) Env.t -> ('t, 'ty) Statement.rec_defs -> ('t, 'ty) Env.t
  val declare_rec_funs :
    ?loc:Env.loc ->
    env:('t, 'ty) Env.t -> ('t, 'ty) Statement.rec_defs -> ('t, 'ty) Env.t
  val spec_funs :
    ?loc:Env.loc ->
    env:('t, 'ty) Env.t -> ('t, 'ty) Statement.spec_defs -> ('t, 'ty) Env.t
  val def_data :
    ?loc:Env.loc ->
    env:('t, 'ty) Env.t ->
    kind:[ `Codata | `Data ] -> 'ty Statement.mutual_types -> ('t, 'ty) Env.t
  val def_preds :
    ?loc:Env.loc ->
    env:('t, 'ty) Env.t ->
    wf:[ `Not_wf | `Wf ] ->
    kind:[ `Copred | `Pred ] ->
    ('t, 'ty) Statement.pred_def list -> ('t, 'ty) Env.t
  val add_copy :
    ?loc:Env.loc ->
    env:('t, 'ty) Env.t -> ('t, 'ty) Statement.copy -> ('t, 'ty) Env.t
  val add_statement :
    env:('t, 'ty) Env.t -> ('t, 'ty) Statement.t -> ('t, 'ty) Env.t
  val add_statement_l :
    env:('t, 'ty) Env.t -> ('t, 'ty) Statement.t list -> ('t, 'ty) Env.t
  val find : env:('t, 'ty) Env.t -> Env.id -> ('t, 'ty) Env.info option
  exception UndefinedID of ID.t
  val find_exn : env:('t, 'ty) Env.t -> Env.id -> ('t, 'ty) Env.info
  val find_ty_exn : env:('t, 'ty) Env.t -> Env.id -> 'ty
  val find_ty : env:('t, 'ty) Env.t -> Env.id -> 'ty option
  module Util :
    functor (T : TermInner.S) ->
      sig
        type term = T.t
        type ty = T.t
        val ty :
          env:(Env.Util.term, Env.Util.ty) Env.t ->
          Env.Util.term -> Env.Util.ty TermInner.or_error
        val ty_exn :
          env:(Env.Util.term, Env.Util.ty) Env.t ->
          Env.Util.term -> Env.Util.ty
        val info_of_ty :
          env:(Env.Util.term, Env.Util.ty) Env.t ->
          Env.Util.ty ->
          (Env.Util.term, Env.Util.ty) Env.info TermInner.or_error
        exception No_head of Env.Util.ty
        val info_of_ty_exn :
          env:(Env.Util.term, Env.Util.ty) Env.t ->
          Env.Util.ty -> (Env.Util.term, Env.Util.ty) Env.info
      end
  val mem : env:('a, 'b) Env.t -> id:Env.id -> bool
  module Print :
    functor (Pt : TermInner.PRINT) (Pty : TermInner.PRINT) ->
      sig val print : (Pt.t, Pty.t) Env.t Env.printer end
end