/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | FinalPolyML.sml | 1365 | lookupValues (EnvVConstr(name, ty, nullary, count, location) :: ntl, valu :: vl) s = 1367 then SOME(makeConstructor state (name, ty, nullary, count, location, valu)) 1389 | allValues (EnvVConstr(name, ty, nullary, count, location) :: ntl, valu :: vl) = 1390 (name, makeConstructor state (name, ty, nullary, count, location, valu)) :: allValues(ntl, vl) 2025 fun doPrint (count, name) = 2027 val cPrint = Int.toString count
|
H A D | Windows.sml | 427 (* The timeout and retry count apply only in the case of
|
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/ |
H A D | regexp_compilerScript.sml | 839 (frange regexp_compare state_map = count next_state) /\ 1002 (range state_map = count next_state) ��� 2052 >> `n'' IN count (LENGTH table)` by metis_tac [EXTENSION] 2070 >> `0n IN count (LENGTH table)` by metis_tac [EXTENSION]
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/prog/ |
H A D | mips_progLib.sml | 224 (fn "mips_prog$mips_CP0_Count" => K "count"
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/ |
H A D | dimacsTools.sml | 282 ** Changed by HA to not reverse order of clauses, and to return var count
|
/seL4-l4v-10.1.1/HOL4/src/rational/ |
H A D | ratLib.sml | 343 (* count all factors *)
|
/seL4-l4v-10.1.1/HOL4/examples/miller/prob/ |
H A D | prob_diceScript.sml | 304 >> Suff `{m | m <= n} = count (SUC n)` >- RW_TAC std_ss []
|
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | CooperShell.sml | 376 (* returns a-count and b-count for v in term t, with negp true if
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
H A D | arm_stepScript.sml | 3892 let count = n2w (4 * bit_count registers) in 3893 let address = if add then rn else rn - count in 3896 let address = address + (count - 4w) 4056 let count = 4 * bit_count registers in 4057 let base_address = if add then rn else rn - n2w count in 4063 constT (SOME (align (start_address,4) + n2w (count - 4))))) 4084 let count = 4 * bit_count registers in 4085 let base_address = if add then rn else rn - n2w count in
|
H A D | arm_encoderLib.sml | 1490 val count = StringCvt.padLeft #" " 8 o pad 4 o lower o toHexString 1492 app (fn (n,i) => print (count (start + n) ^ " " ^ i ^ "\n"))
|
H A D | arm_parserLib.sml | 3098 let val count = bit_count list in value 3116 if count = 1 andalso not narrow_okay then 3147 if count = 1 then 3173 val count = bit_count list value 3201 if count = 1 andalso not narrow_okay then
|
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/model/ |
H A D | arm_stepScript.sml | 3893 let count = n2w (4 * bit_count registers) in 3894 let address = if add then rn else rn - count in 3897 let address = address + (count - 4w) 4057 let count = 4 * bit_count registers in 4058 let base_address = if add then rn else rn - n2w count in 4064 constT (SOME (align (start_address,4) + n2w (count - 4))))) 4085 let count = 4 * bit_count registers in 4086 let base_address = if add then rn else rn - n2w count in
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
H A D | DEBUGGER_.sml | 220 and makeConstructor state (name, ty, nullary, count, location, valu) = 221 makeValueConstr(name, runTimeType state ty, nullary, count, Global(mkConst valu), location)
|
/seL4-l4v-10.1.1/HOL4/examples/diningcryptos/ |
H A D | dining_cryptosScript.sml | 1548 (pred_set$count (SUC(SUC(SUC n))))` 1559 (pred_set$count (SUC (SUC (SUC n))))`) CARD_UNION 1563 (pred_set$count (SUC (SUC (SUC n))))`) 1568 (pred_set$count (SUC (SUC (SUC n)))) INTER 1572 (pred_set$count (SUC (SUC (SUC n))))) = {}` 1586 (pred_set$count (SUC (SUC (SUC n))))) = CARD (pred_set$count (SUC (SUC (SUC n))))` 1592 `(pred_set$count (SUC (SUC (SUC (n:num)))))`, 1596 (pred_set$count (SUC (SUC (SUC (n:num)))))`]) CARD_IMAGE
|
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | SmtLib_Parser.sml | 262 need to count parentheses *)
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | stack_logic.py | 45 for (v, count) in var2.iteritems (): 47 var[v] += count
|
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/ |
H A D | alterAScript.sml | 268 >> `{i | b i ��� aut.final} ��� (count i)`
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | graph_specsLib.sml | 75 (mk_var("count",``:num``) |->
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/ |
H A D | kripke_structureScript.sml | 425 `?M. M = kripke_structure (IMAGE el (count (n+n0)))
|
/seL4-l4v-10.1.1/HOL4/Manual/Quick/ |
H A D | quick.tex | 298 \hol{Count}{apply} \var{function} & returns the theorem count for a function application \\
|
/seL4-l4v-10.1.1/HOL4/src/emit/ |
H A D | basis_emitScript.sml | 464 :: MLSIG "val count : num -> num set" 496 "val count : num -> num set", value
|
/seL4-l4v-10.1.1/HOL4/src/list/src/ |
H A D | ListConv1.sml | 713 fun iter count (d,lst) elty = 714 let val n = (ref count) and x = (ref d) and l = (ref lst)
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/ |
H A D | proof-tools.tex | 614 contate e aggiunte da \ml{count\_vars} alla map che si accumula, e la 617 La funzione \ml{count\_vars} ha la seguente implementazione:
|
H A D | tool.tex | 450 count of the number of intermediate theorems that are generated (which 1325 inference count.
|
/seL4-l4v-10.1.1/HOL4/Manual/Tutorial/ |
H A D | tool.tex | 450 count of the number of intermediate theorems that are generated (which 1325 inference count.
|