Searched refs:f3 (Results 1 - 25 of 94) sorted by relevance

1234

/seL4-l4v-10.1.1/HOL4/src/boss/theory_tests/
H A Dtheory1Script.sml36 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 Dgithub112Script.sml7 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 Dstruct8.c13 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 Dmany.c14 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 Dmany2_win32.c14 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 Dmany_win32.c14 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 DACFScript.sml19 `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 DcpsSyntax.sml29 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 DcpsScript.sml23 `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 Dheap_wrap.c36 void f3(struct thing *t) { function
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/decompiler/
H A Dmips_decomp_demoScript.sml25 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 DcpsSyntax.sml29 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 DcpsScript.sml23 `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 DcpsSyntax.sml29 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 DcpsScript.sml23 `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 DILTheory.sig203 |- (!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 Dselftest.sml56 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 Dpattern_matchingScript.sml25 val _ = def "f3"
26 `(f3 (CONS h t) = (h:'a))`;
/seL4-l4v-10.1.1/HOL4/examples/category/
H A DYonedaScript.sml383 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 DFunctionalRecordUpdate.sml8 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 DcompileScript.sml101 (* 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 Dfc_examples.sml18 val def3 = Define `f3 x = x + f2 x`;
/seL4-l4v-10.1.1/HOL4/src/tfl/src/
H A Dselftest.sml35 (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 Dm1_factorialScript.sml54 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 Dlinux64.S119 lfd %f3, -32-(19*8)(%r28)
178 stfd %f3, 16(%r30)
189 stfs %f3, 8(%r30)

Completed in 107 milliseconds

1234