# Generated by tools/translator: qualified upstream name -> MoonBit name.
ADMISSIBLE_ISUM admissible_isum
CARD_EQ_ISUM card_eq_isum
EXPAND_ISUM_CONV expand_isum_conv
INT_OF_REAL_THM int_of_real_thm
INT_SUB_POW int_sub_pow
INT_SUB_POW_L1 int_sub_pow_l1
INT_SUB_POW_R1 int_sub_pow_r1
ISUM_0 isum_0
ISUM_ABS isum_abs
ISUM_ABS_BOUND isum_abs_bound
ISUM_ABS_LE isum_abs_le
ISUM_ABS_NUMSEG isum_abs_numseg
ISUM_ADD isum_add
ISUM_ADD_NUMSEG isum_add_numseg
ISUM_ADD_SPLIT isum_add_split
ISUM_BIJECTION isum_bijection
ISUM_BOUND isum_bound
ISUM_BOUND_LT isum_bound_lt
ISUM_BOUND_LT_ALL isum_bound_lt_all
ISUM_CASES isum_cases
ISUM_CLAUSES_LEFT isum_clauses_left
ISUM_CLAUSES_NUMSEG isum_clauses_numseg
ISUM_CLAUSES_RIGHT isum_clauses_right
ISUM_CLOSED isum_closed
ISUM_CLOSED_NONEMPTY isum_closed_nonempty
ISUM_COMBINE_L isum_combine_l
ISUM_COMBINE_R isum_combine_r
ISUM_CONST isum_const
ISUM_CONST_NUMSEG isum_const_numseg
ISUM_DELETE isum_delete
ISUM_DELETE_CASES isum_delete_cases
ISUM_DELTA isum_delta
ISUM_DIFF isum_diff
ISUM_DIFFS isum_diffs
ISUM_EQ isum_eq
ISUM_EQ_0 isum_eq_0
ISUM_EQ_0_NUMSEG isum_eq_0_numseg
ISUM_EQ_GENERAL isum_eq_general
ISUM_EQ_GENERAL_INVERSES isum_eq_general_inverses
ISUM_EQ_NUMSEG isum_eq_numseg
ISUM_EQ_SUPERSET isum_eq_superset
ISUM_GROUP isum_group
ISUM_IMAGE isum_image
ISUM_IMAGE_GEN isum_image_gen
ISUM_IMAGE_LE isum_image_le
ISUM_IMAGE_NONZERO isum_image_nonzero
ISUM_INCL_EXCL isum_incl_excl
ISUM_INJECTION isum_injection
ISUM_ISUM_PRODUCT isum_isum_product
ISUM_ISUM_RESTRICT isum_isum_restrict
ISUM_LE isum_le
ISUM_LE_INCLUDED isum_le_included
ISUM_LE_NUMSEG isum_le_numseg
ISUM_LMUL isum_lmul
ISUM_LT isum_lt
ISUM_LT_ALL isum_lt_all
ISUM_MULTICOUNT isum_multicount
ISUM_MULTICOUNT_GEN isum_multicount_gen
ISUM_NEG isum_neg
ISUM_OFFSET isum_offset
ISUM_OFFSET_0 isum_offset_0
ISUM_PARTIAL_PRE isum_partial_pre
ISUM_PARTIAL_SUC isum_partial_suc
ISUM_POS_BOUND isum_pos_bound
ISUM_POS_EQ_0 isum_pos_eq_0
ISUM_POS_EQ_0_NUMSEG isum_pos_eq_0_numseg
ISUM_POS_LE isum_pos_le
ISUM_POS_LE_NUMSEG isum_pos_le_numseg
ISUM_RELATED isum_related
ISUM_RELATED_NONEMPTY isum_related_nonempty
ISUM_RESTRICT isum_restrict
ISUM_RESTRICT_SET isum_restrict_set
ISUM_RMUL isum_rmul
ISUM_SING isum_sing
ISUM_SING_NUMSEG isum_sing_numseg
ISUM_SUB isum_sub
ISUM_SUBSET isum_subset
ISUM_SUBSET_SIMPLE isum_subset_simple
ISUM_SUB_NUMSEG isum_sub_numseg
ISUM_SUPERSET isum_superset
ISUM_SUPPORT isum_support
ISUM_SWAP isum_swap
ISUM_SWAP_NUMSEG isum_swap_numseg
ISUM_TRIV_NUMSEG isum_triv_numseg
ISUM_UNION isum_union
ISUM_UNIONS_NONZERO isum_unions_nonzero
ISUM_UNION_EQ isum_union_eq
ISUM_UNION_LZERO isum_union_lzero
ISUM_UNION_NONZERO isum_union_nonzero
ISUM_UNION_RZERO isum_union_rzero
ISUM_UNIV isum_univ
ISUM_ZERO_EXISTS isum_zero_exists
REAL_OF_NUM_ISUM real_of_num_isum
REAL_OF_NUM_ISUM_NUMSEG real_of_num_isum_numseg
int_isum int_isum
