Searched refs:out (Results 1 - 25 of 544) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/examples/hardware/hol88/
H A DPARITY.ml19 "!in out.
20 (out 0 = T) /\ (!t. out(SUC t) = (in(SUC t) => ~(out t) | out t))
22 (!t. out t = PARITY t in)",
30 (`ONE_DEF`, "ONE(out:num->bool) = !t. out t = T");;
34 (`NOT_DEF`, "NOT(in,out:num->bool) = !t. out
[all...]
H A DStokes.ml12 "(COUNTER 0 reset out = T) /\
13 (COUNTER (SUC m) reset out =
15 ((out(SUC m) = ((reset m=0) => 0 | (out m)+1)) /\
16 COUNTER m reset out)))");;
27 "(INC 0 out p1 = T) /\
28 (INC (SUC m) out p1 =
29 (p1(SUC m) = out(SUC m)+1) /\
30 INC m out p1)");;
34 "(DEL 0 p2 (out
[all...]
/seL4-l4v-master/HOL4/examples/parity/
H A DPARITYScript.sml23 ``!inp out.
24 (out 0 = T) /\
25 (!t. out (SUC t) = if inp (SUC t) then ~out t else out t)
27 !t. out t = PARITY t inp``,
34 val ONE_def = Define `ONE(out:num->bool) = !t. out t = T`;
36 val NOT_def = Define `NOT(inp, out:num->bool) = !t. out
[all...]
H A DPARITY_exercisesScript.sml10 RESET_REG(reset,inp,out) =
11 (!t. reset t ==> (out t = T)) /\
12 (!t. out (t + 1) = if reset t \/ reset (t + 1) then T else inp t)
16 RESET_REG_IMP (reset,inp,out) =
21 MUX(mo,mo,ro2,out)
30 ``RESET_REG_IMP(reset,inp,out) ==>
31 RESET_REG(reset,inp,out)``,
39 The value at out is T if and only if there have been an even
44 RESET_PARITY (reset,inp,out) <=>
45 (out
[all...]
/seL4-l4v-master/HOL4/examples/dev/Fact32/
H A DNOT32.ml4 `NOT32(inp,out) = !t. out t = ~(inp t : word32)`;
9 ``COMB ($~:word32->word32) (inp, out) = NOT32(inp,out)``,
17 ``NOT32(inp,out)
19 NOT32(inp at clk,out at clk)``,
26 \module NOT32 (inp,out);\n\
29 \ output [size:0] out;\n\
31 \ assign out = ~inp;\n\
37 fun NOT32vInst (out
[all...]
H A Dexor32.ml21 `XOR32(in1:num->word32,in2,out) = !t. out t = (in1 t) ?? (in2 t)`;
31 ``COMB (UNCURRY $??) (in1 <> in2, out) = XOR32(in1,in2,out)``,
39 ``XOR32(in1,in2,out)
41 XOR32(in1 at clk,in2 at clk,out at clk)``,
52 (* instances) and a function to print a HOL term ``XOR32(in1,in2,out)`` as *)
53 (* an instance, using the type of ``out`` to compute the word width *)
59 \module XOR32 (in1,in2,out);\n\
62 \ output [size:0] out;\
[all...]
/seL4-l4v-master/HOL4/examples/Hoare-for-divergence/
H A Dwhile_langScript.sml30 output_of ((s,out):state) = out
34 subst n e (s,out) = ((n =+ e s) s,out:value list)
38 print e ((s,out):state) = (s,out ++ [e s])
42 guard x ((s,out):state) = (x s ��� 0)
76 output = LUB { fromList out | ���q t. RTC step (p,s) (q,t,out) }
/seL4-l4v-master/HOL4/help/src-sml/
H A DHOLPage.sml51 fun out s = TextIO.output(os, s) function
53 app out ["<A HREF=\"file://", target, "\">", anchor, "</A>"]
85 ; out "&nbsp;&nbsp;&nbsp;&nbsp;\n"
94 out "<HTML>\
96 out "<BODY BGCOLOR=\""; out bgcolor; out "\">\n";
97 out "<H1>HOL Reference Page</H1>\n";
99 out "<DL>";
101 out"<D
[all...]
H A DDoc2Html.sml87 fun out s = TextIO.output(ostrm,s) function
89 fun markout PARA = out "\n<P>\n"
91 (out "<SPAN class = \"TEXT\">";
92 out (text_encode ss);
93 out "</SPAN>")
95 out ("<em>" ^ text_encode ss ^ "</em>")
97 (out "<SPAN class = \"BRKT\">";
98 out (bracket_trans ss);
99 out "</SPAN>")
101 (out "<DI
[all...]
H A DHtmlsigs.sml5 fun indexbar out srcpath = out (String.concat
153 fun out s = TextIO.output(os, s) function
165 (out "<a name=\""; out target; out "\">"; out anchor; out "</a>")
168 (out "<a href=\"#"; out lin
353 fun out s = TextIO.output(os, s) function
[all...]
H A DPrintbase.sml12 fun out s = TextIO.output(os, s) function
31 out (prtseq (prentry, ", ") entries);
32 out "\n";
40 fun out s = TextIO.output(os, s) function
50 out "\\\\[2ex]\n\n")
53 fun nextstr last [] = out ")\n"
56 (out ", "; out (tt file); nextstr last erest)
58 (out ")\n"; newitem e1 erest)
63 out "\\ite
[all...]
/seL4-l4v-master/HOL4/examples/dev/
H A Dvsynth.sml247 fun out s = TextIO.output(outstr,s) function
249 (printer out;
265 (* ``DTYPE c (clk,inp,out)`` --> ``DTYPE c (clk,inp,out)`` *)
266 (* ``?v. DTYPE v (clk,inp,out)`` --> ``DTYPE c (clk,inp,out)`` *)
284 (* Test a term has the form ``CONSTANT c out``, *)
302 (* ``CONSTANT c out`` --> ("c", ``out``) where c is Verilog form of c *)
428 fun DTYPEvInst tm (out
[all...]
/seL4-l4v-master/HOL4/src/ring/src/
H A Dselftest.sml5 fun ntest (i,out) =
6 convtest ("NUM_NORM_CONV " ^ Parse.term_to_string i, NUM_NORM_CONV, i, out)
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/
H A Dbuild13 [ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
/seL4-l4v-master/isabelle/src/Doc/
H A Dprepare_document14 [ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
/seL4-l4v-master/HOL4/examples/machine-code/acl2/
H A DMakefile7 cat fact-out.lisp
10 /bin/rm fact.lisp fact-out.* untranslate-file.*
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/
H A Dbuild13 [ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
/seL4-l4v-master/l4v/isabelle/src/Doc/
H A Dprepare_document14 [ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
/seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/
H A Dparity.tex33 con un input {\small\verb|in|}, un output {\small\verb|out|} e la
34 specifica che l'$n$-esimo output su {\small\verb|out|} �
96 !t. out t = PARITY t inp
104 {\small\verb|inp|} e {\small\verb|out|} soddisfano\footnote{Preferiremmo
110 out(0) = T
118 !t. out(t+1) = (if inp(t+1) then ~(out t) else out t)
127 !inp out.
128 (out
[all...]
/seL4-l4v-master/l4v/misc/filemerge/faster/
H A Dtranslate.cpp27 static int to_ascii(wifstream &in, wofstream &out) { argument
29 assert(out.is_open());
36 out << c;
38 out << t->second;
45 static int to_unicode(wifstream &in, wofstream &out) { argument
47 assert(out.is_open());
62 out << buffer;
71 out << t->second;
82 out << buffer;
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/
H A DFile.C88 void putUInt(File& out, uint64 val) argument
93 out.putChar(v);
96 out.putChar(0x80 | (v >> 8)),
97 out.putChar((uchar)v);
99 out.putChar(0xA0 | (v >> 16)),
100 out.putChar((uchar)(v >> 8)),
101 out.putChar((uchar)v);
103 out.putChar((v >> 24) | 0xC0),
104 out.putChar((uchar)(v >> 16)),
105 out
[all...]
/seL4-l4v-master/isabelle/Admin/cronjob/
H A Dself_update17 } > run/self_update.out
/seL4-l4v-master/l4v/isabelle/Admin/cronjob/
H A Dself_update17 } > run/self_update.out
/seL4-l4v-master/isabelle/src/Doc/Intro/document/
H A Dgetting.tex246 {\out [| ?P --> ?Q; ?P |] ==> ?Q}
247 {\out val it = "[| ?P --> ?Q; ?P |] ==> ?Q" : thm}
249 {\out [| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q}
250 {\out val it = "[| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q" : thm}
253 appears in{\out slanted typewriter characters}. \ML's response {\out val
265 {\out val it = "[| (?P --> ?Q) & ?Q1; ?P |] ==> ?Q" : thm}
267 {\out val it = "[| ?P --> ?Q; ?P & ?Q1 |] ==> ?Q" : thm}
281 {\out val it = "ALL x. ?P(x) ==> ?P(?x)" : thm}
283 {\out va
[all...]
/seL4-l4v-master/l4v/isabelle/src/Doc/Intro/document/
H A Dgetting.tex246 {\out [| ?P --> ?Q; ?P |] ==> ?Q}
247 {\out val it = "[| ?P --> ?Q; ?P |] ==> ?Q" : thm}
249 {\out [| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q}
250 {\out val it = "[| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q" : thm}
253 appears in{\out slanted typewriter characters}. \ML's response {\out val
265 {\out val it = "[| (?P --> ?Q) & ?Q1; ?P |] ==> ?Q" : thm}
267 {\out val it = "[| ?P --> ?Q; ?P & ?Q1 |] ==> ?Q" : thm}
281 {\out val it = "ALL x. ?P(x) ==> ?P(?x)" : thm}
283 {\out va
[all...]

Completed in 94 milliseconds

1234567891011>>