/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | gctaskfarm.h | 85 static void *WorkerThreadFunction(void *parameter); 88 static DWORD WINAPI WorkerThreadFunction(void *parameter);
|
H A D | gctaskfarm.cpp | 229 void *GCTaskFarm::WorkerThreadFunction(void *parameter) argument 231 GCTaskFarm *t = (GCTaskFarm *)parameter; 236 DWORD WINAPI GCTaskFarm::WorkerThreadFunction(void *parameter) argument 238 GCTaskFarm *t = (GCTaskFarm *)parameter;
|
/seL4-l4v-master/HOL4/src/tfl/src/ |
H A D | selftest.sml | 17 val def3 = test "Constant as parameter (=)" (Hol_defn "baz1") `baz1 x = (x /\ F)` 19 test "Constant as parameter (<=>)" (Hol_defn "baz2") `baz2 x <=> x /\ F` 21 test "Type-constrainted constant as parameter" 24 test "Constant as parameter under quantifier"
|
/seL4-l4v-master/HOL4/src/AI/sml_inspection/ |
H A D | smlParallel.sig | 14 (* 'a: type of parameter, 'b: type of arguments, 'c: returned type *)
|
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | ImplicitGraph.sig | 19 (* fold functions get passed distance from root as extra integer parameter.
|
/seL4-l4v-master/HOL4/examples/elliptic/c_output/ |
H A D | c_outputLib.sig | 15 the function main_func. The parameter tests is a list of pairs 25 each pair. The words are all less to max_word if max_word is not set to 0. Otherwise there is no limit. Finally, the parameter list_length
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | TermParse.sig | 44 For this reason, prim_ctxt_termS takes a function parameter which is given 46 is a good choice for this parameter: it is rebound (using a reference)
|
H A D | parse_type.sig | 35 The parameter is set to true for parsing datatype definitions, where
|
/seL4-l4v-master/HOL4/examples/temporal_deep/src/translations/ |
H A D | translationsLib.sig | 9 * and the ltl formula. The parameter t is used to determine the kind 24 * However, the implementation is more advanced. The parameter fast 48 * a model checker. The first parameter is always the knows fast switch
|
/seL4-l4v-master/HOL4/examples/dev/Fact32/ |
H A D | exor32.ml | 54 (* needed to set parameter "size" in XOR32vDef (termToVerilog_XOR32). *) 60 \ parameter size = 31;\n\
|
H A D | NOT32.ml | 27 \ parameter size = 31;\n\
|
/seL4-l4v-master/HOL4/tools/ |
H A D | buildutils.sig | 77 parameter is the user's specification of the selftest level. 80 additional arguments. The isSuccess parameter interprets
|
/seL4-l4v-master/HOL4/src/portableML/poly/ |
H A D | Dynarray.sig | 25 initialized to the default d. The parameter n is used as a hint of the
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | Cache.sig | 21 parameter to RCACHE is a function that when applied to a term that
|
/seL4-l4v-master/HOL4/examples/misc/ |
H A D | contMonadScript.sml | 14 the last parameter.
|
/seL4-l4v-master/HOL4/examples/AKS/compute/ |
H A D | computeAKSScript.sml | 384 (* Express AKS algorithm in terms of possible results of AKS parameter. *) 387 case aks_param n of (* search for AKS parameter given n *) 444 (* Express AKS algorithm in terms of possible results of AKS parameter. *) 447 case param n of (* search for AKS parameter given n *)
|
/seL4-l4v-master/HOL4/Manual/Description/ |
H A D | QuantHeuristics.tex | 175 \texttt{implication\_concl\_qp} is a quantifier parameter that looks for valid guesses in the conclusion of an implication. 280 There is a quantifier heuristic parameter called \holtxt{pair\_default\_qp}. It first looks for 283 is found, $x$ is instantiated as well. This parameter therefore allows simplifications like: 291 quantifier heuristic parameter \holtxt{pair\_qp}, which allows the 308 by \holtxt{record\_qp}. In contrast to the pair parameter, the one for records gets only one function instead of a 311 The quantifier heuristic parameter \holtxt{default\_record\_qp} expands all records. 315 The parameter for records is stateful, as it uses knowledge from 317 but for general datatypes. The quantifier heuristic parameter 326 The standard quantifier heuristic parameter \holtxt{std\_qp} combines 490 As an example, lets define a parameter tha [all...] |
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
H A D | QuantHeuristics.tex | 175 \texttt{implication\_concl\_qp} is a quantifier parameter that looks for valid guesses in the conclusion of an implication. 270 There is a quantifier heuristic parameter called \holtxt{pair\_default\_qp}. It first looks for 273 is found, $x$ is instantiated as well. This parameter therefore allows simplifications like: 281 quantifier heuristic parameter \holtxt{pair\_qp}, which allows the 298 by \holtxt{record\_qp}. In contrast to the pair parameter, the one for records gets only one function instead of a 301 The quantifier heuristic parameter \holtxt{default\_record\_qp} expands all records. 305 The parameter for records is stateful, as it uses knowledge from 307 but for general datatypes. The quantifier heuristic parameter 316 The standard quantifier heuristic parameter \holtxt{std\_qp} combines 480 As an example, lets define a parameter tha [all...] |
/seL4-l4v-master/HOL4/examples/ind_def/ |
H A D | monosetScript.sml | 80 parameter (which is the schematic variable) *)
|
/seL4-l4v-master/HOL4/examples/temporal_deep/src/model_check/ |
H A D | modelCheckLib.sig | 9 make these lib work. Thus maker sure, the parameter smv_path of temporalLib
|
/seL4-l4v-master/HOL4/examples/AKS/machine/ |
H A D | countParamScript.sml | 2 (* AKS parameter from Count Monad *) 63 (* AKS parameter with Count Monad Documentation *) 73 AKS parameter search in Monadic style: 191 (* AKS parameter search in Monadic style *) 231 (* Define the parameter seek loop *) 263 AKS parameter search: n=31, m=25 264 AKS parameter search: max=1562 265 AKS parameter k=29 276 (* To compute the AKS parameter k *)
|
/seL4-l4v-master/HOL4/src/meson/src/ |
H A D | jrhTactics.sml | 51 (* the first parameter n is used to record the rotations performed
|
/seL4-l4v-master/HOL4/polyml/Tests/ |
H A D | RunTests.sml | 17 (* Max inline size is not available as a CP parameter and some tests
|
/seL4-l4v-master/HOL4/examples/fsub/ |
H A D | kernel_subtypingScript.sml | 80 (* define algorithmic sub-typing, with a depth of derivation parameter *) 126 parameter *)
|
/seL4-l4v-master/HOL4/examples/AKS/theories/ |
H A D | AKStheoremScript.sml | 616 (2 * SUC (LOG2 n)) ** 2 <= ordz k n /\ (* parameter k *) 1229 (2 * ulog n) ** 2 <= ordz k n /\ (* parameter k *) 1550 !n a s. 0 < k /\ (a = (2 * SUC (LOG2 n)) ** 2) /\ (* parameter a *) 1551 (s = 2 * (SQRT (phi k)) * (SUC (LOG2 n))) /\ (* parameter s *) 1559 prime k /\ (a = (2 * SUC (LOG2 n)) ** 2) /\ (* parameter a *) 1560 (s = 2 * (SQRT (phi k)) * (SUC (LOG2 n))) /\ (* parameter s *) 1568 (a = (2 * SUC (LOG2 n)) ** 2) /\ (* parameter a *) 1569 (s = 2 * (SQRT (phi k)) * (SUC (LOG2 n))) /\ (* parameter s *)
|