Searched refs:mk_num (Results 1 - 6 of 6) sorted by path

/seL4-l4v-master/HOL4/examples/machine-code/decompiler/
H A DdecompilerLib.sml643 val mk_num = numSyntax.mk_numeral o Arbnum.fromInt value
645 subst [mk_var("n",``:num``) |-> mk_num i] ``p + (n2w n):word32``
647 val xs = zip (map mk_num (foo entry 0)) (map mk_pos entry)
1813 val mk_num = numSyntax.mk_numeral o Arbnum.fromInt value
1814 val th = SIMP_RULE std_ss [] (INST [mk_var("pos",``:num``) |-> mk_num k] th)
/seL4-l4v-master/HOL4/src/1/
H A DPrim_rec.sml1648 mk_num generates the function corresponding to number n. The abstraction
1651 fun mk_num numbits n = let function
1737 (mk_comb(f, x) == mk_num nb n):: recurse (n + 1) xs
/seL4-l4v-master/graph-refine/
H A Dlogic.py9 from syntax import true_term, false_term, mk_num namespace
126 return mk_eq (mk_bwand (w, mask), mk_num (0, w.typ))
436 return mk_bwand (expr, mk_num (((1 << n) - 1), expr.typ))
1113 arg_offs.append (syntax.mk_num (0, expr2.typ))
1202 return mk_num (0, expr.typ)
H A Dsearch.py17 mk_num, mk_minus, mk_plus, mk_less)
496 result = mk_num (val, x.typ.num + n_extend)
504 result = mk_num ((x.val >> n_bot) & ((1 << length) - 1), length)
896 eq = mk_eq (mk_times (offs_smt, mk_num (4, offs_smt.typ)),
897 mk_num (0, offs_smt.typ))
1470 zero = mk_num (0, lhs.typ)
1582 const_less = lambda n: mk_less (const, mk_num (n, const.typ))
1585 const_ge = lambda n: mk_less (mk_num (n, const.typ), const)
H A Dsolver.py1807 syntax.mk_num (n, token_smt_typ), {})
2003 return syntax.mk_num (n, ln)
2007 return syntax.mk_num (int (s[2:], 2), len (s) - 2)
2009 return syntax.mk_num (int (s[2:], 16), (len (s) - 2) * 4)
H A Dsyntax.py1411 def mk_num (x, typ): function
1420 return mk_num (x, word32T)
1423 return mk_num (x, word8T)

Completed in 103 milliseconds