| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | Useful.sml | 489 val ps = ps @ [i] value
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Useful.sml | 489 val ps = ps @ [i] value
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
| H A D | GdiBase.sml | 215 val (ps, {x=width, ...}, cr) = loadStr v value
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
| H A D | windows_specific.cpp | 1259 PolyStringObject *ps = (PolyStringObject*)str.AsObjPtr(); local
|
| H A D | unix_specific.cpp | 2067 static int findPathVar(TaskData *taskData, PolyWord ps) argument
|
| H A D | process_env.cpp | 438 PolyStringObject * ps = (PolyStringObject *)path.AsObjPtr(); local
|
| H A D | polystring.cpp | 84 POLYUNSIGNED Poly_string_to_C(PolyWord ps, char *buff, POLYUNSIGNED bufflen) argument
95 char *Poly_string_to_C_alloc(PolyWord ps, size_t extraChars) argument
160 POLYUNSIGNED Poly_string_to_C(PolyWord ps, WCHAR *buff, POLYUNSIGNED bufflen) argument
184 WCHAR *Poly_string_to_U_alloc(PolyWord ps, size_t extraChars) argument
|
| H A D | polystring.h | 38 inline POLYUNSIGNED PolyStringLength(PolyWord ps) { return ((PolyStringObject*)ps.AsObjPtr())->length; } argument
58 TempCString(PolyWord ps): m_value(Poly_string_to_C_alloc(ps)) {} argument
95 TempString(PolyWord ps): m_value(Poly_string_to_T_alloc(ps)) {} argument
[all...] |
| H A D | pexport.cpp | 139 PolyStringObject* ps = (PolyStringObject*)p; local
679 PolyStringObject * ps = (PolyStringObject *)p; local
|
| /seL4-l4v-10.1.1/HOL4/src/postkernel/ |
| H A D | TheoryGraph.sml | 102 val ps = Theory.parents thy_s value
|
| /seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
| H A D | patternMatchesSyntax.sml | 448 val ps = pairSyntax.strip_pair pt value
491 val ps value
[all...] |
| H A D | patternMatchesLib.sml | 310 val ps = map2 (fn c => fn arg => let value
335 val ps = List.rev ((v', c_else) :: ps_rev) value
398 val ps = flatten (map process_arg ps) value
470 val ps = case case2pmatch_aux opt v t0 of value
474 val ps = if opt then case2pmatch_remove_unnessary_rows ps else ps value
2394 val ps = (snd current_col) value
3775 val ps = strip_disj (dest_neg pre) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/n-bit/ |
| H A D | bitstringLib.sml | 352 val ps = List.tabulate (i - 1, mk_p) value
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | normalForms.sml | 581 val ps = TRY_CONV TSIMP_CONV; value
|
| /seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/zc2hs/ |
| H A D | zc2hs.cpp | 274 void update(vector<int>& ps, int lit, vector<int>& r1) { argument
311 vector<int> ps; // pivots local
287 get_res(const vector<int>& resolvents, vec<Lit>& res, vector<int>& ps) argument
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
| H A D | SolverTypes.h | 89 Clause(bool learnt, const vec<Lit>& ps, ClauseId id_ = ClauseId_NULL) { argument
106 inline Clause* Clause_new(bool learnt, const vec<Lit>& ps, ClauseId id = ClauseId_NULL) { argument
|
| H A D | Solver.C | 98 const vec<Lit>& ps = learnt ? ps_ : qs; // 'ps' is now the (possibly) reduced vector of literals. variable
[all...] |
| H A D | Solver.h | 185 void addClause (const vec<Lit>& ps) { newClause(ps); } // (used to be a difference between internal and external method...) argument
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Pmatch.sml | 799 val (ps,es) = unzip pes value
|
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
| H A D | lisp_codegenScript.sml | 1605 val ps = filter (not o can dest_sep_hide) (list_dest dest_star p) value
1607 val ps = filter (fn tm => not (car tm = pc) handle HOL_ERR _ => true) ps value
1611 val ps = sorter ps value
|
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
| H A D | lisp_extractLib.sml | 379 val (ps,t) = ``(k:string |-> string list # term) ' ^name_tm`` value
443 val (ps,t) = ``(k:string |-> string list # term) ' ^name_tm`` value
491 val ps = params xs input_ty value
711 val (ps, value
874 val ps = map parts defs_inds value
889 val (ps,t) = ``(k:string |-> string list # term) ' ^name_tm`` value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/x64_compiler/ |
| H A D | x64_codegenLib.sml | 228 val ps = list_dest dest_star p value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
| H A D | helperLib.sml | 842 val ps = (list_dest dest_star o last o list_dest dest_sep_exists) p value
1147 val ps = filter (can dest_pair_one) (list_dest dest_star p) value
1156 val ps = filter (can dest_pair_one) (list_dest dest_star p) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
| H A D | straightlineLib.sml | 31 val ps = list_dest dest_star pre value
|
| H A D | stack_introLib.sml | 11 val ps = list_dest dest_star p value
|