# Generated by tools/translator: qualified upstream name -> MoonBit name.
BOTTOM bottom
CONSTR constr
CONSTR_BOT constr_bot
CONSTR_IND constr_ind
CONSTR_INJ constr_inj
CONSTR_REC constr_rec
DEST_REC_INJ dest_rec_inj
EXISTS_OPTION_THM exists_option_thm
FCONS fcons
FCONS_UNDO fcons_undo
FNIL fnil
FORALL_OPTION_THM forall_option_thm
FORALL_UNWIND_CONV forall_unwind_conv
INJA inja
INJA_INJ inja_inj
INJF injf
INJF_INJ injf_inj
INJN injn
INJN_INJ injn_inj
INJP injp
INJP_INJ injp_inj
INJ_INVERSE2 inj_inverse2
ISO iso
ISO_FUN iso_fun
ISO_REFL iso_refl
ISO_USAGE iso_usage
MATCH_CONV match_conv
MK_REC_INJ mk_rec_inj
NUMPAIR numpair
NUMPAIR_DEST numpair_dest
NUMPAIR_INJ numpair_inj
NUMPAIR_INJ_LEMMA numpair_inj_lemma
NUMSUM numsum
NUMSUM_DEST numsum_dest
NUMSUM_INJ numsum_inj
OUTL outl
OUTR outr
UNWIND_CONV unwind_conv
ZBOT zbot
ZCONSTR zconstr
ZCONSTR_ZBOT zconstr_zbot
ZRECSPACE_CASES zrecspace_cases
ZRECSPACE_INDUCT zrecspace_induct
ZRECSPACE_RULES zrecspace_rules
basic_rectype_net basic_rectype_net
cases cases
define_type define_type
define_type_raw define_type_raw
distinctness distinctness
distinctness_store distinctness_store
extend_rectype_net extend_rectype_net
injectivity injectivity
injectivity_store injectivity_store
list_INDUCT list_induct
list_RECURSION list_recursion
option_DISTINCT option_distinct
option_INDUCT option_induct
option_INJ option_inj
option_RECURSION option_recursion
parse_inductive_type_specification parse_inductive_type_specification
prove_cases_thm prove_cases_thm
prove_constructors_distinct prove_constructors_distinct
prove_constructors_injective prove_constructors_injective
recspace_tydef recspace_tydef
sum_INDUCT sum_induct
sum_RECURSION sum_recursion
the_inductive_types the_inductive_types
