Searched defs:ys (Results 1 - 25 of 44) sorted by relevance

12

/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DSharing.sml49 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 DOptions.sml226 val (ys,xs) = getArgs x r xs value
H A DRule.sml447 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 DSharing.sml49 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 DOptions.sml226 val (ys,xs) = getArgs x r xs value
/seL4-l4v-master/HOL4/examples/machine-code/compiler/
H A Dcodegen_x64Lib.sml188 val (ys,j) = x64_encode_branch_aux forward l NONE value
H A Dcodegen_x86Lib.sml195 val (ys,j) = x86_encode_branch_aux forward l NONE value
H A DcompilerLib.sml152 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 DcodegenLib.sml146 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 DstraightlineLib.sml104 val ys = map (fn (_,(th,_,_),_) => th) xs value
H A DexportLib.sml61 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 Dfile_readerLib.sml64 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 Dx64_codegen_x64Lib.sml189 val (ys,j) = x64_encode_branch_aux forward l NONE value
/seL4-l4v-master/HOL4/examples/machine-code/hoare-triple/
H A DtailrecLib.sml23 val ys = dest_tuple lhs value
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86/
H A Dx86_encodeLib.sml136 val ys = filter (fn (x,y) => ((hd y = hd xs) handle _ => false)) instructions value
[all...]
H A Dprog_x86Lib.sml62 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 Dautomation_lemmasScript.sml570 val ys = map (fst o snd) xs value
/seL4-l4v-master/HOL4/examples/l3-machine-code/riscv/step/
H A Driscv_stepLib.sml123 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 Dx64_encodeLib.sml184 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 Dprog_x64Lib.sml93 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 DregAlloc.sml303 let val ys = List.foldl (fn (t,ls) => strip_pair t @ ls) [] xs value
[all...]
/seL4-l4v-master/HOL4/src/metis/
H A DmlibThm.sml428 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 DunwindLib.sml724 val (ys,A) = strip_forall Body value
/seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/
H A Dmilawa_coreScript.sml398 val ys = map (fn x => (x,genvar(type_of x))) xs value
[all...]
/seL4-l4v-master/HOL4/examples/fun-op-sem/ml/
H A DtypeSoundScript.sml34 val ys = map #residue tms value

Completed in 288 milliseconds

12