Searched refs:index (Results 1 - 25 of 407) sorted by relevance

1234567891011>>

/seL4-l4v-master/isabelle/src/Pure/
H A Dthm_name.scala19 case 0 => thm_name1.index compare thm_name2.index
30 case Thm_Name_Regex(name, Value.Nat(index)) => Thm_Name(name, index)
35 sealed case class Thm_Name(name: String, index: Int)
38 if (name == "" || index == 0) name
39 else name + "(" + index + ")"
42 if (name == "" || index == 0) name
43 else name + "_" + index
/seL4-l4v-master/l4v/isabelle/src/Pure/
H A Dthm_name.scala19 case 0 => thm_name1.index compare thm_name2.index
30 case Thm_Name_Regex(name, Value.Nat(index)) => Thm_Name(name, index)
35 sealed case class Thm_Name(name: String, index: Int)
38 if (name == "" || index == 0) name
39 else name + "(" + index + ")"
42 if (name == "" || index == 0) name
43 else name + "_" + index
/seL4-l4v-master/seL4/src/arch/arm/machine/
H A Dcache.c18 word_t index; local
20 for (index = LINE_INDEX(start); index < LINE_INDEX(end) + 1; index++) {
21 line = index << L1_CACHE_LINE_SIZE_BITS;
29 word_t index; local
47 for (index = LINE_INDEX(start); index < LINE_INDEX(end) + 1; index++) {
48 line = index << L1_CACHE_LINE_SIZE_BIT
80 word_t index; local
96 word_t index; local
138 word_t index; local
149 word_t index; local
[all...]
/seL4-l4v-master/seL4/include/arch/x86/arch/64/mode/model/
H A Dsmp.h27 cpu_id_t index; member in struct:nodeInfo
48 cpu_id_t index; local
50 : [result] "=r"(index)
51 : [offset] "i"(OFFSETOF(nodeInfo_t, index)));
52 return index;
/seL4-l4v-master/l4v/misc/filemerge/faster/
H A Dtranslate.cpp50 unsigned int index = 0; local
55 buffer[index++] = c;
57 if ((index == 1 && buffer[0] != '\\') ||
58 (index == 2 && buffer[1] != '<') ||
59 (index == 3 && buffer[2] == '^')) {
61 buffer[index] = '\0';
63 index = 0;
64 } else if (buffer[index - 1] == '>') {
65 buffer[index] = '\0';
68 die("unrecognised ASCII sequence \"%.*ls\"", (int)index,
114 int index = 0; local
[all...]
/seL4-l4v-master/seL4/src/plat/imx31/machine/
H A Dhardware.c92 word_t index; local
94 for (index = L2_LINE_INDEX(start);
95 index < L2_LINE_INDEX(end) + 1;
96 index++) {
97 line = index << L2_LINE_SIZE_BITS;
106 word_t index; local
108 for (index = L2_LINE_INDEX(start);
109 index < L2_LINE_INDEX(end) + 1;
110 index++) {
111 line = index << L2_LINE_SIZE_BIT
121 word_t index; local
[all...]
/seL4-l4v-master/HOL4/examples/zipper/
H A DzipperScript.sml16 val index_def = Define`index (Z p a s) = LENGTH p`
21 ``index z < size z``,
51 ``index (moveLeft z) = if 0 < index z then index z - 1 else 0``,
57 ``0 < index z ��� index (moveLeft z) = index z - 1``,
62 ``0 < index z ==> moveLeft z <> z``,
68 ``index
[all...]
/seL4-l4v-master/HOL4/src/unwind/Manual/
H A DMakefile30 entries.tex index.tex \
34 @echo "\begin{theindex}" > index.tex
35 @echo "\mbox{}" >> index.tex
36 @echo "\end{theindex}" >> index.tex
44 index:
45 ${MAKEINDEX} unwind.idx index.tex
57 make clean; make tex; make unwind; make index; make unwind ps pdf
/seL4-l4v-master/seL4/include/arch/arm/arch/model/
H A Dsmp.h14 static inline cpu_id_t cpuIndexToID(word_t index) argument
16 return BIT(index);
/seL4-l4v-master/seL4/libsel4/include/sel4/
H A Dmacros.h50 #define SEL4_SIZE_SANITY(index, entry, size) SEL4_COMPILE_ASSERT(index##entry##size, index + entry == size)
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/
H A Dappendix0.tex11 \texttt{[|}\index{$Isabrl@\ttlbr|bold} &
14 \texttt{|]}\index{$Isabrr@\ttrbr|bold} &
19 \isasymAnd\index{$IsaAnd@\isasymAnd|bold}&
20 \texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
44 \texttt{|}\index{$HOL0or@\ttor|bold} &
50 \verb$~$\index{$HOL0not@\verb$~$|bold} &
53 \verb$~=$\index{$HOL0noteq@\verb$~=$|bold} &
56 \ttindexbold{ALL}, \texttt{!}\index{$HOL0All@\ttall|bold} &
59 \ttindexbold{EX}, \texttt{?}\index{$HOL0Ex@\texttt{?}|bold} &
61 \isasymuniqex\index{
[all...]
H A Droot.tex15 \index{conditional expressions|see{\isa{if} expressions}}
16 \index{primitive recursion|see{recursion, primitive}}
17 \index{product type|see{pairs and tuples}}
18 \index{structural induction|see{induction, structural}}
19 \index{termination|see{functions, total}}
20 \index{tuples|see{pairs and tuples}}
21 \index{*<*lex*>|see{lexicographic product}}
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/
H A Dappendix0.tex11 \texttt{[|}\index{$Isabrl@\ttlbr|bold} &
14 \texttt{|]}\index{$Isabrr@\ttrbr|bold} &
19 \isasymAnd\index{$IsaAnd@\isasymAnd|bold}&
20 \texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
44 \texttt{|}\index{$HOL0or@\ttor|bold} &
50 \verb$~$\index{$HOL0not@\verb$~$|bold} &
53 \verb$~=$\index{$HOL0noteq@\verb$~=$|bold} &
56 \ttindexbold{ALL}, \texttt{!}\index{$HOL0All@\ttall|bold} &
59 \ttindexbold{EX}, \texttt{?}\index{$HOL0Ex@\texttt{?}|bold} &
61 \isasymuniqex\index{
[all...]
H A Droot.tex15 \index{conditional expressions|see{\isa{if} expressions}}
16 \index{primitive recursion|see{recursion, primitive}}
17 \index{product type|see{pairs and tuples}}
18 \index{structural induction|see{induction, structural}}
19 \index{termination|see{functions, total}}
20 \index{tuples|see{pairs and tuples}}
21 \index{*<*lex*>|see{lexicographic product}}
/seL4-l4v-master/isabelle/src/Doc/How_to_Prove_it/document/
H A Dprelude.tex1 \usepackage{makeidx} % allows index generation
4 \usepackage{multicol} % used for the two-column index
34 {\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}}
55 %index
57 \newcommand{\concept}[1]{\conceptnoidx{#1}\index{#1}}
58 \newcommand{\conceptidx}[2]{\conceptnoidx{#1}\index{#2}}
59 \newcommand{\indexed}[2]{#1\index{#2@\protect#1}}
/seL4-l4v-master/l4v/isabelle/src/Doc/How_to_Prove_it/document/
H A Dprelude.tex1 \usepackage{makeidx} % allows index generation
4 \usepackage{multicol} % used for the two-column index
34 {\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}}
55 %index
57 \newcommand{\concept}[1]{\conceptnoidx{#1}\index{#1}}
58 \newcommand{\conceptidx}[2]{\conceptnoidx{#1}\index{#2}}
59 \newcommand{\indexed}[2]{#1\index{#2@\protect#1}}
/seL4-l4v-master/l4v/tools/c-parser/testfiles/
H A Dextern_dups.c25 int index(int i) function
/seL4-l4v-master/seL4/src/plat/pc99/machine/
H A Dioapic.c89 int index = ioapic * IOAPIC_IRQ_LINES + pin; local
95 ioredtbl_state[index] |= IOREDTBL_LOW_INTERRUPT_MASK;
97 ioredtbl_state[index] &= ~IOREDTBL_LOW_INTERRUPT_MASK;
100 assert((ioredtbl_state[index] & 0xff) != 0);
103 ioapic_write(ioapic, IOAPIC_WINDOW, ioredtbl_state[index]);
150 uint32_t index = 0; local
152 index = ioapic * IOAPIC_IRQ_LINES + pin;
159 ioredtbl_state[index] = IOREDTBL_LOW_INTERRUPT_MASK |
166 ioredtbl_state[index] |= ioapic_read(ioapic, IOAPIC_WINDOW) & ~MASK(16);
167 ioapic_write(ioapic, IOAPIC_WINDOW, ioredtbl_state[index]);
[all...]
/seL4-l4v-master/HOL4/src/num/arith/Manual/
H A Ddescription.tex6 arithmetic\index{linear arithmetic}. There are also some associated functions,
11 Presburger natural arithmetic\index{Presburger arithmetic}. Presburger natural
17 Products\index{products}\index{multiplication} of two expressions which both
23 been put in prenex normal form\index{prenex normal form} it must contain only
25 universal\index{quantifiers!universal} (`forall') or all
26 existential\index{quantifiers!existential}. Variables may appear
27 free\index{free variables} (unquantified) provided any quantifiers that do
32 \index{normalisation}
33 The function makes use of a number of preprocessors\index{preprocessor
[all...]
H A DMakefile36 index:
49 make clean; make tex; make arith; make index; make arith ps pdf
/seL4-l4v-master/HOL4/examples/dev/sw/
H A DSymbol.sml6 val index : symbol -> int value
35 fun mkSymbol name index =
36 (name,index) : symbol
39 fun index(s,n) = n function
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DSymbol.sml6 val index : symbol -> int value
35 fun mkSymbol name index =
36 (name,index) : symbol
39 fun index(s,n) = n function
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/
H A DSymbol.sml6 val index : symbol -> int value
35 fun mkSymbol name index =
36 (name,index) : symbol
39 fun index(s,n) = n function
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/
H A DSymbol.sml6 val index : symbol -> int value
35 fun mkSymbol name index =
36 (name,index) : symbol
39 fun index(s,n) = n function
/seL4-l4v-master/HOL4/src/num/reduce/Manual/
H A DMakefile13 all:; make clean; make ids; make reduce; make index; make reduce ps pdf
23 index:

Completed in 275 milliseconds

1234567891011>>