/seL4-l4v-10.1.1/HOL4/examples/unification/triangular/nominal/ |
H A D | nsubstScript.sml | 40 (`~INJ f (count (SUC (CARD (FDOM s)))) (FDOM s)`
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | profTools.sml | 32 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 D | locking.cpp | 250 // 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 D | Stream.sig | 24 val count : int -> int stream value
|
H A D | Stream.sml | 29 fun count n = Cons (n, fn () => count (n + 1)); function
|
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/ |
H A D | jedit_bibtex.scala | 115 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 D | Stream.sig | 24 val count : int -> int stream value
|
H A D | Stream.sml | 29 fun count n = Cons (n, fn () => count (n + 1)); function
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | jedit_bibtex.scala | 115 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 D | hfsScript.sml | 74 `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 D | m0Script.sml | 130 ("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 D | mlibTermorder.sml | 82 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 D | mlibMultiset.sml | 39 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 D | count.ml | 2 % FILE : count.ml % 10 new_theory `count`;;
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
H A D | Shape.sml | 79 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 D | real_sigmaScript.sml | 406 ``!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 D | buildcline.sml | 130 {help = "thread count", long = ["mt"], short = "", 131 desc = optInt "thread count" 0 #multithread},
|
/seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
H A D | scan.scala | 63 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 D | scan.scala | 63 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 D | holindex.lex | 74 %count
|
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/ |
H A D | gcdsetScript.sml | 20 { 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 D | emitter.py | 81 #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 D | Lexer.lex | 183 %count
|
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.1/official-semantics/ |
H A D | ExtendedSyntaxScript.sml | 86 | 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 D | ind_rel.sml | 619 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...] |