Searched refs:str (Results 251 - 275 of 332) sorted by relevance

<<11121314

/seL4-l4v-10.1.1/graph-refine/
H A Dsearch.py465 if type (s) == str:
587 if type (p) != str]
1153 trace ('Testing guess for pair: %s' % str (pair))
1219 if str (it[1][1]) == 'InductFailed']
1693 return str (n)
1722 printout ("Decided to case split at %s" % str (details))
1727 printout ('Found a future induction at %s' % str (details[0]))
H A Dstack_logic.py146 trace (str (vs))
147 trace (str (hyps))
224 trace (str ([hyp] + hyps))
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/zc2hs/
H A Dzc2hs.cpp205 iss.str(line);
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A DextendTranslateScript.sml1393 val STRING_STRCAT = prove(``str (STRCAT s1 s2) = acl2_strcat (str s1) (str s2)``,
1408 val STRING_PREFIX = prove(``bool (isPREFIX s1 s2) = ite (not (less (length (str s2)) (length (str s1))))
1409 (equal (coerce (str s1) (sym "COMMON-LISP" "LIST")) (acl2_take (length (str s1)) (coerce (str s2) (sym "COMMON-LISP" "LIST")))) nil``,
H A Dacl2encodeLib.sml218 {const = ``str``,definition = combinTheory.I_THM, induction = NONE};
242 (simple_encode_map_encode ``str``)
254 ("str ?", op&&& o (equal ``str`` ## stringSyntax.is_string_literal) o dest_comb);
H A Dsexp.sml272 (* `(stringp(str x) = t) /\ (stringp _ = nil)`; *)
1202 ("(str " ^ "\"" ^ s ^ "\")")
1221 ("(str " ^ "\"" ^ s ^ "\")")
1242 ``str ^(abbrevMLstring s)``
1264 | mlsexp_to_string (mlstr s) = ("(str " ^ "\"" ^ s ^ "\")")
1349 | mlsexp_to_term (mlstr s) = ``str ^(abbrevMLstring s)``
/seL4-l4v-10.1.1/l4v/misc/regression/
H A Drun_tests.py335 return ("Exception launching timeout_output: %s" % str(e))
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/decompiler/
H A Darm_decomp_demoScript.sml155 e52d4004 (* push {r4} ; (str *)
/seL4-l4v-10.1.1/HOL4/src/parse/
H A Dparse_type.sml195 "'" ^ str (Char.chr (i - 0x3B1 + Char.ord #"a"))
/seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/
H A Dlisp_gcScript.sml53 E4835004 (* L2:str r5,[r3],#4 *)
54 E4836004 (* str r6,[r3],#4 *)`;
68 E4895004 (* str r5,[r9],#4 *)
80 E509501C (* str r5,[r9,#-28] *)
83 E5895004 (* str r5,[r9,#4] *)
104 E5893000 (* str r3,[r9] *)`;
113 E5093018 (* str r3,[r9,#-24] *)
114 E5094014 (* str r4,[r9,#-20] *)
115 E5095010 (* str r5,[r9,#-16] *)
116 E509600C (* str r
[all...]
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DPrint.sml49 val escapeMap = List.map (fn c => (c, "\\" ^ str c)) escape
59 | NONE => str c
117 fun charWord c = mkWord (str c);
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DPrint.sml49 val escapeMap = List.map (fn c => (c, "\\" ^ str c)) escape
59 | NONE => str c
117 fun charWord c = mkWord (str c);
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/correctness/
H A DcorrectScript.sml392 ~(ic = mla_mul) /\ ~(ic = ldr) /\ ~(ic = str) /\ ~(ic = ldm) /\
960 val _ = print "*\nVerifying: swp, ldr, str\n*\n"; (*=========================*)
965 (DECODE_INST ireg IN {swp; ldr; str}) /\ (aregn2 = 2w) /\
1927 \\ Cases_on `DECODE_INST ireg IN {swp; ldr; str}`
2004 DECODE_INST ireg IN {swp; ldr; str} \/
2066 DECODE_INST ireg IN {swp; ldr; str} \/
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/
H A Dsexp.sml297 (* `(stringp(str x) = t) /\ (stringp _ = nil)`; *)
1276 ("(str " ^ "\"" ^ s ^ "\")")
1295 ("(str " ^ "\"" ^ s ^ "\")")
1316 ``str ^(abbrevMLstring s)``
1338 | mlsexp_to_string (mlstr s) = ("(str " ^ "\"" ^ s ^ "\")")
1423 | mlsexp_to_term (mlstr s) = ``str ^(abbrevMLstring s)``
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/
H A Dsexp.sml272 (* `(stringp(str x) = t) /\ (stringp _ = nil)`; *)
1202 ("(str " ^ "\"" ^ s ^ "\")")
1221 ("(str " ^ "\"" ^ s ^ "\")")
1242 ``str ^(abbrevMLstring s)``
1264 | mlsexp_to_string (mlstr s) = ("(str " ^ "\"" ^ s ^ "\")")
1349 | mlsexp_to_term (mlstr s) = ``str ^(abbrevMLstring s)``
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DTYPECHECK_PARSETREE.sml900 SOME str => SOME(str, location)
910 fun copyEntries (str as Struct{locations, signat = sigTbl, name=strName, ...}, varLoc) =
935 List.map (fn c => mkSelectedVar (c, str, openLocs)) valConstrs)
944 makeSelectedStruct (strVal, str, openLocs);
953 mkSelectedVar (value, str, openLocs);
/seL4-l4v-10.1.1/HOL4/src/1/
H A DPrim_rec.sml412 fun pass str =
413 if (mem str (!slist))
416 else (slist := str :: !slist; str)
/seL4-l4v-10.1.1/HOL4/src/emit/
H A Dextended_emitScript.sml365 \ (String.^(String.str (Char.chr 1), s))"
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibUseful.sml597 val pp_char = pp_map str pp_string;
/seL4-l4v-10.1.1/HOL4/tools/Holmake/poly/
H A DProcessMultiplexor.sml401 (fn (c, (cs, n)) => ((str (chr n), (c, Waiting))::cs, n + 1))
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_symbolsScript.sml415 null_term_str a df f str =
416 ?p. (one_string a (str ++ [CHR 0]) * p) (fun2set (f,df)) /\
417 EVERY (\x. ~(x = CHR 0)) str`;
420 exists_null_term_str a df f = ?str. null_term_str a df f str`;
423 mem2string a df f = @str. null_term_str a df f str`;
3047 \\ `(str = []) \/ ?x l. str = SNOC x l` by METIS_TAC [rich_listTheory.SNOC_CASES]
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/parse/
H A Dlisp_parseScript.sml1257 \\ `?str ps. sexp2abbrevt_aux exp T abbrevs {} = (str,ps)` by METIS_TAC [PAIR]
1271 string2sexp str = (sexp_parse (FST (sexp_lex str)))`;
/seL4-l4v-10.1.1/HOL4/Manual/Tools/
H A Dpolyscripter.sml208 fun addIndent ws = String.translate(fn #"\n" => "\n"^ws | c => str c)
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/
H A DlemmasScript.sml323 `!i. (DECODE_INST i = str) ==> ~(i %% 20)`,
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/
H A DannotatedIR.sml70 (itlist (curry (fn (stm,str) => "; " ^ formatInst stm ^ str)) (tl stmL) "") ^ "]"))

Completed in 405 milliseconds

<<11121314