Searched refs:count (Results 76 - 100 of 240) sorted by relevance

12345678910

/seL4-l4v-10.1.1/HOL4/examples/unification/triangular/nominal/
H A DnsubstScript.sml40 (`~INJ f (count (SUC (CARD (FDOM s)))) (FDOM s)`
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/
H A DprofTools.sml32 fun prc s = if !prf then print (s^".count = "^(Int.toString(find(!cnt,s)))^"\n") else ()
46 (* timers (also have their own call count and inference count) *)
72 val _ = print ("count = "^(Int.toString(find(!cnt,s)))^"\t")
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/
H A Dlocking.cpp250 // The semaphore is initialised with a count of zero.
287 static int count=0;
288 sprintf(semname, "poly%0d-%0d", (int)getpid(), count++);
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DStream.sig24 val count : int -> int stream value
H A DStream.sml29 fun count n = Cons (n, fn () => count (n + 1)); function
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/
H A Djedit_bibtex.scala115 val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
148 handler.handleToken(line, JEditToken.END, line.count, 0, context1)
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DStream.sig24 val count : int -> int stream value
H A DStream.sml29 fun count n = Cons (n, fn () => count (n + 1)); function
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/
H A Djedit_bibtex.scala115 val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
148 handler.handleToken(line, JEditToken.END, line.count, 0, context1)
/seL4-l4v-10.1.1/HOL4/examples/hfs/
H A DhfsScript.sml74 `INJ f (count (bnd + 2)) (count (bnd + 1))`
76 `FINITE (count (bnd + 1))` by simp[] >>
77 `CARD (count (bnd + 1)) < CARD (count (bnd + 2))` by simp[] >>
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/model/
H A Dm0Script.sml130 ("SHPR2",CTy"SHPR2"),("SHPR3",CTy"SHPR3"),("VTOR",F32),("count",nTy),
2482 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 3)]))))
2495 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 3)]))))
2515 ("count",
2516 TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 4)])))))
2535 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 3)]))))
2608 ("count",
[all...]
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibTermorder.sml82 let val vars = vars @ [""] in fn eqn => map (M.count eqn) vars end;
137 fun trivial q = M.nonzero q=0 orelse M.nonzero q=1 andalso 0<M.count q "";
187 M.all (fn ("",_) => true | (v,i) => i <= M.count eqn2 v) eqn1 andalso
188 M.all (fn ("",_) => true | (v,i) => M.count eqn1 v <= i) eqn2 andalso
310 nicevar v :: map (int_to_string o M.count (B.find (tab,v))) vars
345 fun g (v,i,n) = n + M.count eqn v * i
H A DmlibMultiset.sml39 fun count m x = case M.peek (m,x) of SOME n => n | NONE => 0; function
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/mos-count/
H A Dcount.ml2 % FILE : count.ml %
10 new_theory `count`;;
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/
H A DShape.sml79 val (ptarr, count) = ptList pts
81 polygon (h, ptarr, count) handle ex => (Memory.free ptarr; raise ex);
/seL4-l4v-10.1.1/HOL4/src/real/
H A Dreal_sigmaScript.sml406 ``!f n. REAL_SUM_IMAGE f (pred_set$count n) =
410 >> `pred_set$count (SUC n) = n INSERT pred_set$count n`
413 >> `pred_set$count n DELETE n = pred_set$count n`
600 ("REAL_SUM_IMAGE_EQ_sum", ``!n r. sum (0,n) r = REAL_SUM_IMAGE r (count n)``,
605 >> Suff `count n DELETE n = count n`
/seL4-l4v-10.1.1/HOL4/tools/
H A Dbuildcline.sml130 {help = "thread count", long = ["mt"], short = "",
131 desc = optInt "thread count" 0 #multithread},
/seL4-l4v-10.1.1/isabelle/src/Pure/General/
H A Dscan.scala63 var count = 0
65 while (!finished && i < end && count < max_count) {
68 if (pred(sym)) { i += n; count += 1 }
71 if (count < min_count) Failure("bad input", in)
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/
H A Dscan.scala63 var count = 0
65 while (!finished && i < end && count < max_count) {
68 if (pred(sym)) { i += n; count += 1 }
71 if (count < min_count) Failure("bad input", in)
/seL4-l4v-10.1.1/HOL4/src/TeX/
H A Dholindex.lex74 %count
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/
H A DgcdsetScript.sml20 { n | n <= MIN_SET (s DELETE 0) } = count (MIN_SET (s DELETE 0) + 1)
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/chronos/
H A Demitter.py81 #The user specified a manual loop-count override
121 count, desc = emitted_loop_counts[bin_head]
122 self.emitted_loop_counts_file.write("0x%x : count %d, desc: %s\n" % ( bin_head, count, desc))
164 #if this is a loop head, emit its loop count
/seL4-l4v-10.1.1/HOL4/help/src-sml/
H A DLexer.lex183 %count
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.1/official-semantics/
H A DExtendedSyntaxScript.sml86 | ES_RANGE_REPEAT of esere # count (* r[*i] *)
88 | ES_RANGE_EQ_REPEAT of ebexp # count (* b[= i] *)
89 | ES_RANGE_GOTO_REPEAT of ebexp # count (* b[-> i] *)
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/
H A Dind_rel.sml619 ought to solve the goal. The count parameters keeps track of what
625 fun mk_more_tactics num_hyps count (hyp1::hyps) =
627 fun mk_still_more_tactics count =
628 if count < num_rules + num_hyps then
630 let val rule_thm = ASSUME (nth (rev asms, count))
633 end)::mk_still_more_tactics (count + 1)
642 let val rule_thm = ASSUME (nth (rev asms, count))
650 end::mk_more_tactics num_hyps (count + 1) hyps
653 fun mk_tactics count (rule::rules) =
667 (mk_tactics (count
[all...]

Completed in 165 milliseconds

12345678910