# Generated by tools/translator: qualified upstream name -> MoonBit name.
ACS acs_v1
ACS_BOUNDS acs_bounds
ACS_BOUNDS_LT acs_bounds_lt
ACS_COS acs_cos
ACS_MONO_LT acs_mono_lt
ASN asn_v1
ASN_BOUNDS asn_bounds
ASN_BOUNDS_LT asn_bounds_lt
ASN_SIN asn_sin
ATN atn_v1
ATN_0 atn_0
ATN_1 atn_1
ATN_BOUNDS atn_bounds
ATN_INJ atn_inj
ATN_LE_PI4 atn_le_pi4
ATN_LT_PI4 atn_lt_pi4
ATN_LT_PI4_NEG atn_lt_pi4_neg
ATN_LT_PI4_POS atn_lt_pi4_pos
ATN_MONO_LE_EQ atn_mono_le_eq
ATN_MONO_LT atn_mono_lt
ATN_MONO_LT_EQ atn_mono_lt_eq
ATN_NEG atn_neg
ATN_POS_LE atn_pos_le
ATN_POS_LT atn_pos_lt
ATN_TAN atn_tan
CIRCLE_SINCOS circle_sincos
CONTINUOUS_CONV continuous_conv
CONTINUOUS_RULE continuous_rule
COS_0 cos_0
COS_2 cos_2
COS_ABS cos_abs
COS_ACS cos_acs
COS_ADD cos_add
COS_ASN_NZ cos_asn_nz
COS_ATN_NZ cos_atn_nz
COS_BOUND cos_bound
COS_BOUNDS cos_bounds
COS_CONVERGES cos_converges
COS_DOUBLE cos_double
COS_FDIFF cos_fdiff
COS_ISZERO cos_iszero
COS_NEG cos_neg
COS_NPI cos_npi
COS_ONE_2PI cos_one_2pi
COS_PAIRED cos_paired
COS_PERIODIC cos_periodic
COS_PERIODIC_PI cos_periodic_pi
COS_PI cos_pi
COS_PI2 cos_pi2
COS_POS_PI cos_pos_pi
COS_POS_PI2 cos_pos_pi2
COS_SIN cos_sin
COS_SIN_SQRT cos_sin_sqrt
COS_TOTAL cos_total
COS_ZERO cos_zero
COS_ZERO_LEMMA cos_zero_lemma
DEFINT_0 defint_0
DEFINT_ADD defint_add
DEFINT_CMUL defint_cmul
DEFINT_COMBINE defint_combine
DEFINT_CONST defint_const
DEFINT_DELTA defint_delta
DEFINT_DELTA_LEFT defint_delta_left
DEFINT_DELTA_RIGHT defint_delta_right
DEFINT_EQ defint_eq
DEFINT_FINITE_SPIKE defint_finite_spike
DEFINT_INTEGRAL defint_integral
DEFINT_LE defint_le
DEFINT_NEG defint_neg
DEFINT_POINT_SPIKE defint_point_spike
DEFINT_SUB defint_sub
DEFINT_TRIANGLE defint_triangle
DEFINT_WRONG defint_wrong
DIFFERENTIABLE_CONV differentiable_conv
DIFFERENTIABLE_RULE differentiable_rule
DIFFS_EQUIV diffs_equiv
DIFFS_LEMMA diffs_lemma
DIFFS_LEMMA2 diffs_lemma2
DIFFS_NEG diffs_neg
DIFF_ACS diff_acs
DIFF_ACS_SIN diff_acs_sin
DIFF_ASN diff_asn
DIFF_ASN_COS diff_asn_cos
DIFF_ATN diff_atn
DIFF_COMPOSITE diff_composite
DIFF_CONV diff_conv
DIFF_COS diff_cos
DIFF_EXP diff_exp
DIFF_LN diff_ln
DIFF_SIN diff_sin
DIFF_SQRT diff_sqrt
DIFF_TAC diff_tac
DIFF_TAN diff_tan
DINT_UNIQ dint_uniq
DIVISION_0 division_0
DIVISION_1 division_1
DIVISION_APPEND division_append
DIVISION_APPEND_EXPLICIT division_append_explicit
DIVISION_APPEND_LEMMA1 division_append_lemma1
DIVISION_APPEND_LEMMA2 division_append_lemma2
DIVISION_APPEND_STRONG division_append_strong
DIVISION_BOUNDS division_bounds
DIVISION_DSIZE_EQ division_dsize_eq
DIVISION_DSIZE_EQ_ALT division_dsize_eq_alt
DIVISION_DSIZE_GE division_dsize_ge
DIVISION_DSIZE_LE division_dsize_le
DIVISION_EQ division_eq
DIVISION_EXISTS division_exists
DIVISION_GT division_gt
DIVISION_INTERMEDIATE division_intermediate
DIVISION_LBOUND division_lbound
DIVISION_LBOUND_LT division_lbound_lt
DIVISION_LE division_le
DIVISION_LE_SUC division_le_suc
DIVISION_LHS division_lhs
DIVISION_LT division_lt
DIVISION_LT_GEN division_lt_gen
DIVISION_MONO_LE division_mono_le
DIVISION_MONO_LE_SUC division_mono_le_suc
DIVISION_RHS division_rhs
DIVISION_SINGLE division_single
DIVISION_THM division_thm
DIVISION_UBOUND division_ubound
DIVISION_UBOUND_LT division_ubound_lt
EVEN_DIV2 even_div2
EXP_LN exp_ln
EXT_CONV ext_conv
FINE_MIN fine_min
FTC1 ftc1
GAUGE_MIN gauge_min
GAUGE_MIN_FINITE gauge_min_finite
INTEGRABLE_CAUCHY integrable_cauchy
INTEGRABLE_COMBINE integrable_combine
INTEGRABLE_CONST integrable_const
INTEGRABLE_CONTINUOUS integrable_continuous
INTEGRABLE_CONV integrable_conv
INTEGRABLE_DEFINT integrable_defint
INTEGRABLE_LIMIT integrable_limit
INTEGRABLE_POINT_SPIKE integrable_point_spike
INTEGRABLE_RULE integrable_rule
INTEGRABLE_SPLIT_SIDES integrable_split_sides
INTEGRABLE_SUBINTERVAL integrable_subinterval
INTEGRABLE_SUBINTERVAL_LEFT integrable_subinterval_left
INTEGRABLE_SUBINTERVAL_RIGHT integrable_subinterval_right
INTEGRAL_ADD integral_add
INTEGRAL_BY_PARTS integral_by_parts
INTEGRAL_CMUL integral_cmul
INTEGRAL_CONST integral_const
INTEGRAL_EQ integral_eq
INTEGRAL_LE integral_le
INTEGRAL_NULL integral_null
INTEGRAL_SUB integral_sub
INTEGRATION_BY_PARTS integration_by_parts
LESS_1 less_1
LESS_SUC_EQ less_suc_eq
LE_MATCH_TAC le_match_tac
LN_1 ln_1
LN_DIV ln_div
LN_EXP ln_exp
LN_INJ ln_inj
LN_INV ln_inv
LN_LE ln_le
LN_LT_X ln_lt_x
LN_MONO_LE ln_mono_le
LN_MONO_LT ln_mono_lt
LN_MUL ln_mul
LN_POS ln_pos
LN_POS_LT ln_pos_lt
LN_POW ln_pow
MCLAURIN mclaurin
MCLAURIN_ALL_LE mclaurin_all_le
MCLAURIN_ALL_LT mclaurin_all_lt
MCLAURIN_ATN mclaurin_atn
MCLAURIN_BI_LE mclaurin_bi_le
MCLAURIN_COS mclaurin_cos
MCLAURIN_EXP_LE mclaurin_exp_le
MCLAURIN_EXP_LEMMA mclaurin_exp_lemma
MCLAURIN_EXP_LT mclaurin_exp_lt
MCLAURIN_LN_NEG mclaurin_ln_neg
MCLAURIN_LN_POS mclaurin_ln_pos
MCLAURIN_NEG mclaurin_neg
MCLAURIN_SIN mclaurin_sin
MCLAURIN_ZERO mclaurin_zero
MULT_DIV_2 mult_div_2
PI2 pi2
PI2_BOUNDS pi2_bounds
PI2_PI4 pi2_pi4
PI_POS pi_pos
POWDIFF powdiff
POWDIFF_LEMMA powdiff_lemma
POWREV powrev
POWSER_0 powser_0
POWSER_EQUAL powser_equal
POWSER_EQUAL_0 powser_equal_0
POWSER_INSIDE powser_inside
POWSER_INSIDEA powser_insidea
POWSER_LIMIT_0 powser_limit_0
POWSER_LIMIT_0_STRONG powser_limit_0_strong
POW_EQ pow_eq
POW_LT pow_lt
POW_ROOT_POS pow_root_pos
POW_ZERO pow_zero
POW_ZERO_EQ pow_zero_eq
REAL_ATN_POWSER real_atn_powser
REAL_ATN_POWSER_DIFFL real_atn_powser_diffl
REAL_ATN_POWSER_DIFFS_DIFFS_SUMMABLE real_atn_powser_diffs_diffs_summable
REAL_ATN_POWSER_DIFFS_SUM real_atn_powser_diffs_sum
REAL_ATN_POWSER_DIFFS_SUMMABLE real_atn_powser_diffs_summable
REAL_ATN_POWSER_SUMMABLE real_atn_powser_summable
REAL_DIV_SQRT real_div_sqrt
REAL_EXP_0 real_exp_0
REAL_EXP_ADD real_exp_add
REAL_EXP_ADD_MUL real_exp_add_mul
REAL_EXP_BOUND_LEMMA real_exp_bound_lemma
REAL_EXP_CONVERGES real_exp_converges
REAL_EXP_FDIFF real_exp_fdiff
REAL_EXP_INJ real_exp_inj
REAL_EXP_LE_X real_exp_le_x
REAL_EXP_LN real_exp_ln
REAL_EXP_LT_1 real_exp_lt_1
REAL_EXP_MONO_IMP real_exp_mono_imp
REAL_EXP_MONO_LE real_exp_mono_le
REAL_EXP_MONO_LT real_exp_mono_lt
REAL_EXP_N real_exp_n
REAL_EXP_NEG real_exp_neg
REAL_EXP_NEG_MUL real_exp_neg_mul
REAL_EXP_NEG_MUL2 real_exp_neg_mul2
REAL_EXP_NZ real_exp_nz
REAL_EXP_POS_LE real_exp_pos_le
REAL_EXP_POS_LT real_exp_pos_lt
REAL_EXP_SUB real_exp_sub
REAL_EXP_TOTAL real_exp_total
REAL_EXP_TOTAL_LEMMA real_exp_total_lemma
ROOT_0 root_0
ROOT_1 root_1
ROOT_DIV root_div
ROOT_INJ root_inj
ROOT_INV root_inv
ROOT_LN root_ln
ROOT_LT_LEMMA root_lt_lemma
ROOT_MONO_LE root_mono_le
ROOT_MONO_LE_EQ root_mono_le_eq
ROOT_MONO_LT root_mono_lt
ROOT_MONO_LT_EQ root_mono_lt_eq
ROOT_MUL root_mul
ROOT_POS_POSITIVE root_pos_positive
ROOT_POS_UNIQ root_pos_uniq
ROOT_POW_POS root_pow_pos
RSUM_BOUND rsum_bound
RSUM_DIFF_BOUND rsum_diff_bound
SEQ_NPOW seq_npow
SIN_0 sin_0
SIN_ACS_NZ sin_acs_nz
SIN_ADD sin_add
SIN_ASN sin_asn
SIN_BOUND sin_bound
SIN_BOUNDS sin_bounds
SIN_CIRCLE sin_circle
SIN_CONVERGES sin_converges
SIN_COS sin_cos
SIN_COS_ADD sin_cos_add
SIN_COS_NEG sin_cos_neg
SIN_COS_SQRT sin_cos_sqrt
SIN_DOUBLE sin_double
SIN_FDIFF sin_fdiff
SIN_NEG sin_neg
SIN_NEGLEMMA sin_neglemma
SIN_NPI sin_npi
SIN_PAIRED sin_paired
SIN_PERIODIC sin_periodic
SIN_PERIODIC_PI sin_periodic_pi
SIN_PI sin_pi
SIN_PI2 sin_pi2
SIN_POS sin_pos
SIN_POS_PI sin_pos_pi
SIN_POS_PI2 sin_pos_pi2
SIN_POS_PI_LE sin_pos_pi_le
SIN_TOTAL sin_total
SIN_ZERO sin_zero
SIN_ZERO_LEMMA sin_zero_lemma
SIN_ZERO_PI sin_zero_pi
SQRT_EVEN_POW2 sqrt_even_pow2
STRADDLE_LEMMA straddle_lemma
SUM_DIFFS sum_diffs
SYM_CANON_CONV sym_canon_conv
TAN_0 tan_0
TAN_ABS_GE_X tan_abs_ge_x
TAN_ADD tan_add
TAN_ATN tan_atn
TAN_BOUND_PI2 tan_bound_pi2
TAN_COT tan_cot
TAN_DOUBLE tan_double
TAN_NEG tan_neg
TAN_NPI tan_npi
TAN_PERIODIC tan_periodic
TAN_PERIODIC_NPI tan_periodic_npi
TAN_PERIODIC_PI tan_periodic_pi
TAN_PI tan_pi
TAN_PI4 tan_pi4
TAN_POS_PI2 tan_pos_pi2
TAN_SEC tan_sec
TAN_TOTAL tan_total
TAN_TOTAL_LEMMA tan_total_lemma
TAN_TOTAL_POS tan_total_pos
TDIV_BOUNDS tdiv_bounds
TDIV_LE tdiv_le
TERMDIFF termdiff
TERMDIFF_CONVERGES termdiff_converges
TERMDIFF_LEMMA1 termdiff_lemma1
TERMDIFF_LEMMA2 termdiff_lemma2
TERMDIFF_LEMMA3 termdiff_lemma3
TERMDIFF_LEMMA4 termdiff_lemma4
TERMDIFF_LEMMA5 termdiff_lemma5
TERMDIFF_STRONG termdiff_strong
acs acs
add_to_diff_net add_to_diff_net
asn asn
atn atn
cos cos
defint defint
diff_net diff_net
diffs diffs
division division
dsize dsize
exp exp
fine fine
gauge gauge
integrable integrable
integral integral
ln ln
pi pi
root root
rsum rsum
sin sin
tan tan
tdiv tdiv
