/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibSupport.sml | 136 if small_space (M.size m) n (length (FV fm)) 1 then M.count m fm
|
H A D | mlibUseful.sig | 58 (* Lists: note we count elements from 0 *)
|
H A D | mlibModel.sml | 423 fun count m fm = function 433 chat ("count: " ^ formula_to_string fm ^ ": " ^
|
/seL4-l4v-master/HOL4/src/pred_set/src/ |
H A D | pred_setSyntax.sml | 63 val (count_tm, mk_count, dest_count, is_count) = s1 "count"
|
/seL4-l4v-master/HOL4/examples/PSL/1.1/official-semantics/ |
H A D | SyntacticSugarScript.sml | 149 `count = NUM of num (* number *)
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | HM_Core_Cline.sml | 141 (wn "Ignoring non-positive job count"; t)
|
/seL4-l4v-master/HOL4/src/prekernel/ |
H A D | Lib.sig | 61 val extract_pc : string -> string * int (* "pc" = "prime count" *)
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | testutils.sml | 102 (print ("Failure count = " ^ Int.toString (!iref) ^ "\n");
|
/seL4-l4v-master/HOL4/src/datatype/ |
H A D | ind_types.sml | 311 val count = ref 0 value 314 temp_binding (safepfx ^ current_theory() ^ Int.toString (!count)) 316 if (not (null (decls nm))) then (count := !count + 100; 318 else (count := !count + 1; nm)
|
/seL4-l4v-master/HOL4/examples/algebra/ring/ |
H A D | ringInstancesScript.sml | 84 ZN_def |- !n. ZN n = <|carrier := count n; sum := add_mod n; prod := times_mod n|> 85 ! ZN_eval |- !n. ((ZN n).carrier = count n) /\ 303 <| carrier := count n; 323 ``!n. ((ZN n).carrier = count n) /\ 384 `!x. x IN count n <=> x < n` by rw[] >> 488 If n = 1, (ZN 1).carrier = count 1 = {0}
|
/seL4-l4v-master/HOL4/examples/ARM/v7/ |
H A D | arm_seq_monadScript.sml | 807 let count = FST (coprocessors.load_count inst coprocessors.state) 810 (forT 0 (count - 1) readm)
|
/seL4-l4v-master/HOL4/examples/ARM_security_properties/model/ |
H A D | arm_seq_monadScript.sml | 813 let count = FST (coprocessors.load_count inst coprocessors.state) 816 (forT 0 (count - 1) readm)
|
/seL4-l4v-master/isabelle/src/Tools/Graphview/ |
H A D | layout.scala | 236 .count(inner_child => outer_child < inner_child)).sum).sum
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Graphview/ |
H A D | layout.scala | 236 .count(inner_child => outer_child < inner_child)).sum).sum
|
/seL4-l4v-master/HOL4/src/real/ |
H A D | seqScript.sml | 1768 ?k. IMAGE f (count N) SUBSET count k CROSS count k``, 1787 ?N. count k CROSS count k SUBSET IMAGE f (count N)``, 1790 Q.SPECL [`f`, `UNIV CROSS UNIV`, `count k CROSS count k`] o
|
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/ |
H A D | Base.sml | 844 return a count of the number actually assigned. *) 869 val count = List.length l value 873 val vec = malloc(Word.fromInt count * sizea) 877 (vec, count)
|
/seL4-l4v-master/HOL4/tools/ |
H A D | holscript-mode.el | 521 (let* ((count (- tab-width (mod (current-column) tab-width)))) 522 (dotimes (i count) (insert " "))))))
|
/seL4-l4v-master/HOL4/examples/fermat/little/ |
H A D | FLTactionScript.sml | 65 Zadd_def |- !n. Zadd n = <|carrier := count n; 169 (* |- !n. Zadd n = <|carrier := count n; id := 0; op := (\i j. (i + j) MOD n)|> *) 175 (* val Zadd_carrier = |- !n. (Zadd n).carrier = count n: thm *)
|
/seL4-l4v-master/HOL4/examples/miller/prob/ |
H A D | probScript.sml | 1611 (Q.SPECL [`f`, `n`, `count n`] 1721 BIJ c (count n) (range (FST o f)) ==> 1729 BIGUNION (IMAGE (\m. $= (c m) o FST o f) (count n))` 1730 >- (Suff `BIGUNION (IMAGE (\m. $= (c m) o FST o f) (count n)) = UNIV` 1764 (count n))) = 1768 (count n))) + 1873 (?c n. BIJ c (count n) (range (FST o f)))``, 2541 (IMAGE (\n. {s | ~c (FST (FUNPOW (UNCURRY b) n (a,s)))}) (count m))` 2942 (count m)))` 3043 (count [all...] |
H A D | prob_diceScript.sml | 298 >> Suff `{m | m <= n} = count (SUC n)` >- RW_TAC std_ss []
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | FinalPolyML.sml | 1369 | lookupValues (EnvVConstr(name, ty, nullary, count, location) :: ntl, valu :: vl) s = 1371 then SOME(makeConstructor state (name, ty, nullary, count, location, valu)) 1393 | allValues (EnvVConstr(name, ty, nullary, count, location) :: ntl, valu :: vl) = 1394 (name, makeConstructor state (name, ty, nullary, count, location, valu)) :: allValues(ntl, vl) 2029 fun doPrint (count, name) = 2031 val cPrint = Int.toString count
|
/seL4-l4v-master/HOL4/examples/algebra/polynomial/ |
H A D | polyMultiplicityScript.sml | 253 Claim: s SUBSET count (SUC (deg p)) 266 Since FINITE (count (SUC (deg p))) by FINITE_COUNT 279 `s SUBSET count (SUC (deg p))` by
|
/seL4-l4v-master/HOL4/src/HolSat/ |
H A D | dimacsTools.sml | 299 ** Changed by HA to not reverse order of clauses, and to return var count
|
/seL4-l4v-master/HOL4/src/rational/ |
H A D | ratLib.sml | 353 (* count all factors *)
|
/seL4-l4v-master/HOL4/examples/formal-languages/regular/ |
H A D | regexp_compilerScript.sml | 1070 (frange regexp_compare state_map = count next_state) /\ 1224 (range state_map = count next_state) /\ 2069 >> `n'' IN count (LENGTH table)` by metis_tac [EXTENSION] 2087 >> `0n IN count (LENGTH table)` by metis_tac [EXTENSION]
|