Searched refs:count (Results 151 - 175 of 240) sorted by relevance

12345678910

/seL4-l4v-10.1.1/HOL4/src/pred_set/src/
H A Dpred_setScript.sml3216 val count_def = new_definition ("count_def", ``count (n:num) = {m | m < n}``);
3220 ``!m n. m IN count n = m < n``,
3226 ``count 0 = {}``,
3233 ``!n. count (SUC n) = n INSERT count n``,
3239 ``!n. FINITE (count n)``,
3247 ``!n. CARD (count n) = n``,
3257 ``(count n1 = count n2) <=> (n1 = n2)``,
3696 val NOT_IN_COUNT = Q.prove (`~ (m IN count
[all...]
H A Dpred_setSyntax.sml63 val (count_tm, mk_count, dest_count, is_count) = s1 "count"
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/
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])
H A DBase.sml852 return a count of the number actually assigned. *)
877 val count = List.length l value
881 val vec = malloc(Word.fromInt count * sizea)
885 (vec, count)
/seL4-l4v-10.1.1/HOL4/src/holyhammer/legacy/
H A Dhh_tac.ml329 ((fun ty -> let count = !gcounter in
330 (gcounter := count + 1;
331 mk_var("_"^(string_of_int count),ty))),
/seL4-l4v-10.1.1/HOL4/examples/miller/prob/
H A Dprob_uniformScript.sml618 0 < n /\ a SUBSET count n ==>
650 >> Suff `e IN count (SUC n')` >- RW_TAC bool_ss [SPECIFICATION, IN_COUNT]
656 0 < n /\ a SUBSET count n /\ 2 * log2 (n + 1) <= t ==>
H A DprobScript.sml1635 (Q.SPECL [`f`, `n`, `count n`]
1745 BIJ c (count n) (range (FST o f)) ==>
1753 BIGUNION (IMAGE (\m. $= (c m) o FST o f) (count n))`
1754 >- (Suff `BIGUNION (IMAGE (\m. $= (c m) o FST o f) (count n)) = UNIV`
1788 (count n))) =
1792 (count n))) +
1897 (?c n. BIJ c (count n) (range (FST o f)))``,
2565 (IMAGE (\n. {s | ~c (FST (FUNPOW (UNCURRY b) n (a,s)))}) (count m))`
2966 (count m)))`
3067 (count
[all...]
/seL4-l4v-10.1.1/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-10.1.1/HOL4/examples/logic/ltl/
H A DgeneralHelpersScript.sml118 `FINITE {f' n | n ��� count b }` suffices_by fs[IN_ABS,count_def]
1511 >> `U ��� (count N)` by (
1552 `{a | ?k. a = (f i + k) MOD N } = count N` by (
1559 >> `n ��� count N` by simp[count_def]
1568 >> `U = count N`
1572 by (`f i ��� count N` suffices_by metis_tac[] >> fs[count_def])
H A DbuechiAScript.sml62 ��� (a, r (j+1)) ��� aut.trans (r j) ��� at x j ��� a} DIFF (count k)` by (
66 >> `FINITE (count k)` by metis_tac[FINITE_COUNT]
/seL4-l4v-10.1.1/HOL4/src/1/
H A DConseqConv.sig221 not count
375 not count
/seL4-l4v-10.1.1/seL4/src/arch/x86/kernel/
H A Dboot.c227 for (i = 0; i < mem_p_regs.count; i++) {
/seL4-l4v-10.1.1/HOL4/examples/elliptic/
H A DUseful.sig122 (* Lists: note we count elements from 0 *)
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibSupport.sml136 if small_space (M.size m) n (length (FV fm)) 1 then M.count m fm
H A DmlibUseful.sig58 (* Lists: note we count elements from 0 *)
H A DmlibModel.sml422 fun count m fm = function
432 chat ("count: " ^ formula_to_string fm ^ ": " ^
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A DHM_Core_Cline.sml138 (wn "Ignoring non-positive job count"; t)
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.1/official-semantics/
H A DSyntacticSugarScript.sml149 `count = NUM of num (* number *)
/seL4-l4v-10.1.1/HOL4/examples/diningcryptos/
H A Dextra_realScript.sml1168 (!n. 0 <= f n) /\ INJ j1 (count n1) UNIV /\
1169 IMAGE j1 (count n1) SUBSET IMAGE j2 (count n2) ==>
1262 Q.SPECL [`h`, `s`, `count N INTER s`] o
1265 >> Know `FINITE (count N INTER s)`
1336 Q.SPECL [`h`, `s`, `count n INTER s`] o
1339 >> Know `FINITE (count n INTER s)`
/seL4-l4v-10.1.1/HOL4/src/datatype/
H A Dind_types.sml302 val count = ref 0 value
305 temp_binding (safepfx ^ current_theory() ^ Int.toString (!count))
307 if (not (null (decls nm))) then (count := !count + 100;
309 else (count := !count + 1; nm)
/seL4-l4v-10.1.1/HOL4/src/real/
H A DseqScript.sml1767 ?k. IMAGE f (count N) SUBSET count k CROSS count k``,
1786 ?N. count k CROSS count k SUBSET IMAGE f (count N)``,
1789 Q.SPECL [`f`, `UNIV CROSS UNIV`, `count k CROSS count k`] o
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/
H A Darm_seq_monadScript.sml807 let count = FST (coprocessors.load_count inst coprocessors.state)
810 (forT 0 (count - 1) readm)
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/model/
H A Darm_seq_monadScript.sml813 let count = FST (coprocessors.load_count inst coprocessors.state)
816 (forT 0 (count - 1) readm)
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/
H A Dgc_share_phase.cpp128 void sortList(PolyObject *head, POLYUNSIGNED nItems, POLYUNSIGNED &count);
375 // Clear the entries in the hash table but not the sharing count.
468 // Clear the entries in the hash table but not the sharing count.
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/
H A DX86FOREIGNCALL.sml184 | _ => raise InternalError "rtsCall: Abi/argument count not implemented"
283 | _ => raise InternalError "rtsCall: Abi/argument count not implemented"

Completed in 186 milliseconds

12345678910