Searched refs:mk_less (Results 26 - 37 of 37) sorted by relevance
12
| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | syntax.py | 1356 def mk_less (x, y, signed = False): function
1486 mk_eq, mk_less_eq, mk_less, mk_implies, mk_and, mk_or, mk_not, mk_word32,
|
| H A D | pseudo_compile.py | 17 mk_less_eq, mk_less, mk_implies, mk_and, mk_or, mk_not, mk_word32, mk_word8,
|
| H A D | search.py | 19 mk_num, mk_minus, mk_plus, mk_less)
1584 const_less = lambda n: mk_less (const, mk_num (n, const.typ))
1587 const_ge = lambda n: mk_less (mk_num (n, const.typ), const)
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
| H A D | Import.sml | 1169 SOME numSyntax.mk_less, SOME intSyntax.mk_less)
|
| /seL4-l4v-10.1.1/HOL4/src/integer/ |
| H A D | CooperMath.sml | 317 val g_t_lt0 = EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, g_t)))
918 EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, term_of_int i)))
|
| H A D | IntDP_Munge.sml | 287 val div_nzero = EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, divisor)))
|
| H A D | OmegaSymbolic.sml | 293 EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, f)))
|
| H A D | OmegaMath.sml | 126 val zero_lt_g = EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, g_t)))
|
| /seL4-l4v-10.1.1/HOL4/src/n-bit/ |
| H A D | blastLib.sml | 43 numSyntax.mk_less (i, j)
124 val thm = numSyntax.mk_less (ti, lvs)
|
| /seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
| H A D | numSimps.sml | 560 mDISCH (mk_less(zero_tm, v)) (REWRITE_RULE [base_rewrite] base_thm)
|
| /seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
| H A D | quantHeuristicsScript.sml | 1023 val l = mk_less (pre_n_t, len_t);
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
| H A D | holfootLib.sml | 229 numSyntax.mk_less (ec, numSyntax.mk_plus (ec', nc')))
2228 if i2 then (SOME (mk_disj (numSyntax.mk_less (nc2, ec1), mk_eq (ec2, ec1))),
|
Completed in 212 milliseconds
12