# Generated by tools/translator: qualified upstream name -> MoonBit name.
MEASURE measure
MEASURE_LE measure_le
MINIMAL_BAD_SEQUENCE minimal_bad_sequence
WF wf
WF_ANTISYM wf_antisym
WF_DCHAIN wf_dchain
WF_DHAIN_TRANSITIVE wf_dhain_transitive
WF_EQ wf_eq
WF_EREC wf_erec
WF_FALSE wf_false
WF_IND wf_ind
WF_INDUCT_TAC wf_induct_tac
WF_LEX wf_lex
WF_LEX_DEPENDENT wf_lex_dependent
WF_MEASURE wf_measure
WF_MEASURE_GEN wf_measure_gen
WF_POINTWISE wf_pointwise
WF_REC wf_rec
WF_REC_EXISTS wf_rec_exists
WF_REC_INVARIANT wf_rec_invariant
WF_REC_TAIL wf_rec_tail
WF_REC_TAIL_GENERAL wf_rec_tail_general
WF_REC_WF wf_rec_wf
WF_REC_num wf_rec_num
WF_REFL wf_refl
WF_RESTRICT wf_restrict
WF_SUBSET wf_subset
WF_UREC wf_urec
WF_UREC_WF wf_urec_wf
WF_num wf_num
