/seL4-l4v-master/l4v/tools/c-parser/testfiles/ |
H A D | locvarfncall.c | 9 int mult(int x, int y) function 20 r = mult(f(7), g(7)); 26 return mult(f(i),g(i+1)); 31 int x = mult(f(i), g(i+1));
|
H A D | fncall.c | 9 int mult(int x, int y) function 24 total = mult(factor, total);
|
/seL4-l4v-master/HOL4/examples/elliptic/ |
H A D | groupScript.sml | 471 mult : 'a -> 'a -> 'a |>`; 477 (!x y :: (g.carrier). g.mult x y IN g.carrier) /\ 479 (!x :: (g.carrier). g.mult g.id x = x) /\ 480 (!x :: (g.carrier). g.mult (g.inv x) x = g.id) /\ 481 (!x y z :: (g.carrier). g.mult (g.mult x y) z = g.mult x (g.mult y z)) }`; 485 (group_exp G g (SUC n) = G.mult g (group_exp G g n))`; 490 g IN Group /\ !x y :: (g.carrier). g.mult [all...] |
H A D | groupTools.sml | 61 key = ``g.mult x y``,
|
H A D | fieldScript.sml | 167 val field_add_def = Define `field_add (f : 'a field) = f.sum.mult`; 172 val field_mult_def = Define `field_mult (f : 'a field) = f.prod.mult`; 769 >> (Suff `f.prod.mult x f.prod.id IN f.prod.carrier` 773 ++ Suff `f.prod.mult x (f.sum.inv f.prod.id) IN f.prod.carrier` 833 ++ Suff `f.prod.mult x y IN f.prod.carrier` 916 ++ Suff `f.prod.mult x y IN f.prod.carrier` 2456 mult := (\x y. if x = zero_elt then y 2462 mult := (\x y. if x = zero_elt then zero_elt
|
H A D | fieldTools.sml | 736 val _ = not (is_field_mult a) orelse raise Bug "a is a mult" 737 and _ = not (is_field_mult b) orelse raise Bug "b is a mult" 804 NONE => raise Bug "a not a mult" 809 NONE => raise Bug "b not a mult"
|
/seL4-l4v-master/HOL4/src/ring/src/ |
H A D | numRingScript.sml | 36 val _ = temp_overload_on("mult",���$* : num->num->num���);
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | hol_defaxioms_proofsScript.sml | 135 [acl2_numberp (add x y); acl2_numberp (mult x y); 143 [acl2_numberp (add x y); acl2_numberp (mult x y); 232 |- |= equal (mult (mult x y) z) (mult x (mult y z)), 238 ``|= equal (mult (mult x y) z) (mult x (mult [all...] |
H A D | translateScript.sml | 936 val INTEGERP_MULT = store_thm("INTEGERP_MULT",``!a b. (|= integerp a) /\ (|= integerp b) ==> |= integerp (mult a b)``, 962 val INT_MULT = store_thm("INT_MULT",``!a b. int (a * b) = mult (int a) (int b)``, 1025 ``!a b. nat (a * b) = mult (nat a) (nat b)``, 1052 val RATIONALP_MULT = store_thm("RATIONALP_MULT",``!a b. (|= rationalp a) /\ (|= rationalp b) ==> |= rationalp (mult a b)``, 1069 val RAT_MULT = store_thm("RAT_MULT",``!a b. rat (a * b) = mult (rat a) (rat b)``, 1079 ``!a b. ~(b = 0) ==> (rat (a / b) = mult (rat a) (reciprocal (rat b)))``, 1102 val ACL2_NUMBERP_MULT = store_thm("ACL2_NUMBERP_MULT",``!a b. |= acl2_numberp (mult a b)``, 1113 val COM_MULT = store_thm("COM_MULT",``!a b. num (a * b) = mult (num a) (num b)``,RW_TAC std_ss [mult_def]); 1122 val COM_DIV = store_thm("COM_DIV",``!a b. ~(b = com_0) ==> (num (a / b) = mult (num a) (reciprocal (num b)))``, 1312 ``!a b. (|= natp a) /\ (|= natp b) ==> |= natp (mult [all...] |
H A D | hol_defaxiomsScript.sml | 2015 (let q = mult i (reciprocal j) in 2030 (let q = mult i (reciprocal j) in 2043 (let q = mult i (reciprocal j) in 2055 (let q = mult i (reciprocal j) in 2064 (integerp (mult fl (reciprocal (nat 2))),fl)] 2071 (integerp (mult cl (reciprocal (nat 2))),cl)] 2077 |- mod x y = add x (unary_minus (mult (floor x y) y)), 2083 `mod x y = add x (unary_minus (mult (floor x y) y))`; 2088 |- x rem y = add x (unary_minus (mult (truncate x y) y)), 2093 |- evenp x = integerp (mult [all...] |
H A D | extendTranslateScript.sml | 70 then (mult (reciprocal r) (acl2_expt r (add i (int 1)))) 71 else (mult r (acl2_expt r (add i (unary_minus (int 1))))))) 171 let q = mult a (reciprocal b) in 183 let q = mult a (reciprocal b) in 400 (numerator (mult (int a) (reciprocal (int b))) = 402 (denominator (mult (int a) (reciprocal (int b))) = 598 `acl2_mod x y = add x (unary_minus (mult (acl2_floor x y) y))`; 601 `acl2_rem x y = add x (unary_minus (mult (acl2_truncate x y) y))`; 838 `acl2_evenp x = integerp (mult x (reciprocal (int 2)))`; 908 `acl2_ash i c = acl2_floor (mult (ifi [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw2/test/ |
H A D | refined_format.sml | 178 mult(x:word32,y) = 188 |- mult (x,y) =
|
/seL4-l4v-master/HOL4/src/num/arith/src/ |
H A D | Solve_ineqs.sml | 157 val mult = lcm (coeff1,coeff2) value 158 val mult1 = mult div coeff1 159 and mult2 = mult div coeff2
|
H A D | Gen_arith.sml | 128 val _ = Int.>(length ms, 1) orelse failwith "not a mult"
|
/seL4-l4v-master/HOL4/examples/dev/AES/tupled/ |
H A D | RoundOpScript.sml | 383 val [mult] = decls "**"; value 418 THEN RESTR_EVAL_TAC [mult,B_HEX,D_HEX,E_HEX,TWO,THREE,NINE]
|
/seL4-l4v-master/HOL4/examples/dev/AES/word8/ |
H A D | RoundOpScript.sml | 379 val mult = Term `Mult$**`; value 409 THEN RESTR_EVAL_TAC [mult,n2w]
|
/seL4-l4v-master/HOL4/examples/Crypto/AES/ |
H A D | RoundOpScript.sml | 376 val mult = Term `Mult$**`; value 406 THEN RESTR_EVAL_TAC [mult,n2w]
|
/seL4-l4v-master/HOL4/examples/acl2/examples/M1/ |
H A D | hol_defaxiomsScript.sml | 2030 (let q = mult i (reciprocal j) in 2045 (let q = mult i (reciprocal j) in 2060 (let q = mult i (reciprocal j) in 2073 (let q = mult i (reciprocal j) in 2085 (let q = mult i (reciprocal j) in 2094 (integerp (mult fl (reciprocal (nat 2))),fl)] 2101 (integerp (mult cl (reciprocal (nat 2))),cl)] 2107 |- mod x y = add x (unary_minus (mult (floor x y) y)), 2113 `mod x y = add x (unary_minus (mult (floor x y) y))`; 2118 `mod x y = add x (unary_minus (mult (floo [all...] |
/seL4-l4v-master/HOL4/examples/dev/AES/curried/ |
H A D | RoundOpScript.sml | 408 val [mult] = decls "**"; value 443 THEN RESTR_EVAL_TAC [mult,B_HEX,D_HEX,E_HEX,TWO,THREE,NINE]
|
/seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | hol_defaxiomsScript.sml | 2019 (let q = mult i (reciprocal j) in 2034 (let q = mult i (reciprocal j) in 2047 (let q = mult i (reciprocal j) in 2059 (let q = mult i (reciprocal j) in 2068 (integerp (mult fl (reciprocal (nat 2))),fl)] 2075 (integerp (mult cl (reciprocal (nat 2))),cl)] 2081 |- mod x y = add x (unary_minus (mult (floor x y) y)), 2087 `mod x y = add x (unary_minus (mult (floor x y) y))`; 2092 |- x rem y = add x (unary_minus (mult (truncate x y) y)), 2097 |- evenp x = integerp (mult [all...] |
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | realconv.cpp | 865 mult 1009 b1 = mult(b, p5); 1019 p51 = p5->next = mult(p5,p5); 1024 p51 = p5->next = mult(p5,p5); 3124 bb1 = mult(bs, bb); 4196 b1 = mult(mhi, b);
|
/seL4-l4v-master/HOL4/src/AI/ |
H A D | aiLib.sml | 625 let val mult = pow 10.0 n in value 626 Real.fromInt (Real.round (r * mult)) / mult
|
/seL4-l4v-master/graph-refine/ |
H A D | stack_logic.py | 125 for (x, mult) in vs: 130 new_vs[v] += var[v] * mult 131 const += c * mult
|
/seL4-l4v-master/HOL4/examples/algebra/finitefield/ |
H A D | ffExtendScript.sml | 517 The GF(2) is simple: add x y = (x + y) MOD 2, mult x y = (x * y) MOD 2, 547 mult x y = if (x == 0) then 0 else if (y == 0) then 0 else 1 + (((x - 1) + (y - 1)) MOD 3) 551 GF(4).mult x y = GF(2).mult x y
|
/seL4-l4v-master/HOL4/examples/AI_tasks/ |
H A D | mleDiophSynt.sml | 57 then raise ERR "apply_move_poly" "mult"
|