/seL4-l4v-master/HOL4/Manual/Quick/ |
H A D | quick.tex | 298 \hol{Count}{apply} \var{function} & returns the theorem count for a function application \\
|
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
H A D | misc.tex | 809 incremented. A total count as well as counts per primitive inference 848 the argument \ml{x} and performs a count of inferences during this
|
/seL4-l4v-master/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-master/HOL4/Manual/Tutorial/ |
H A D | tool.tex | 450 count of the number of intermediate theorems that are generated (which 1325 inference count.
|
/seL4-l4v-master/HOL4/examples/ARM/v4/mlton/ |
H A D | evalML.sml | 389 fun print_state fname state count = 396 TextIO.output(ostrm,"Instuctions Run:" ^ Int.toString count ^ "\n"); 528 val count = ref 0; value 533 let val _ = count := !count + 1 536 val _ = printer watches (!count) s ns 577 val _ = print_state "run.out" final_state (!count);
|
/seL4-l4v-master/HOL4/examples/ARM/v7/ |
H A D | armLib.sml | 232 val count = pad 8 o pad0 4 o lower o toHexString value 234 List.app (fn (n,i) => output_code ostrm (count (start + n)) i)
|
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 | 3095 let val count = bit_count list in value 3113 if count = 1 andalso not narrow_okay then 3144 if count = 1 then 3170 val count = bit_count list value 3198 if count = 1 andalso not narrow_okay then
|
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/v7/eval/ |
H A D | emit_eval.sig | 32 count (* max number of cycles, -ve for unbounded *)
|
H A D | emit_eval.sml | 305 "count leading zeroes" 684 fun arm_run trace prog options count = 688 ptree_arm_run trace (prog, state) count 701 val count = input_number (fn i => ~1 <= i) "Enter number of cycles: " value 703 case time (arm_run (int_to_trace trace) prog options) count
|
/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)
|
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-master/HOL4/examples/HolCheck/ |
H A D | ksTools.sml | 119 (* we do not count any atomic propositions over next state variables since by defn AP's are :state->bool *)
|
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-master/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] *)
|
H A D | SyntacticSugarScript.sml | 149 `count = NUM of num (* number *)
|
/seL4-l4v-master/HOL4/examples/acl2/examples/M1/ |
H A D | hol_defaxiomsScript.sml | 2183 > Matt says: The measure for (expt r i) is (abs (ifix i)). Intuitively, we count 2184 > down for positive exponents and count up for negative exponents
|
/seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | hol_defaxiomsScript.sml | 2153 > Matt says: The measure for (expt r i) is (abs (ifix i)). Intuitively, we count 2154 > down for positive exponents and count up for negative exponents
|
/seL4-l4v-master/HOL4/examples/acl2/examples/ |
H A D | testEncode.sml | 467 val count_def = Define ` (count (Branch []) = 0n) /\ 468 (count (Branch ((x,hd)::tl)) = 1 + count (hd:num rose_tree) + count (Branch tl))`;
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | hol_defaxiomsScript.sml | 2149 > Matt says: The measure for (expt r i) is (abs (ifix i)). Intuitively, we count 2150 > down for positive exponents and count up for negative exponents
|
H A D | testACL2encoding.ml | 23 let val (count,results) = type_tests 26 (count := (!count) + 1 ; 28 int_to_string (!count),failed) :: (!results))
|
/seL4-l4v-master/HOL4/examples/dev/Fact32/ |
H A D | NOT32.ml | 38 let val count = !NOT32vInst_count 39 val _ = (NOT32vInst_count := count+1); 40 val inst_name = "NOT32" ^ "_" ^ Int.toString count
|
H A D | exor32.ml | 71 let val count = !XOR32vInst_count 72 val _ = (XOR32vInst_count := count+1); 73 val inst_name = "XOR32" ^ "_" ^ Int.toString count
|