/seL4-l4v-10.1.1/HOL4/src/boss/theory_tests/ |
H A D | theory1Script.sml | 36 val f3_def = Define`f3 n = n + 1`; 37 val f3_def = Define`f3 n = n + 2`; 38 val f3_def = Define`f3 n = n + 3`; 39 val f3_def = Define`f3 n = n + 4`; 41 val g3_def = Define`g3 n = f3 (n + 1)` 42 val f3_def = Define`f3 n = n + 5`;
|
H A D | github112Script.sml | 7 val f3_def = Define `f3 x = (case [] of _ => 1) + (case 2 of _ => 2)`
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.call/ |
H A D | struct8.c | 13 float f3; member in struct:__anon64 21 ts.f3 += 1; 59 ts8_arg.f3 = -5.55f; 64 printf ("%g\n", ts8_arg.f3); 71 printf ("%g\n", ts8_result->f3); 76 CHECK(ts8_result->f3 == -5.55f + 1);
|
H A D | many.c | 14 static float ABI_ATTR many(float f1, float f2, float f3, float f4, float f5, float f6, float f7, float f8, float f9, float f10, float f11, float f12, float f13) argument 18 (double) f1, (double) f2, (double) f3, (double) f4, (double) f5, 23 return f1+f2+f3+f4+f5+f6+f7+f8+f9+f10+f11+f12+f13;
|
H A D | many2_win32.c | 14 float f3, 26 return ((f1/f2+f3/f4+f5/f6+f7/f8+f9/f10+f11/f12) * f13); 12 fastcall_many(float f1, float f2, float f3, float f4, float f5, float f6, float f7, float f8, float f9, float f10, float f11, float f12, float f13) argument
|
H A D | many_win32.c | 14 float f3, 26 return ((f1/f2+f3/f4+f5/f6+f7/f8+f9/f10+f11/f12) * f13); 12 stdcall_many(float f1, float f2, float f3, float f4, float f5, float f6, float f7, float f8, float f9, float f10, float f11, float f12, float f13) argument
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | ACFScript.sml | 19 `cj f1 f2 f3 = \x. if f1 x then f2 x else f3 x`; 49 ``!f f1 f2 f3. 50 (!x:'a. f x = if f1(x) then f2(x) else f(f3 x)) 51 ==> (?R. WF R /\ (!x. ~f1 x ==> R (f3 x) x)) 52 ==> (f:'a->'b = sc (tr f1 f3) f2)``, 59 Q.SPEC `\x. f x = sc (tr f1 f3) f2 x`) THEN
|
H A D | cpsSyntax.sml | 29 fun mk_ite(f1,f2,f3) = 33 list_mk_comb(inst[alpha|->d1,beta|->r2]ite_tm,[f1,f2,f3]) 37 fun mk_rec(f1,f2,f3) = 41 list_mk_comb(inst[alpha|->d1,beta|->r2]rec_tm,[f1,f2,f3])
|
H A D | cpsScript.sml | 23 `Ite f1 f2 f3 = \x. if f1 x then f2 x else f3 x`; 27 `Rec (x:'a) = if f1 x then f2 x else Rec (f3 x)`; 304 ``!f f1 f2 f3. 305 (!x:'a. f x = if f1(x) then f2(x) else f(f3 x)) 306 ==> (?R. WF R /\ (!x. ~f1 x ==> R (f3 x) x)) 307 ==> (f:'a->'b = Rec f1 f2 f3)``,
|
/seL4-l4v-10.1.1/l4v/tools/autocorres/tests/examples/ |
H A D | heap_wrap.c | 36 void f3(struct thing *t) { function
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/decompiler/ |
H A D | mips_decomp_demoScript.sml | 25 add.d $f3, $f1, $f2 26 sub.d $f1, $f2, $f3 29 madd.d $f2, $f1, $f2, $f3
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | cpsSyntax.sml | 29 fun mk_ite(f1,f2,f3) = 33 list_mk_comb(inst[alpha|->d1,beta|->r2]ite_tm,[f1,f2,f3]) 37 fun mk_rec(f1,f2,f3) = 41 list_mk_comb(inst[alpha|->d1,beta|->r2]rec_tm,[f1,f2,f3])
|
H A D | cpsScript.sml | 23 `Ite f1 f2 f3 = \x. if f1 x then f2 x else f3 x`; 27 `Rec (x:'a) = if f1 x then f2 x else Rec (f3 x)`; 304 ``!f f1 f2 f3. 305 (!x:'a. f x = if f1(x) then f2(x) else f(f3 x)) 306 ==> (?R. WF R /\ (!x. ~f1 x ==> R (f3 x) x)) 307 ==> (f:'a->'b = Rec f1 f2 f3)``,
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | cpsSyntax.sml | 29 fun mk_ite(f1,f2,f3) = 33 list_mk_comb(inst[alpha|->d1,beta|->r2]ite_tm,[f1,f2,f3]) 37 fun mk_rec(f1,f2,f3) = 41 list_mk_comb(inst[alpha|->d1,beta|->r2]rec_tm,[f1,f2,f3])
|
H A D | cpsScript.sml | 23 `Ite f1 f2 f3 = \x. if f1 x then f2 x else f3 x`; 27 `Rec (x:'a) = if f1 x then f2 x else Rec (f3 x)`; 304 ``!f f1 f2 f3. 305 (!x:'a. f x = if f1(x) then f2(x) else f(f3 x)) 306 ==> (?R. WF R /\ (!x. ~f1 x ==> R (f3 x) x)) 307 ==> (f:'a->'b = Rec f1 f2 f3)``,
|
H A D | ILTheory.sig | 203 |- (!f f1 f2 f3 a. CTL_STRUCTURE_case f f1 f2 f3 (BLK a) = f a) /\ 204 (!f f1 f2 f3 a0 a1. CTL_STRUCTURE_case f f1 f2 f3 (SC a0 a1) = f1 a0 a1) /\ 205 (!f f1 f2 f3 a0 a1 a2. 206 CTL_STRUCTURE_case f f1 f2 f3 (CJ a0 a1 a2) = f2 a0 a1 a2) /\ 207 !f f1 f2 f3 a0 a1. CTL_STRUCTURE_case f f1 f2 f3 (TR a0 a1) = f3 a0 a1 430 |- (!f f1 f2 f3 f [all...] |
/seL4-l4v-10.1.1/HOL4/src/num/termination/ |
H A D | selftest.sml | 56 f3 (y : 'a) (z : 'a) = \x. case x of 0 => 0n | SUC n => f3 y z n
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/test/ |
H A D | pattern_matchingScript.sml | 25 val _ = def "f3" 26 `(f3 (CONS h t) = (h:'a))`;
|
/seL4-l4v-10.1.1/HOL4/examples/category/ |
H A D | YonedaScript.sml | 383 qmatch_abbrev_tac `(f1 o f2 -:ens_cat (homs c) = f3 o f4 -:ens_cat (homs c)) ��� X` >> 404 `f3 :- f3.dom ��� f3.cod -:ens_cat (homs c)` by ( 405 qunabbrev_tac `f3` >> 417 `f4 ���> f3 -:ens_cat (homs c)` by ( 418 fsrw_tac [][Abbr`f3`] ) >> 419 `n.cod@@z = f3.cod` by ( 420 fsrw_tac [][maps_to_in_def,Abbr`f3`] ) >>
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | FunctionalRecordUpdate.sml | 8 fun f3 z = next f2 z function 9 fun f4 z = next f3 z 34 fun c3 from = c2 (from f3)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/ |
H A D | compileScript.sml | 101 (* Ite f1 f2 f3 if f1 then f2 else f3 *) 102 (* Rec f1 f2 f3 tail recursion with test f1, base f2 and step f3 *) 112 Define `Ite f1 f2 f3 = \x. if f1 x then f2 x else f3 x`; 260 ``!P1 P2 P3 f1 f2 f3. 261 (P1 ===> DEV f1) /\ (P2 ===> DEV f2) /\ (P3 ===> DEV f3) 263 ITE P1 P2 P3 ===> DEV (Ite f1 f2 f3)``, 267 THEN `DEV f3 (start_ [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/examples/ |
H A D | fc_examples.sml | 18 val def3 = Define `f3 x = x + f2 x`;
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | selftest.sml | 35 (Hol_defn "f3") 36 `f3 x = case x of (f,T,_) => ~f | (_,F,f) => f F`;
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/acl2/ |
H A D | m1_factorialScript.sml | 54 val f3 = el 1 (CONJUNCTS defs2); value 64 val _ = sexp.print_acl2def out (sexp.defun (concl f3));
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/powerpc/ |
H A D | linux64.S | 119 lfd %f3, -32-(19*8)(%r28) 178 stfd %f3, 16(%r30) 189 stfs %f3, 8(%r30)
|