/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.call/ |
H A D | return_ll.c | 9 static long long return_ll(long long ll) argument 11 return ll; 20 long long ll; local 23 values[0] = ≪ 29 for (ll = 0LL; ll < 100LL; ll++) 32 CHECK(rlonglong == ll); 35 for (ll = 55555555555000LL; ll < 5555555555510 [all...] |
H A D | huge_struct.c | 54 int8_t ll; member in struct:BigStruct 151 retVal.kk, retVal.ll, retVal.mm, retVal.nn, retVal.oo, retVal.pp, 310 retVal.kk, retVal.ll, retVal.mm, retVal.nn, retVal.oo, retVal.pp, 338 retVal.kk, retVal.ll, retVal.mm, retVal.nn, retVal.oo, retVal.pp,
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/examples/queen/ |
H A D | queen.cxx | 56 int ll = k-i+j; local 57 if (ll>=0 && ll<N) 59 c &= X[i][j] >> !X[k][ll]; 65 int ll = i+j-k; local 66 if (ll>=0 && ll<N) 68 d &= X[i][j] >> !X[k][ll];
|
/seL4-l4v-10.1.1/HOL4/src/coalgebras/ |
H A D | llistScript.sml | 123 val LTL_HD_def = zDefine `LTL_HD ll = case llist_rep ll 0 of NONE => NONE 124 | SOME h => SOME (llist_abs (llist_rep ll o SUC), h)` ; 137 val LHD = new_definition("LHD", ``LHD ll = llist_rep ll 0``); 140 ``LTL ll = case LHD ll of 142 | SOME _ => SOME (llist_abs (\n. llist_rep ll (n + 1)))`` 146 `LHD ll = OPTION_MAP SND (LTL_HD ll)`, [all...] |
/seL4-l4v-10.1.1/HOL4/src/compute/examples/ |
H A D | Sort.sml | 47 fun double l () = let val ll = l() in ll@ll end; value 48 fun triple l () = let val ll = l() in ll@(ll@ll) end; value
|
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/lprefix_lub/ |
H A D | lprefix_lubScript.sml | 49 `IS_SOME (LTAKE n ll) ��� LLENGTH ll = SOME n ��� less_opt n (LLENGTH ll)`, 94 `!ll n x. LNTH n ll = SOME x ��� less_opt n (LLENGTH ll)`, 97 `ll = [||] ��� ?h t. ll = h:::t` by metis_tac [llist_CASES] >> 274 (!ll. ll ��� l [all...] |
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/ |
H A D | utils.sml | 222 of TREE(lk,RED,ll,lr) => 223 TREE(k,RED,TREE(lk,BLACK,ll,lr), 229 of TREE(lk,RED,ll,lr) => 230 TREE(k,RED,TREE(lk,BLACK,ll,lr), 236 of l as TREE(lk,RED,ll, lr as TREE(lrk,RED,lrl,lrr)) => 239 TREE(k,RED,TREE(lk,BLACK,ll,lr), 241 | _ => TREE(lrk,BLACK,TREE(lk,RED,ll,lrl), 243 | l as TREE(lk,RED, ll as TREE(llk,RED,lll,llr), lr) => 246 TREE(k,RED,TREE(lk,BLACK,ll,lr), 248 | _ => TREE(lk,BLACK,ll,TRE [all...] |
/seL4-l4v-10.1.1/HOL4/src/emit/ |
H A D | extended_emitScript.sml | 240 ``LHD ll = llcases NONE (\(h,t). SOME h) ll``, 241 Q.ISPEC_THEN `ll` STRUCT_CASES_TAC llist_CASES THEN 245 ``LTL ll = llcases NONE (\(h,t). SOME t) ll``, 246 Q.ISPEC_THEN `ll` STRUCT_CASES_TAC llist_CASES THEN 250 ``!ll. LTAKE n ll = 252 else case LHD ll of 255 (LTAKE (n - 1) (THE (LTL ll)))``, [all...] |
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
H A D | tttTermData.sml | 101 val ll = rpt_split_sl "," body value 103 if ll = [[]] then ([],cont) else (ll, cont) 110 let val (ll,cont) = read_list l in value 111 (List.concat ll, cont)
|
H A D | tttTacticData.sml | 144 val ll = rpt_split_sl "," body value 146 if ll = [[]] then ([],cont) else (ll, cont) 153 let val (ll,cont) = read_list l in value 154 (List.concat ll, cont)
|
/seL4-l4v-10.1.1/HOL4/Manual/Quick/ |
H A D | quick.tex | 26 \begin{tabular}{ll} 37 \begin{tabular}{ll} 51 \begin{tabular}{ll} 67 \begin{tabular}{ll} 80 \begin{tabular}{ll} 95 \begin{tabular}{ll} 112 \begin{tabular}{ll} 126 \begin{tabular}{ll} 144 \begin{tabular}{ll} 155 \noindent\begin{tabular}{ll} [all...] |
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/examples/ |
H A D | alu.sml | 76 val ll = (i2b r); value 77 val ll = ll@List.tabulate(l - (List.length ll),(fn x => 0)); value 78 in if (List.nth(ll,b)=0) then F else T handle Subscript => F end; 83 val ll = (i2b r); value 84 val ll = ll@List.tabulate(l - (List.length ll),(fn x => 0)); value 85 in if (List.nth(ll, [all...] |
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
H A D | run_arm_evalScript.sml | 75 val ll = length l value 77 if n < ll then 80 l @ List.tabulate(n - ll, fn _ => "0x0")
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | load_sexp.ml | 89 val ll = load_book "summary"; 107 val ll_simp = map (map (I ## SIMP_RULE list_ss g_simps)) ll;
|
/seL4-l4v-10.1.1/HOL4/examples/PSL/path/ |
H A D | FinitePSLPathScript.sml | 78 Define `(CONCAT [] = []) /\ (CONCAT(l::ll) = l <> CONCAT ll)`; 244 ``!P. ALL_EL (\l. (LENGTH l = 1) /\ P(EL(LENGTH l - 1)l)) ll 245 ==> ALL_EL P (CONCAT ll)``, 246 Induct_on `ll` 254 ``!ll. CONCAT (MAP (\l. [l]) ll) = ll``, 261 ``!ll n. n < LENGTH ll [all...] |
/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | Table.sml | 332 Branch2 (ll, lp, lr) => 333 (true, Branch3 (ll, lp, lr, if_eq ord p' p, r')) 334 | Branch3 (ll, lp, lm, lq, lr) => (false, Branch2 335 (Branch2 (ll, lp, lm), lq, Branch2 (lr, if_eq ord p' p, r'))) 354 (Branch2 (ll, lp, lr), Branch2 _) => 355 Branch2 (Branch3 (ll, lp, lr, if_eq ord p' p, m'), q, r) 356 | (Branch3 (ll, lp, lm, lq, lr), _) => 357 Branch3 (Branch2 (ll, lp, lm), lq, 372 | (Branch3 (ll, lp, lm, lq, lr), Branch2 (ml, mp, mr)) => 373 Branch3 (Branch2 (ll, l [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/powerpc/ |
H A D | ffi_sysv.c | 359 long long *ll; member in union:__anon48 400 long long **ll; member in union:__anon49 552 *next_arg.ll = **p_argv.ll; 567 *gpr_base.ll++ = **p_argv.ll;
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/ |
H A D | x64AssemblerLib.sml | 213 fun printFormatted (f, c, p) ll = 223 val ll = List.map (update_m o f) ll value 234 end) ll
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | envTools.sml | 42 else let val (_,ll) = strip_comb e 43 in if (Term.compare(q,List.nth(ll,1))=EQUAL) then List.nth(ll,2) else get_env_val_aux empty_env q (List.nth(ll,0)) end
|
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/official-semantics/ |
H A D | KripkeScript.sml | 82 * A useful special case (possibly the only one we'll need) is to identify
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/xtensa/ |
H A D | ffi.c | 111 long long **ll; member in union:__anon52 158 *(unsigned long long*)addr = **p_argv.ll;
|
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/parser/ |
H A D | ParserTools.sml | 338 let val ll = parsePath p value 340 val nl = List.tabulate(length ll + 1,I) 343 (fn n => if rhs(concl(EVAL(pathflToTerm(List.drop(ll,n),fm)))) = ``F`` 378 let val ll = parsePath p value 383 (map_interval (fn w => rhs(concl(EVAL(pathsereToTerm(w,se))))) ll)
|
/seL4-l4v-10.1.1/HOL4/src/refute/ |
H A D | Canon.sml | 179 let val (ll,r) = dest_comb tm value 180 in let val s = name_of_const ll 187 in AP_TERM ll (ABS v (NNF_CONV_P emb bvs bod)) 191 in AP_TERM ll (ABS v (NNF_CONV_P true (v::bvs) bod)) 196 let val (oper,l) = dest_comb ll 225 let val (ll,r) = dest_comb tm value 226 in let val s = name_of_const ll 236 let val (oper,l) = dest_comb ll
|
/seL4-l4v-10.1.1/HOL4/src/new-datatype/ |
H A D | Witness.sml | 118 val llrecycle = prove(``!x. ?ll. ll = x:::ll``,
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | TheoryReader.sml | 54 val ll = rpt_split_sl "," body value 56 if ll = [[]] 58 else (ll, cont)
|