Lines Matching defs:cmp
307 SORT_UPDATES_CONV ord cmp cnv
312 using the compset "cmp" and conversion "cnv" is used to test equality.
329 fun SORT_UPDATES_CONV ord cmp cnv =
336 sortingTheory.QSORT_DEF] cmp
337 val SORT_CONV = computeLib.CBV_CONV cmp
441 val cmp = reduceLib.num_compset()
444 numLib.SUC_RULE numeral_bitTheory.MOD_2EXP_MAX] cmp
449 SORT_UPDATES_MAPTO_CONV f wordsSyntax.word_lo_tm cmp wordsLib.word_EQ_CONV
476 val cmp = reduceLib.num_compset()
477 val () = computeLib.add_thms [GSYM ty2num_11, ty2num_thm] cmp
478 val cnv = computeLib.CBV_CONV cmp
482 cmp cnv