| /seL4-l4v-10.1.1/HOL4/examples/real-to-float/ |
| H A D | daisyLib.sml | 19 val strs = String.tokens (fn c => mem c cs) str value
20 val err = el 3 strs |> stringSyntax.fromMLstring
21 val lower = el 5 strs |> stringSyntax.fromMLstring
22 val upper = el 6 strs |> stringSyntax.fromMLstring
|
| /seL4-l4v-10.1.1/HOL4/examples/lambda/barendregt/ |
| H A D | reductionEval.sml | 290 val (strs, sets) = value
295 fun do_them (strs,sets) ys (w as (asl,g)) =
307 if HOLset.isEmpty strs then ALL_TAC
309 val avoid_t = mk_set (HOLset.listItems strs)
313 else if HOLset.isEmpty strs then let
319 val base = mk_set (HOLset.listItems strs)
337 do_them (HOLset.add(strs,newname_t), sets) rest
341 do_them (strs,sets) y_fvs
|
| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | stats.py | 203 def strs (seconds): function in function:print_total_time
205 print 'Slowest problem: %ss (%s)' % strs (time_vals[-1])
206 print 'Total time: %ss (%s)' % strs (sum (time_vals))
|
| H A D | graph-refine.py | 269 strs = [pair.funs[pair.tags[0]] for pair in pairs if pair]
270 return ' '.join (strs)
|
| /seL4-l4v-10.1.1/HOL4/help/src-sml/ |
| H A D | Parsspec.sml | 57 | OPENspec strs => res
58 | INCLUDEspecs strs => res
|
| /seL4-l4v-10.1.1/HOL4/tools-poly/poly/ |
| H A D | Help.sml | 107 fun show name centerline initiallySought (strs : string Vector.vector) =
109 val lines = Vector.length strs
126 else if instr s (Vector.sub(strs, (i+curr) mod lines)) then
182 let val line = Vector.sub(strs, i)
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
| H A D | exportLib.sml | 101 val pat = ``Call next name args strs``
106 val (strs,ty) = tm |> rand |> listSyntax.dest_list value
108 val strs = strs |> map stringSyntax.fromHOLstring value
112 in (next,name,args,strs) end
|
| /seL4-l4v-10.1.1/HOL4/examples/lambda/basics/ |
| H A D | binderLib.sml | 153 fun find_avoids (t, (strs, sets)) = let
173 (addList(strs,strings), addList(addList(sets, fv_terms), stringsets))
184 val (strs, sets) = List.foldl find_avoids (empty_tmset, empty_tmset) (w::asl) value
206 fun do_one used strs sets' (g as (asl, w)) =
231 List.foldl mk_union (mk_set (HOLset.listItems strs)) sets'
246 (HOLset.add(strs,new_t))
253 do_one empty_tmset strs sets' g
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
| H A D | compiler.sml | 270 val (th,strs) = arm_compilerLib.arm_compile (SPEC_ALL def) ind (!style)
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
| H A D | DEBUGGER_.sml | 323 fun makeStructDebugEntries (strs: structVals list, debugEnv, level, lex, mkAddr) =
337 updateState (level, mkAddr) (List.foldl loadStruct ([], debugEnv) strs)
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw2/examples/ |
| H A D | arm_compiler_demoScript.sml | 44 val (th,strs) = arm_compile def ind as_proc
45 (* val _ = map print (["\n\n\n"] @ strs @ ["\n\n\n"]) *)
|
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
| H A D | lisp_extractLib.sml | 870 val strs = listSyntax.mk_list(map fromMLstring params,``:string``) value
871 val x1 = pairSyntax.mk_pair(strs,body)
|
| /seL4-l4v-10.1.1/l4v/tools/haskell-translator/ |
| H A D | lhs_pars.py | 546 strs = [str(bit) for bit in bits]
547 return ' '.join(strs)
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
| H A D | TYPECHECK_PARSETREE.sml | 904 val strs = List.mapPartial findStructure ptl value
969 val () = List.app copyEntries strs;
|