Searched refs:count (Results 176 - 200 of 316) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/
H A DClipboard.sml274 val (vec, count) = list2Vector cCLIPFORMAT l
275 val res = getPriorityClipboardFormat(vec, count) handle ex => (Memory.free vec; raise ex)
H A DMenu.sml535 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 Dboot.c93 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 Dspell_checker.scala201 updates.valuesIterator.count(upd => !upd.permanent)
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/
H A Dspell_checker.scala201 updates.valuesIterator.count(upd => !upd.permanent)
/seL4-l4v-master/HOL4/examples/algebra/polynomial/
H A DpolyFieldModuloScript.sml4843 (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 Dpred_setScript.sml3404 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 Dtrace_refute.py78 count = 0
82 count += 1
83 fun_addrs_counts[f] = count
H A Dsolver.py201 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 DffBasicScript.sml270 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 Dreal_measureScript.sml320 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 DcardinalScript.sml748 ``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 Dxwindows.cpp2408 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 Dprocesses.cpp396 /* 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 DAKScleanScript.sml329 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 Dprob_uniformScript.sml611 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 DmonoidScript.sml649 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 Dmllex.sml511 | "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 DgeneralHelpersScript.sml119 `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 DbuechiAScript.sml63 ��� (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 DConseqConv.sig221 not count
375 not count
/seL4-l4v-master/HOL4/examples/AKS/compute/
H A DcomputeBasicScript.sml261 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 Dmercurial.scala203 lines.count(header) == 1 && {
/seL4-l4v-master/l4v/isabelle/src/Pure/General/
H A Dmercurial.scala203 lines.count(header) == 1 && {
/seL4-l4v-master/HOL4/examples/elliptic/
H A DUseful.sig122 (* Lists: note we count elements from 0 *)

Completed in 208 milliseconds

1234567891011>>