Searched refs:parameter (Results 1 - 25 of 117) sorted by relevance

12345

/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dgctaskfarm.h85 static void *WorkerThreadFunction(void *parameter);
88 static DWORD WINAPI WorkerThreadFunction(void *parameter);
H A Dgctaskfarm.cpp229 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 Dselftest.sml17 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 DsmlParallel.sig14 (* 'a: type of parameter, 'b: type of arguments, 'c: returned type *)
/seL4-l4v-master/HOL4/src/portableML/
H A DImplicitGraph.sig19 (* fold functions get passed distance from root as extra integer parameter.
/seL4-l4v-master/HOL4/examples/elliptic/c_output/
H A Dc_outputLib.sig15 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 DTermParse.sig44 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 Dparse_type.sig35 The parameter is set to true for parsing datatype definitions, where
/seL4-l4v-master/HOL4/examples/temporal_deep/src/translations/
H A DtranslationsLib.sig9 * 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 Dexor32.ml54 (* needed to set parameter "size" in XOR32vDef (termToVerilog_XOR32). *)
60 \ parameter size = 31;\n\
H A DNOT32.ml27 \ parameter size = 31;\n\
/seL4-l4v-master/HOL4/tools/
H A Dbuildutils.sig77 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 DDynarray.sig25 initialized to the default d. The parameter n is used as a hint of the
/seL4-l4v-master/HOL4/src/simp/src/
H A DCache.sig21 parameter to RCACHE is a function that when applied to a term that
/seL4-l4v-master/HOL4/examples/misc/
H A DcontMonadScript.sml14 the last parameter.
/seL4-l4v-master/HOL4/examples/AKS/compute/
H A DcomputeAKSScript.sml384 (* 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 DQuantHeuristics.tex175 \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 DQuantHeuristics.tex175 \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 DmonosetScript.sml80 parameter (which is the schematic variable) *)
/seL4-l4v-master/HOL4/examples/temporal_deep/src/model_check/
H A DmodelCheckLib.sig9 make these lib work. Thus maker sure, the parameter smv_path of temporalLib
/seL4-l4v-master/HOL4/examples/AKS/machine/
H A DcountParamScript.sml2 (* 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 DjrhTactics.sml51 (* the first parameter n is used to record the rotations performed
/seL4-l4v-master/HOL4/polyml/Tests/
H A DRunTests.sml17 (* Max inline size is not available as a CP parameter and some tests
/seL4-l4v-master/HOL4/examples/fsub/
H A Dkernel_subtypingScript.sml80 (* define algorithmic sub-typing, with a depth of derivation parameter *)
126 parameter *)
/seL4-l4v-master/HOL4/examples/AKS/theories/
H A DAKStheoremScript.sml616 (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 *)

Completed in 118 milliseconds

12345