/seL4-l4v-master/HOL4/src/IndDef/ |
H A D | selftest.sml | 109 (* isolate_to_front test cases *)
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Unix.sml | 85 need to test whether we have an executable at the beginning.
|
/seL4-l4v-master/HOL4/examples/bootstrap/ |
H A D | automation_lemmasScript.sml | 599 (* test *) 602 test source_syntax$Equal = Name "Equal" ��� 603 test source_syntax$Less = Name "Less" 641 exp (If t xs e1 e2) = list [Name "If"; test t; list (MAP exp xs); exp e1; exp e2] ���
|
/seL4-l4v-master/HOL4/src/AI/ |
H A D | aiLib.sml | 230 fun first_test_n test n l = 233 else if test (hd l) 234 then hd l :: first_test_n test (n - 1) (tl l) 235 else first_test_n test n (tl l)
|
/seL4-l4v-master/HOL4/src/tactictoe/src/ |
H A D | tttRecord.sml | 70 " tactic test: " ^ rts_round 6 (!ortho_teststac_time) ^ ")",
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | gc_share_phase.cpp | 272 bool test = TestForScan(&pWord); local 275 if (test) 549 // locked will now be immutable. The test in TestForScan is bypassed
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_FUNCTIONS.sml | 75 | codeProps (TagTest{ test, ... }) = codeProps test 588 | checkUse isMain (TagTest{test, ...}, cl, _) = checkUse isMain (test, cl -- 1, false)
|
H A D | BaseCodeTreeSig.sml | 114 | TagTest of { test: codetree, tag: word, maxTag: word }
|
/seL4-l4v-master/HOL4/src/datatype/mutrec/ |
H A D | MutRecDef.sml | 67 fun find test [] = NONE 68 | find test (x::xs) = if test x then SOME x else find test xs 358 type; otherwise we need to test that the return values
|
/seL4-l4v-master/HOL4/examples/elliptic/c_output/ |
H A D | c_outputLib.sml | 665 (*write test*) 666 val file_name_test = filename^"-test.c";
|
/seL4-l4v-master/HOL4/src/portableML/poly/concurrent/ |
H A D | Future.sml | 205 val test = Exn.capture Thread_Attributes.expose_interrupt (); value 207 if ok andalso not (Exn.is_interrupt_exn test) then ()
|
/seL4-l4v-master/HOL4/examples/PSL/path/ |
H A D | PSLPathScript.sml | 353 * LESS m is predicate to test if a number is less than m 360 * LESSX m is predicate to test if a number is less than extended number m
|
/seL4-l4v-master/HOL4/examples/acl2/examples/LTL/ |
H A D | LTLScript.sml | 334 ; Same test as the transition-subset-p test above!
|
/seL4-l4v-master/HOL4/src/q/ |
H A D | Q.sml | 490 fun test (pat, thetasz) (bvs, subt) = function 509 (case gen_find_term (test patsz) t of
|
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | Portable.sml | 377 fun subst_assoc test = 381 if test redex then SOME residue else assc rst
|
/seL4-l4v-master/HOL4/examples/AKS/machine/ |
H A D | countPrimeScript.sml | 197 (* Primality test by seeking factor up to (1 + SQRT n) *) 597 (* Thus the traditional primality test by trial factors is not polynomial-time in (ulog n). *)
|
/seL4-l4v-master/HOL4/src/holyhammer/ |
H A D | hhExportTh0.sml | 170 (* test term 210 (* test term
|
H A D | hhExportTf0.sml | 135 (* test term 175 (* test term
|
/seL4-l4v-master/HOL4/src/AI/machine_learning/ |
H A D | mlReinforce.sml | 308 fun test (_,(_,winl)) = null winl orelse not (hd winl) 309 val (neg,pos) = partition test targetwinl
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | Overload.sml | 382 fun test ((fvs, pat), (orig, nm, tstamp)) = let function 399 val inst_data = List.mapPartial test matches
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | CODEGEN_PARSETREE.sml | 539 | codeGenerate(Cond {test, thenpt, elsept, thenBreak, elseBreak, ...}, context) = 541 val (testCode, testEnv) = codeGenerate(test, context) 742 | codeGenerate(While {test, body, breakPoint, ...}, context as { debugEnv, ...}) = 744 val (testCode, testEnv) = codeGenerate(test, context) 752 | codeGenerate(c as Case {test, match, ...}, context as { debugEnv, ...}) = 754 applied to the test expression. *) 756 val testCode = codegen (test, context) 1231 (* The old test was "totalArgs = 1", but that's not really
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | ACF.sml | 184 (* Predicate to test whether a term occurs in another term *)
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | stringBinTree.sml | 47 (*apply first arg(conv) to test part of the cond term which is on the rhs of the snd arg (an eq term)*)
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | testTypesScript.sml | 132 (* Some examples from src/datatype/jrh.test *)
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | metis.sml | 85 {switches = ["--test"], arguments = [],
|