# Generated by tools/translator: qualified upstream name -> MoonBit name.
APPROX_EXP approx_exp
APPROX_LEMMA1 approx_lemma1
APPROX_LN approx_ln
ELIMINATE_DEF eliminate_def
EXPAND_RANGE_CONV expand_range_conv
MCLAURIN_EXP_LE1 mclaurin_exp_le1
REALCALC_ABS realcalc_abs
REALCALC_ADD realcalc_add
REALCALC_CONV realcalc_conv
REALCALC_DOWNGRADE realcalc_downgrade
REALCALC_EQ realcalc_eq
REALCALC_GE realcalc_ge
REALCALC_GT realcalc_gt
REALCALC_INT realcalc_int
REALCALC_INV realcalc_inv
REALCALC_INV_LEMMA realcalc_inv_lemma
REALCALC_LE realcalc_le
REALCALC_LT realcalc_lt
REALCALC_MUL realcalc_mul
REALCALC_NEG realcalc_neg
REALCALC_PRECONV realcalc_preconv
REALCALC_REL_CONV realcalc_rel_conv_v1
REALCALC_SQRT realcalc_sqrt
REAL_ABS_LEMMA real_abs_lemma
REAL_ABS_LEMMA1 real_abs_lemma1
REAL_ABS_TRIANGLE_LEMMA real_abs_triangle_lemma
REAL_EXP_13 real_exp_13
REAL_EXP_15 real_exp_15
REAL_LE_SUC_POW2 real_le_suc_pow2
REAL_MONO_POW2 real_mono_pow2
REAL_MUL_RSUM0 real_mul_rsum0
REAL_NDIV_LEMMA1a real_ndiv_lemma1a
REAL_NDIV_LEMMA1b real_ndiv_lemma1b
REAL_NDIV_LEMMA2 real_ndiv_lemma2
REAL_NDIV_LEMMA3 real_ndiv_lemma3
REAL_OPPSIGN real_oppsign
REAL_OPPSIGN_LEMMA real_oppsign_lemma
REAL_SUB_SUM0 real_sub_sum0
STEPS_EXP steps_exp
STEPS_EXP_0 steps_exp_0
STEPS_EXP_1 steps_exp_1
STEPS_EXP_2 steps_exp_2
STEPS_EXP_3 steps_exp_3
STEPS_EXP_4 steps_exp_4
STEPS_EXP_LEMMA steps_exp_lemma
STEPS_LN steps_ln
STEP_COS step_cos
STEP_EXP step_exp
STEP_EXP_0 step_exp_0
STEP_EXP_1 step_exp_1
STEP_EXP_2 step_exp_2
STEP_EXP_3 step_exp_3
STEP_EXP_4 step_exp_4
STEP_EXP_4_PLUS step_exp_4_plus
STEP_EXP_5 step_exp_5
STEP_EXP_RULE step_exp_rule
STEP_EXP_THM step_exp_thm
STEP_LEMMA1 step_lemma1
STEP_LEMMA2 step_lemma2
STEP_LN step_ln
STEP_SIN step_sin
TAYLOR_EXP taylor_exp
TAYLOR_EXP_WEAK taylor_exp_weak
TAYLOR_LN taylor_ln
log2 log2
raw_eval raw_eval
realcalc_cache realcalc_cache
realcalc_rel_conv realcalc_rel_conv
thm_eval thm_eval
thm_wrap thm_wrap
