# Generated by tools/translator: qualified upstream name -> MoonBit name.
Cop.Subst.empty empty_v1
Cop.Subst.eq eq
Cop.Subst.eq_lit eq_lit_v1
Cop.Subst.ground_lit ground_lit_v1
Cop.Subst.inst_lit inst_lit_v1
Cop.Subst.inst_tm inst_tm_v1
Cop.Subst.to_list to_list_v2
Cop.Subst.unify unify
Cop.Subst.unify_lit unify_lit_v1
Cop.Subst.unify_rename unify_rename
Cop.Subst.unify_rename_subst unify_rename_subst
Cop.Subst.unify_tms unify_tms_v1
Cop.Subst.unify_tms_off unify_tms_off_v1
Cop.deepen deepen
Cop.deepen_to deepen_to
Cop.search_opts search_opts
Cop.strategy strategy
Database.axioms2db axioms2db
Database.clause_max_var clause_max_var
Database.db db
Database.db_entries db_entries
Database.mapentry mapentry
Equality.create_eq_axs create_eq_axs
Equality.create_equality_axioms create_equality_axioms
Extclause.assert_iclause assert_iclause
Extclause.assert_imatrix assert_imatrix
Extclause.assert_matrix assert_matrix
Extclause.claBC_of_litmat_ext clabc_of_litmat_ext
Extclause.litext_of_clause_ext litext_of_clause_ext
Extclause.litext_of_litmat_ext litext_of_litmat_ext
Extclause.matBC_of_clause_ext matbc_of_clause_ext
Extclause.offset_clause_ext offset_clause_ext
Extclause.offset_iv offset_iv
Extclause.offset_litmat_ext offset_litmat_ext
Fol_term.lit_ground lit_ground
Fol_term.lit_max_var lit_max_var
Fol_term.map_lit_vars map_lit_vars
Fol_term.map_term map_term
Fol_term.map_term_vars map_term_vars
Fol_term.negate_lit negate_lit
Fol_term.term_ground term_ground
Fol_term.term_max_var term_max_var
Fol_term.var var_
Hashek.MARK_ASSUMS mark_assums
Hashek.MARK_CONCL mark_concl
Hashek.hashek_def hashek_def
Hashek.hashek_eq hashek_eq
Hashek.hashek_prop hashek_prop
Hashek.hashek_thm hashek_thm
Hashek.hashek_tm hashek_tm
LEANCOP leancop_v1
LEANCOP_TAC leancop_tac_v1
Leancop.GEN_LEANCOP_TAC gen_leancop_tac
Leancop.LEANCOP leancop
Leancop.LEANCOP_DEEPEN leancop_deepen
Leancop.LEANCOP_TAC leancop_tac
Leancop.PREPARE_LEAN_TAC prepare_lean_tac
Leancop.PURE_LEANCOP pure_leancop
Leancop.start start
NANOCOP nanocop_v1
NANOCOP_TAC nanocop_tac_v1
Nanocop.GEN_NANOCOP_TAC gen_nanocop_tac
Nanocop.NANOCOP nanocop
Nanocop.NANOCOP_DEEPEN nanocop_deepen
Nanocop.NANOCOP_TAC nanocop_tac
Nanocop.PREPARE_NANOCOP_TAC prepare_nanocop_tac
Nanocop.PRINT_ID_TAC print_id_tac
Nanocop.PRINT_TAC print_tac
Nanocop.PURE_NANOCOP pure_nanocop
Nanocop.fol_of_thm fol_of_thm
Nanocop.start start_v1
Ncdatabase.db db_v1
Ncdatabase.db_entries db_entries_v1
Ncdatabase.insert_db insert_db
Ncdatabase.matrix2db matrix2db
Ncmatrix.break_map break_map
Ncmatrix.clause_ground clause_ground
Ncmatrix.clause_lits clause_lits
Ncmatrix.clause_max_var clause_max_var_v1
Ncmatrix.clause_of_form clause_of_form
Ncmatrix.clause_of_matrix clause_of_matrix
Ncmatrix.clause_offset clause_offset
Ncmatrix.clause_positive clause_positive
Ncmatrix.copy_clause copy_clause
Ncmatrix.copy_matrix copy_matrix
Ncmatrix.iclause_max_var iclause_max_var
Ncmatrix.iclause_of_form iclause_of_form
Ncmatrix.iclause_offset iclause_offset
Ncmatrix.iclause_positive iclause_positive
Ncmatrix.imatrix_max_var imatrix_max_var
Ncmatrix.imatrix_positive imatrix_positive
Ncmatrix.index_clause index_clause
Ncmatrix.index_iclause index_iclause
Ncmatrix.index_imatrix index_imatrix
Ncmatrix.index_litmat index_litmat
Ncmatrix.index_matrix index_matrix_v1
Ncmatrix.lit lit
Ncmatrix.lit_of_litmat lit_of_litmat
Ncmatrix.lit_positive lit_positive
Ncmatrix.litmat_max_var litmat_max_var
Ncmatrix.litmat_of_form litmat_of_form
Ncmatrix.litmat_positive litmat_positive
Ncmatrix.map_clause map_clause
Ncmatrix.map_clause_vars map_clause_vars
Ncmatrix.map_iclause map_iclause
Ncmatrix.map_iclause_vars map_iclause_vars
Ncmatrix.map_imatrix map_imatrix
Ncmatrix.map_imatrix_vars map_imatrix_vars
Ncmatrix.map_litmat map_litmat
Ncmatrix.map_litmat_vars map_litmat_vars
Ncmatrix.map_matrix map_matrix
Ncmatrix.map_matrix_vars map_matrix_vars
Ncmatrix.mat mat
Ncmatrix.matrix_max_var matrix_max_var
Ncmatrix.matrix_of_form matrix_of_form
Ncmatrix.matrix_positive matrix_positive
Ncmatrix.offset_clause offset_clause
Ncmatrix.offset_iclause offset_iclause
Ncmatrix.offset_matrix offset_matrix
Ncmatrix.strip_conj strip_conj
Ncmatrix.strip_disj strip_disj
Ncmatrix.strip_forallq strip_forallq
Ncprint.pp_print_iclause pp_print_iclause
Ncprint.pp_print_imatrix pp_print_imatrix
Ncprint.pp_print_index pp_print_index
Ncprint.pp_print_litmat pp_print_litmat
Ncprint.pp_print_matrix pp_print_matrix
Ncprint.pp_print_matrix_ni pp_print_matrix_ni
Ncprint.pp_print_nclause pp_print_nclause
Ncprint.print_iclause print_iclause
Ncprint.print_iclause_i print_iclause_i
Ncprint.print_matrix_i print_matrix_i
Ncprint.print_nclause print_nclause
Ncprint.string_of_iclause string_of_iclause
Ncprint.string_of_iclause_i string_of_iclause_i
Ncprint.string_of_litmat string_of_litmat
Ncprint.string_of_matrix string_of_matrix
Ncprint.string_of_nclause string_of_nclause
Ncproof.pp_print_prf pp_print_prf
Ncproof.pp_print_proof pp_print_proof
Ncproof.pp_print_proofs pp_print_proofs
Ncproof.print_proof_def print_proof_def
Ncproof.print_proofa print_proofa
Ncproof.string_of_inst_litmat string_of_inst_litmat
Ncrecon.CONTRADICTION contradiction
Ncrecon.DISJ_CASES_LIST disj_cases_list
Ncrecon.bot_of_clause_ext bot_of_clause_ext
Ncrecon.bot_of_litmat_ext bot_of_litmat_ext
Ncrecon.bot_of_proof bot_of_proof
Ncrecon.clause_index_mapping clause_index_mapping
Ncrecon.eat_proofs eat_proofs
Ncrecon.flip_neg flip_neg
Ncrecon.inst_var inst_var
Ncrecon.matrix_index_mapping matrix_index_mapping
Ncrecon.mk_recon_data mk_recon_data
Ncrecon.nth_conj nth_conj
Ncrecon.nth_disj nth_disj
Ncrecon.prefix_problem prefix_problem
Ncrecon.spec_vars spec_vars
Ncsearch.cut cut_v2
Ncsearch.nth_clause nth_clause
Ncsearch.nth_matrix nth_matrix
Ncsearch.pick pick
Ncsearch.prove_clause prove_clause_v1
Ncsearch.prove_ec prove_ec
Ncsearch.prove_lit prove_lit_v1
Ncsearch.prove_litmat prove_litmat
Ncsearch.prove_mat prove_mat
Ncsearch.unify_rename unify_rename_v1
Ncsearch.unify_vars unify_vars
Ncsearch.unique unique
Prepare.PREPARE_COP_TAC prepare_cop_tac
Print.pp_enclose pp_enclose
Print.pp_enclose_cut pp_enclose_cut
Print.pp_enum pp_enum
Print.pp_interleave pp_interleave
Print.pp_iter pp_iter
Print.pp_iter_sp pp_iter_sp
Print.pp_nl pp_nl
Print.pp_print_fterm pp_print_fterm
Print.pp_print_lit pp_print_lit
Print.pp_print_null pp_print_null
Print.pp_print_var pp_print_var
Print.pp_with_box pp_with_box
Print.string_of_fterm string_of_fterm
Print.string_of_lit string_of_lit
Print.string_of_lits string_of_lits
Recon.hashek_of_proof hashek_of_proof
Recon.hol_negate hol_negate
Search.cut cut_v1
Search.prove_clause prove_clause
Search.prove_lit prove_lit
Strom.append append
Strom.cache cache
Strom.concat concat
Strom.concat_map concat_map
Strom.cons cons
Strom.cut cut
Strom.filter filter
Strom.filter_map filter_map
Strom.integers_from integers_from
Strom.iter iter
Strom.map map
Strom.mapi mapi
Strom.next_opt next_opt
Strom.nil nil
Strom.of_list of_list
Strom.take take
Strom.take_while take_while
Strom.to_list to_list
Substarray.add_subst add_subst_v1
Substarray.empty empty_v1
Substarray.eq_lit eq_lit_v1
Substarray.eq_tm eq_tm
Substarray.eq_var_tm eq_var_tm_v1
Substarray.ground_lit ground_lit_v1
Substarray.ground_tm ground_tm_v1
Substarray.inst_lit inst_lit_v1
Substarray.inst_term inst_term
Substarray.inst_tm inst_tm_v1
Substarray.istriv istriv_v1
Substarray.offset_vars offset_vars
Substarray.restore_subst restore_subst
Substarray.to_list to_list_v2
Substarray.unify_lit unify_lit_v1
Substarray.unify_tm unify_tm_v1
Substarray.unify_tm_off unify_tm_off_v1
Substarray.unify_tms unify_tms_v1
Substarray.unify_tms_off unify_tms_off_v1
Substlist.add_subst add_subst
Substlist.empty empty
Substlist.eq_lit eq_lit
Substlist.eq_term eq_term
Substlist.eq_terms eq_terms
Substlist.eq_var_tm eq_var_tm
Substlist.ground_lit ground_lit
Substlist.ground_tm ground_tm
Substlist.inst_lit inst_lit
Substlist.inst_tm inst_tm
Substlist.istriv istriv
Substlist.to_list to_list_v1
Substlist.unify_lit unify_lit
Substlist.unify_tm unify_tm
Substlist.unify_tm_off unify_tm_off
Substlist.unify_tms unify_tms
Substlist.unify_tms_off unify_tms_off
exn:Cop.Subst.Unify Unify1
exn:Strom.End_of_strom End_of_strom
exn:Substarray.Unify Unify1
exn:Substlist.Unify Unify
offset_lit offset_lit
offset_term offset_term
type:Cop.Subst.t T1
type:Cop.search_opts SearchOpts
type:Database.contrapositive Contrapositive
type:Extclause.clause_ext ClauseExt
type:Extclause.litmat_ext LitmatExt
type:Ncdatabase.contrapositive Contrapositive1
type:Ncmatrix.clause Clause
type:Ncmatrix.iclause Iclause
type:Ncmatrix.imatrix Imatrix
type:Ncmatrix.litmat Litmat
type:Ncmatrix.matrix Matrix
type:Ncproof.proof Proof1
type:Ncrecon.recon_data ReconData
type:Proof.proof Proof
type:Strom.strom Strom
type:Substarray.t T1
type:Substlist.t T
type:iterm Iterm
type:lit Lit
