/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Sharing.sml | 49 val ys = y :: ys value 66 val ys = y :: ys value 90 val ys = if same then xs else y :: ys value 107 val ys = if same then xs else y :: ys value [all...] |
H A D | Options.sml | 226 val (ys,xs) = getArgs x r xs value
|
H A D | Rule.sml | 447 and ys = List.tabulate (n,yIVar) value 474 and ys = List.tabulate (n,yIVar) value
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Sharing.sml | 49 val ys = y :: ys value 66 val ys = y :: ys value 90 val ys = if same then xs else y :: ys value 107 val ys = if same then xs else y :: ys value [all...] |
H A D | Options.sml | 226 val (ys,xs) = getArgs x r xs value
|
/seL4-l4v-master/HOL4/examples/machine-code/compiler/ |
H A D | codegen_x64Lib.sml | 188 val (ys,j) = x64_encode_branch_aux forward l NONE value
|
H A D | codegen_x86Lib.sml | 195 val (ys,j) = x86_encode_branch_aux forward l NONE value
|
H A D | compilerLib.sml | 152 val ys = map prove_eq xs value 163 val (ys,def,pre) = compile_all_aux tm value 172 val (ys,_,_) = last xs value 174 val ys = map (fn (n,th) => (n,UNABBREV_CODE_RULE th)) ys value 209 val ys = map (mk_ALIGNED o snd) (xs1 @ xs2) value [all...] |
H A D | codegenLib.sml | 146 val ys = (strip_comments 0) xs value 153 val ys = map f (quote_to_strings code) value 163 val ys = map process ys value 174 val ys = list_append ys value 191 val ys = map (fn (s,v) => " " ^ s ^ implode (repeatc (m - size(s)) #" ") ^ " " ^ v ^ "\\n") xs value 323 val ys = zip (dest_tuple tm1) (dest_tuple tm2) handle e => [(tm1,tm2)] value 324 val ys = filter (fn (x,y) => x !~ y) ys value 373 val ys = list_dest pairSyntax.dest_pair tm1 value 375 val ys = foldr (uncurry append) [] (map goo zs) handle e => [] value 376 val ys = filter (fn (t1,t2) => t1 !~ t2) ys value [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/graph/ |
H A D | straightlineLib.sml | 104 val ys = map (fn (_,(th,_,_),_) => th) xs value
|
H A D | exportLib.sml | 61 val ys = map stringSyntax.fromHOLstring xs value 71 val ys = tm |> rator |> rator |> rand |> dest_string_list value 85 val ys = xs |> map pairSyntax.dest_pair value
|
H A D | file_readerLib.sml | 64 val ys = drop_until (can dest_section_declaration) xs value 70 val ys = drop_until (fn x => x = "\n" orelse x="\r\n") ys value [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/x64_compiler/ |
H A D | x64_codegen_x64Lib.sml | 189 val (ys,j) = x64_encode_branch_aux forward l NONE value
|
/seL4-l4v-master/HOL4/examples/machine-code/hoare-triple/ |
H A D | tailrecLib.sml | 23 val ys = dest_tuple lhs value
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | x86_encodeLib.sml | 136 val ys = filter (fn (x,y) => ((hd y = hd xs) handle _ => false)) instructions value [all...] |
H A D | prog_x86Lib.sml | 62 val ys = find_terml (can (match_term ``XWRITE_EFLAG a x``)) h value 66 val ys = map (fn tm => ((cdr o car) tm, cdr tm)) ys value
|
/seL4-l4v-master/HOL4/examples/bootstrap/ |
H A D | automation_lemmasScript.sml | 570 val ys = map (fst o snd) xs value
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/riscv/step/ |
H A D | riscv_stepLib.sml | 123 val (ys,zs) = flip_nth_underscore n xs value 126 val (ys,zs) = flip_nth_underscore (n-1) xs value
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | x64_encodeLib.sml | 184 val ys = filter (fn (x,y) => ((hd y = hd xs) handle _ => false)) instructions value 201 val ys = if not (hd xs = "MOVZX") then ys else let value 208 val ys = if not ((hd xs = "MOV") andalso (zsize = 64) andalso (can string_to_int (last xs))) then ys else value 221 val ys = if zsize = 8 then filter (fn (x,y) => (token_data_size (el 2 y) = 8) handle HOL_ERR _ => true) ys value 226 val ys = map (fn (x,y) => (x,map simplify_token y)) ys value [all...] |
H A D | prog_x64Lib.sml | 93 val ys = find_terml (can (match_term ``ZWRITE_MEM2 a x``)) h value 97 val ys = map (fn tm => (get_arg tm, cdr tm)) ys value 163 val ys = (map (cdr o car o cdr) xs) value 224 val ys value 317 val ys = (map (cdr o car) xs) value [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw2/ |
H A D | regAlloc.sml | 303 let val ys = List.foldl (fn (t,ls) => strip_pair t @ ls) [] xs value [all...] |
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibThm.sml | 428 val ys = List.tabulate (arity, fn i => Var ("y" ^ int_to_string i)) value 439 val ys = List.tabulate (arity, fn i => Var ("y" ^ int_to_string i)) value
|
/seL4-l4v-master/HOL4/src/unwind/ |
H A D | unwindLib.sml | 724 val (ys,A) = strip_forall Body value
|
/seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/ |
H A D | milawa_coreScript.sml | 398 val ys = map (fn x => (x,genvar(type_of x))) xs value [all...] |
/seL4-l4v-master/HOL4/examples/fun-op-sem/ml/ |
H A D | typeSoundScript.sml | 34 val ys = map #residue tms value
|