/seL4-l4v-master/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-master/HOL4/examples/lambda/barendregt/ |
H A D | reductionEval.sml | 298 val (strs, sets) = value 303 fun do_them (strs,sets) ys (w as (asl,g)) = 315 if HOLset.isEmpty strs then ALL_TAC 317 val avoid_t = mk_set (HOLset.listItems strs) 321 else if HOLset.isEmpty strs then let 327 val base = mk_set (HOLset.listItems strs) 345 do_them (HOLset.add(strs,newname_t), sets) rest 349 do_them (strs,sets) y_fvs
|
/seL4-l4v-master/graph-refine/ |
H A D | stats.py | 209 def strs (seconds): function in function:print_total_time 211 print 'Slowest problem: %ss (%s)' % strs (time_vals[-1]) 212 print 'Total time: %ss (%s)' % strs (sum (time_vals))
|
H A D | graph-refine.py | 267 strs = [pair.funs[pair.tags[0]] for pair in pairs if pair] 268 return ' '.join (strs)
|
/seL4-l4v-master/HOL4/help/src-sml/ |
H A D | Parsspec.sml | 57 | OPENspec strs => res 58 | INCLUDEspecs strs => res
|
/seL4-l4v-master/HOL4/src/postkernel/ |
H A D | ThyDataSexp.sml | 170 fun sterms0 (s, acc as (strs,tms)) = 173 | SharedString s => (s::strs,tms) 174 | Term tm => (strs,tm::tms) 175 | Thm th => (strs, concl th :: (hyp th @ tms)) 176 | Type ty => (strs, Term.mk_var("x", ty) :: tms) 178 | KName{Thy,Name} => (Thy::Name::strs,tms)
|
H A D | SharingTables.sml | 332 fun add_strings strs (SDI {strtable,idtable,tytable,tmtable,exp}) = 334 val strtable = List.foldl str1 strtable strs
|
/seL4-l4v-master/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-master/HOL4/examples/machine-code/graph/ |
H A D | exportLib.sml | 102 val pat = ``Call next name args strs`` 107 val (strs,ty) = tm |> rand |> listSyntax.dest_list value 109 val strs = strs |> map stringSyntax.fromHOLstring value 115 in (next,name,args,strs) end
|
/seL4-l4v-master/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-master/HOL4/examples/dev/sw2/ |
H A D | compiler.sml | 268 val (th,strs) = arm_compilerLib.arm_compile (SPEC_ALL def) ind (!style)
|
/seL4-l4v-master/HOL4/examples/bootstrap/ |
H A D | automation_lemmasScript.sml | 550 val strs = map (fn v => mk_var(fst (dest_var v) ^ "_" ^ s,���:string���)) vs value 551 val nums = map (fn t => ���name ^t���) strs 559 val t2 = listSyntax.mk_list(strs,���:string���)
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | DEBUGGER_.sml | 339 fun makeStructDebugEntries (strs: structVals list, debugEnv, level, lex, mkAddr) = 353 updateState (level, mkAddr) (List.foldl loadStruct ([], debugEnv) strs)
|
/seL4-l4v-master/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-master/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
H A D | lisp_extractLib.sml | 881 val strs = listSyntax.mk_list(map fromMLstring params,``:string``) value 882 val x1 = pairSyntax.mk_pair(strs,body)
|
/seL4-l4v-master/l4v/tools/haskell-translator/ |
H A D | lhs_pars.py | 545 strs = [str(bit) for bit in bits] 546 return ' '.join(strs)
|
/seL4-l4v-master/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;
|