sig
  val bool_ty : Types.t
  val nat_ty : Types.t
  val lookup_env_opt :
    Typed_ast.env -> Name.t list -> Typed_ast.local_env option
  val lookup_env : Typed_ast.env -> Name.t list -> Typed_ast.local_env
  val env_apply :
    Typed_ast.env ->
    Ast.component option ->
    Name.t -> (Typed_ast.name_kind * Path.t * Ast.l) option
  val lookup_mod_descr_opt :
    Typed_ast.env -> Name.t list -> Name.t -> Typed_ast.mod_descr option
  val lookup_mod_descr :
    Typed_ast.env -> Name.t list -> Name.t -> Typed_ast.mod_descr
  val names_get_const :
    Typed_ast.env ->
    Name.t list -> Name.t -> Types.const_descr_ref * Typed_ast.const_descr
  val strings_get_const :
    Typed_ast.env ->
    string list -> string -> Types.const_descr_ref * Typed_ast.const_descr
  val get_const :
    Typed_ast.env -> string -> Types.const_descr_ref * Typed_ast.const_descr
  val const_exists : Typed_ast.env -> string -> bool
  val const_descr_to_kind :
    Types.const_descr_ref * Typed_ast.const_descr -> Typed_ast.name_kind
  val strings_get_const_id :
    Typed_ast.env ->
    Ast.l ->
    string list ->
    string ->
    Types.t list -> Types.const_descr_ref Types.id * Typed_ast.const_descr
  val get_const_id :
    Typed_ast.env ->
    Ast.l ->
    string ->
    Types.t list -> Types.const_descr_ref Types.id * Typed_ast.const_descr
  val strings_mk_const_exp :
    Typed_ast.env ->
    Ast.l -> string list -> string -> Types.t list -> Typed_ast.exp
  val mk_const_exp :
    Typed_ast.env -> Ast.l -> string -> Types.t list -> Typed_ast.exp
  val dest_field_types :
    Ast.l ->
    Typed_ast.env ->
    Types.const_descr_ref -> Types.t * Path.t * Typed_ast.const_descr
  val get_field_type_descr :
    Ast.l -> Typed_ast.env -> Types.const_descr_ref -> Types.type_descr
  val get_field_all_fields :
    Ast.l ->
    Typed_ast.env -> Types.const_descr_ref -> Types.const_descr_ref list
  val lookup_class_descr :
    Ast.l -> Typed_ast.env -> Path.t -> Types.class_descr
  val lookup_field_for_class_method :
    Ast.l ->
    Types.class_descr -> Types.const_descr_ref -> Types.const_descr_ref
  val lookup_inst_method_for_class_method :
    Ast.l -> Types.instance -> Types.const_descr_ref -> Types.const_descr_ref
  val class_descr_get_dict_type : Types.class_descr -> Types.t -> Types.t
  val class_all_methods_inlined_for_target :
    Ast.l -> Typed_ast.env -> Target.target -> Path.t -> bool
  val update_const_descr :
    Ast.l ->
    (Typed_ast.const_descr -> Typed_ast.const_descr) ->
    Types.const_descr_ref -> Typed_ast.env -> Typed_ast.env
  val c_env_store :
    Typed_ast.c_env ->
    Typed_ast.const_descr -> Typed_ast.c_env * Types.const_descr_ref
  val c_env_save :
    Typed_ast.c_env ->
    Types.const_descr_ref option ->
    Typed_ast.const_descr -> Typed_ast.c_env * Types.const_descr_ref
  val const_target_rep_to_loc : Typed_ast.const_target_rep -> Ast.l
  val const_target_rep_allow_override : Typed_ast.const_target_rep -> bool
  val type_target_rep_to_loc : Types.type_target_rep -> Ast.l
  val type_target_rep_allow_override : Types.type_target_rep -> bool
  val constant_descr_to_name :
    Target.target -> Typed_ast.const_descr -> bool * Name.t * Name.t option
  val const_descr_ref_to_ascii_name :
    Typed_ast.c_env -> Types.const_descr_ref -> Name.t
  val type_descr_to_name :
    Target.target -> Path.t -> Types.type_descr -> Name.t
  val constant_descr_rename :
    Target.non_ident_target ->
    Name.t ->
    Ast.l ->
    Typed_ast.const_descr -> Typed_ast.const_descr * (Ast.l * Name.t) option
  val mod_target_rep_rename :
    Target.non_ident_target ->
    string ->
    Name.t ->
    Ast.l ->
    Typed_ast.mod_target_rep Target.Targetmap.t ->
    Typed_ast.mod_target_rep Target.Targetmap.t
  val type_descr_rename :
    Target.non_ident_target ->
    Name.t ->
    Ast.l -> Types.type_descr -> Types.type_descr * (Ast.l * Name.t) option
  val type_defs_rename_type :
    Ast.l ->
    Types.type_defs ->
    Path.t -> Target.non_ident_target -> Name.t -> Types.type_defs
  val const_descr_has_target_rep :
    Target.target -> Typed_ast.const_descr -> bool
  val mk_name_lskips_annot :
    Ast.l -> Name.lskips_t -> Types.t -> Typed_ast.name_lskips_annot
  val dest_var_exp : Typed_ast.exp -> Name.t option
  val is_var_exp : Typed_ast.exp -> bool
  val dest_tup_exp : int option -> Typed_ast.exp -> Typed_ast.exp list option
  val is_tup_exp : int option -> Typed_ast.exp -> bool
  val is_var_tup_exp : Typed_ast.exp -> bool
  val mk_tf_exp : bool -> Typed_ast.exp
  val dest_tf_exp : Typed_ast.exp -> bool option
  val is_tf_exp : bool -> Typed_ast.exp -> bool
  val dest_const_exp : Typed_ast.exp -> Types.const_descr_ref Types.id option
  val is_const_exp : Typed_ast.exp -> bool
  val dest_num_exp : Typed_ast.exp -> int option
  val is_num_exp : Typed_ast.exp -> bool
  val mk_num_exp : Types.t -> int -> Typed_ast.exp
  val is_empty_backend_exp : Typed_ast.exp -> bool
  val mk_eq_exp :
    Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
  val mk_and_exp :
    Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
  val mk_and_exps : Typed_ast.env -> Typed_ast.exp list -> Typed_ast.exp
  val mk_le_exp :
    Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
  val mk_sub_exp :
    Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
  val mk_from_list_exp : Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp
  val mk_cross_exp :
    Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
  val mk_set_sigma_exp :
    Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
  val mk_set_filter_exp :
    Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
  val mk_set_image_exp :
    Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
  val mk_fun_exp : Typed_ast.pat list -> Typed_ast.exp -> Typed_ast.exp
  val mk_opt_fun_exp : Typed_ast.pat list -> Typed_ast.exp -> Typed_ast.exp
  val mk_app_exp :
    Ast.l ->
    Types.type_defs -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
  val mk_list_app_exp :
    Ast.l ->
    Types.type_defs -> Typed_ast.exp -> Typed_ast.exp list -> Typed_ast.exp
  val mk_eta_expansion_exp :
    Types.type_defs -> Name.t list -> Typed_ast.exp -> Typed_ast.exp
  val mk_paren_exp : Typed_ast.exp -> Typed_ast.exp
  val mk_opt_paren_exp : Typed_ast.exp -> Typed_ast.exp
  val may_need_paren : Typed_ast.exp -> bool
  val mk_case_exp :
    bool ->
    Ast.l ->
    Typed_ast.exp ->
    (Typed_ast.pat * Typed_ast.exp) list -> Types.t -> Typed_ast.exp
  val mk_let_exp :
    Ast.l -> Name.t * Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
  val mk_if_exp :
    Ast.l -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
  val mk_undefined_exp : Ast.l -> string -> Types.t -> Typed_ast.exp
  val mk_dummy_exp : Types.t -> Typed_ast.exp
  val dest_app_exp : Typed_ast.exp -> (Typed_ast.exp * Typed_ast.exp) option
  val strip_app_exp : Typed_ast.exp -> Typed_ast.exp * Typed_ast.exp list
  val dest_infix_exp :
    Typed_ast.exp -> (Typed_ast.exp * Typed_ast.exp * Typed_ast.exp) option
  val is_infix_exp : Typed_ast.exp -> bool
  val strip_infix_exp : Typed_ast.exp -> Typed_ast.exp * Typed_ast.exp list
  val strip_app_infix_exp :
    Typed_ast.exp -> Typed_ast.exp * Typed_ast.exp list * bool
  val is_type_def_abbrev : Typed_ast.def -> bool
  val is_type_def_record : Typed_ast.def -> bool
  type used_entities = {
    used_consts : Types.const_descr_ref list;
    used_consts_set : Types.Cdset.t;
    used_types : Path.t list;
    used_types_set : Types.Pset.t;
    used_modules : Path.t list;
    used_modules_set : Types.Pset.t;
    used_tnvars : Types.TNset.t;
  }
  val empty_used_entities : Typed_ast_syntax.used_entities
  val add_exp_entities :
    Typed_ast_syntax.used_entities ->
    Typed_ast.exp -> Typed_ast_syntax.used_entities
  val add_def_aux_entities :
    Target.target ->
    bool ->
    Typed_ast_syntax.used_entities ->
    Typed_ast.def_aux -> Typed_ast_syntax.used_entities
  val add_def_entities :
    Target.target ->
    bool ->
    Typed_ast_syntax.used_entities ->
    Typed_ast.def -> Typed_ast_syntax.used_entities
  val get_checked_modules_entities :
    Target.target ->
    bool -> Typed_ast.checked_module list -> Typed_ast_syntax.used_entities
  val remove_init_ws : Ast.lex_skips -> Ast.lex_skips * Ast.lex_skips
  val drop_init_ws : Ast.lex_skips -> Ast.lex_skips * Ast.lex_skips
  val space_init_ws : Ast.lex_skips -> Ast.lex_skips * Ast.lex_skips
  val space_com_init_ws : Ast.lex_skips -> Ast.lex_skips * Ast.lex_skips
  val strip_paren_typ_exp : Typed_ast.exp -> Typed_ast.exp
  val is_recursive_def : Typed_ast.def_aux -> bool * bool
  val try_termination_proof :
    Target.target ->
    Typed_ast.c_env -> Typed_ast.def_aux -> bool * bool * bool
  val is_pp_loc : Ast.l -> bool
  val is_pp_exp : Typed_ast.exp -> bool
  val is_pp_def : Typed_ast.def -> bool
  val val_def_get_name : Typed_ast.val_def -> Name.t option
  val val_def_get_class_constraints_no_target_rep :
    Typed_ast.env ->
    Target.target -> Typed_ast.val_def -> (Path.t * Types.tnvar) list
  val val_def_get_class_constraints :
    Typed_ast.env -> Typed_ast.val_def -> (Path.t * Types.tnvar) list
  val val_def_get_free_tnvars :
    Typed_ast.env -> Typed_ast.val_def -> Types.TNset.t
  val env_tag_to_string : Typed_ast.env_tag -> string
  val constr_family_to_id :
    Ast.l ->
    Typed_ast.env ->
    Types.t ->
    Types.constr_family_descr ->
    (Types.const_descr_ref Types.id list *
     (Types.t -> Types.const_descr_ref Types.id) option)
    option
  val check_constr_family :
    Ast.l -> Typed_ast.env -> Types.t -> Types.constr_family_descr -> unit
  val check_for_inline_cycles : Target.target -> Typed_ast.c_env -> unit
end