/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/ |
H A D | Clipboard.sml | 274 val (vec, count) = list2Vector cCLIPFORMAT l 275 val res = getPriorityClipboardFormat(vec, count) handle ex => (Memory.free vec; raise ex)
|
H A D | Menu.sml | 535 val count = List.length mlist 560 let val count = List.length mlist value 562 val menu = alloc count (Cstruct [Cshort,Cshort,Cpointer Cchar])
|
/seL4-l4v-master/seL4/src/arch/x86/kernel/ |
H A D | boot.c | 93 init_freemem(mem_p_regs->count, mem_p_regs->list, MAX_RESERVED, reserved, v_reg, extra_bi_size_bits);
|
/seL4-l4v-master/isabelle/src/Pure/Tools/ |
H A D | spell_checker.scala | 201 updates.valuesIterator.count(upd => !upd.permanent)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/ |
H A D | spell_checker.scala | 201 updates.valuesIterator.count(upd => !upd.permanent)
|
/seL4-l4v-master/HOL4/examples/algebra/polynomial/ |
H A D | polyFieldModuloScript.sml | 4843 (PPOW (IMAGE SUC (count n))) (PolyRing r).carrier 4848 (1) s IN POW (IMAGE SUC (count n)) ==> PPROD (IMAGE f s) IN (PolyRing r).carrier 4849 s IN POW (IMAGE SUC (count n)) 4850 ==> s SUBSET (IMAGE SUC (count n)) by IN_POW 4854 (2) s IN POW (IMAGE SUC (count n)) /\ 4855 s' IN POW (IMAGE SUC (count n)) /\ 4865 Now, s IN POW (IMAGE SUC (count n)) ==> s SUBSET (IMAGE SUC (count n)) by IN_POW 4866 s' IN POW (IMAGE SUC (count n)) ==> s' SUBSET (IMAGE SUC (count [all...] |
/seL4-l4v-master/HOL4/src/pred_set/src/ |
H A D | pred_setScript.sml | 3404 val count_def = new_definition ("count_def", ``count (n:num) = {m | m < n}``); 3407 !m n. m IN count n <=> m < n 3414 ``count 0 = {}``, 3421 ``!n. count (SUC n) = n INSERT count n``, 3427 ``!n. FINITE (count n)``, 3435 ``!n. CARD (count n) = n``, 3444 ("COUNT_11", ``!n1 n2. (count n1 = count n2) <=> (n1 = n2)``, 3451 ("COUNT_DELETE", ``!n. count [all...] |
/seL4-l4v-master/graph-refine/ |
H A D | trace_refute.py | 78 count = 0 82 count += 1 83 fun_addrs_counts[f] = count
|
H A D | solver.py | 201 count = [0] variable 206 count[0] += 1 207 name = 'ex_%d_%d' % (random_name, count[0]) 679 lpars = responses[0].count ('(') 680 rpars = responses[0].count (')') 685 lpars += r.count ('(') 686 rpars += r.count (')')
|
/seL4-l4v-master/HOL4/examples/algebra/finitefield/ |
H A D | ffBasicScript.sml | 270 Since IMAGE $## univ(:num) = IMAGE $## (count p) by field_num_mod, MOD_LESS 283 `IMAGE $## univ(:num) = IMAGE $## (count p)` by 552 = CARD (count (char r)) by GF_property 732 Note (ZN n).carrier = count n by ZN_eval 736 x IN (count n) ==> x IN IMAGE ((ZN n).sum.exp 1) univ(:num) 749 `(ZN n).carrier = count n` by rw[ZN_eval] >>
|
/seL4-l4v-master/HOL4/src/probability/ |
H A D | real_measureScript.sml | 320 measure m (BIGUNION (IMAGE f (count n))))``, 383 lam (BIGUNION (IMAGE f (count n)) INTER g))``, 531 `(lam g = lam (BIGUNION (IMAGE f (count n)) INTER g) + 532 lam ((space gsig DIFF BIGUNION (IMAGE f (count n))) INTER g)) /\ 534 lam ((space gsig DIFF BIGUNION (IMAGE f (count n))) INTER g)` 537 >- (Suff `BIGUNION (IMAGE f (count n)) IN lambda_system gsig lam` 851 >> Q.EXISTS_TAC `\n. f n DIFF (BIGUNION (IMAGE f (count n)))` 853 `suminf (measure m o (\n. f n DIFF (BIGUNION (IMAGE f (count n)))))` 865 `summable (measure m o (\n. f n DIFF (BIGUNION (IMAGE f (count n))))) /\ 866 suminf (measure m o (\n. f n DIFF (BIGUNION (IMAGE f (count [all...] |
/seL4-l4v-master/HOL4/src/pred_set/src/more_theories/ |
H A D | cardinalScript.sml | 748 ``A ** {} =~ count 1``, 760 ``{x} ** B =~ count 1 /\ A ** {x} =~ A``, 773 ``POW A =~ count 2 ** A``, 790 ``A ** count n =~ { l | (LENGTH l = n) /\ !e. MEM e l ==> e IN A }``, 907 ``INFINITE A /\ 0 < n ==> A ** count n =~ A``, 912 `A ** (n INSERT count n) =~ A CROSS A ** count n` 914 `A ** count n =~ A` by simp[] >> 915 `A CROSS A ** count n =~ A CROSS A` by metis_tac[CARDEQ_CROSS, cardeq_REFL] >> 985 ``list A =~ BIGUNION (IMAGE (\n. A ** count [all...] |
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | xwindows.cpp | 2408 int count; local 2415 info = XGetVisualInfo(DEREFDISPLAYHANDLE(dsHandle)->display,VisualIDMask,&T,&count); 2762 int up,down; /* count of button transitions */ 3029 PolyWord count; /* ML int */ member in struct:__anon26 3056 PolyWord count; /* ML int */ member in struct:__anon29 3333 data->count = DEREFWORD(Make_arbitrary_precision(taskData, 0)); 3353 data->count = DEREFWORD(Make_arbitrary_precision(taskData, ev->xgraphicsexpose.count)); 4479 int count; local 4483 cmaps = XListInstalledColormaps(DEREFDISPLAYHANDLE(dsHandle)->display,drawable,&count); 5068 int count; local 5108 int count; local 5133 int count; local 5591 int count; local 5631 int count; local 5657 int count; local [all...] |
H A D | processes.cpp | 396 /* A mutex was locked i.e. the count was ~1 or less. We will have set it to 397 ~1. This code blocks if the count is still ~1. It does actually return 444 /* Unlock a mutex. Called after decrementing the count and discovering 1465 // The loop count has expired and there is at least one thread that hasn't exited. 1483 // We also count the number of threads in ML code. Taking the 1794 // by each ML thread and increments the count for each thread that has used a 2157 unsigned count = 0; local 2165 while (i < count && cpus[i] != n) i++; 2166 if (i == count) cpus[count [all...] |
/seL4-l4v-master/HOL4/examples/AKS/theories/ |
H A D | AKScleanScript.sml | 329 reducePQ_subset |- !p q k. 0 < k ==> reducePQ p q k SUBSET count k 2383 (* Theorem: 0 < k ==> (reducePQ p q k) SUBSET (count k) *) 2386 Thus (reducePQ p q k) SUBSET (count k) by reducePQ_def, SUBSET_DEF 2390 ``!p q k. 0 < k ==> (reducePQ p q k) SUBSET (count k)``, 2396 Note (reducePQ p q k) SUBSET (count k) by reducePQ_subset, 0 < k 2397 and FINITE (count k) by FINITE_COUNT 2407 Note (reducePQ p q k) SUBSET (count k) by reducePQ_subset, 0 < k 2408 and FINITE (count k) by FINITE_COUNT 2409 ==> CARD (reducePQ p q k) <= CARD (count k) by CARD_SUBSET 2469 Since M SUBSET count [all...] |
/seL4-l4v-master/HOL4/examples/miller/prob/ |
H A D | prob_uniformScript.sml | 611 0 < n /\ a SUBSET count n ==> 643 >> Suff `e IN count (SUC n')` >- RW_TAC bool_ss [SPECIFICATION, IN_COUNT] 649 0 < n /\ a SUBSET count n /\ 2 * log2 (n + 1) <= t ==>
|
/seL4-l4v-master/HOL4/examples/algebra/monoid/ |
H A D | monoidScript.sml | 649 The map (count (SUC c)) -> G such that n -> x ** n is: 652 But c < SUC c = CARD (count (SUC c)), and this contradicts the Pigeon-hole Principle. 660 `INJ (\n. x ** n) (count (SUC c)) G` by rw[INJ_DEF] >>
|
/seL4-l4v-master/HOL4/tools/mllex/ |
H A D | mllex.sml | 511 | "count" => COUNT 930 val count = ref 0 value 1018 (count := !count+1; 1068 msg ("\nNumber of distinct rows = " ^ (Int.toString (!count))); 1070 (Int.toString (!count*(!CharSetSize)*(if !CharFormat then 1 else 8))));
|
/seL4-l4v-master/HOL4/examples/logic/ltl/ |
H A D | generalHelpersScript.sml | 119 `FINITE {f' n | n ��� count b }` suffices_by fs[IN_ABS,count_def] 1512 >> `U ��� (count N)` by ( 1553 `{a | ?k. a = (f i + k) MOD N } = count N` by ( 1560 >> `n ��� count N` by simp[count_def] 1569 >> `U = count N` 1573 by (`f i ��� count N` suffices_by metis_tac[] >> fs[count_def])
|
H A D | buechiAScript.sml | 63 ��� (a, r (j+1)) ��� aut.trans (r j) ��� at x j ��� a} DIFF (count k)` by ( 67 >> `FINITE (count k)` by metis_tac[FINITE_COUNT]
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | ConseqConv.sig | 221 not count 375 not count
|
/seL4-l4v-master/HOL4/examples/AKS/compute/ |
H A D | computeBasicScript.sml | 261 c <- 0 // initial count 263 c <- c + 1 // increment count 1977 c <- 1 // initial count, when j = 1, always coprime j n 1979 if (coprime j n) c <- c + 1 // increment count if coprime j n 1988 count_coprime n j k = (* j = n downto 1, k = count from 0 *) 1989 if 1 < j then (* decrement j, and update count k depending on coprime j n *) 1997 count_coprime n j = (* j = n downto 1, return count from 1 *) 1998 if 1 < j then (* decrement j, and update count k depending on coprime j n *)
|
/seL4-l4v-master/isabelle/src/Pure/General/ |
H A D | mercurial.scala | 203 lines.count(header) == 1 && {
|
/seL4-l4v-master/l4v/isabelle/src/Pure/General/ |
H A D | mercurial.scala | 203 lines.count(header) == 1 && {
|
/seL4-l4v-master/HOL4/examples/elliptic/ |
H A D | Useful.sig | 122 (* Lists: note we count elements from 0 *)
|