/seL4-l4v-master/l4v/isabelle/src/Pure/PIDE/ |
H A D | rendering.scala | 422 case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) => 424 depth % 4 match {
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | muSyntax.sml | 440 (* returns maximum quantifier depth *) 505 (* return the alternation depth of the given formula *) 522 (* return the max same-quantifier nesting depth of the given formula *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | TYPECHECK_PARSETREE.sml | 305 fun assignSeq(env, depth, l, isExp) = 310 val expT = assignValues(level, depth, env, v, h) 385 fun printList (doPrint: 'a*FixedInt.int->pretty) (c: 'a list, separator, depth): pretty list = 386 if depth <= 0 then [PrettyString "..."] 390 | [v] => [doPrint (v, depth)] 394 doPrint (v, depth), 401 printList doPrint (vs, separator, depth - 1)
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | xwindows.cpp | 2224 unsigned depth, 2236 borderWidth,depth,clas,visual,0,0); 2512 PolyWord depth; /* ML int */ member in struct:__anon18 2534 if (image->format == XYPixmap) dsize = dsize * image->depth; 2547 unsigned depth = get_C_ulong(taskData, I->depth); local 2571 image.depth = depth; 2595 X->depth = DEREFWORD(Make_arbitrary_precision(taskData, image->depth)); 2215 CreateWindow( TaskData *taskData, Handle parent, int x, int y, unsigned w, unsigned h, unsigned borderWidth, unsigned depth, unsigned clas, Visual *visual, Handle handler, Handle state ) argument 4015 unsigned width,height,borderWidth,depth; local [all...] |
H A D | savestate.cpp | 121 POLYEXTERNALSYMBOL POLYUNSIGNED PolySaveState(FirstArgument threadId, PolyWord fileName, PolyWord depth); 759 POLYUNSIGNED PolySaveState(FirstArgument threadId, PolyWord fileName, PolyWord depth) argument 768 // The value of depth is zero for top-level save so we need to add one for hierarchy. 769 unsigned newHierarchy = get_C_unsigned(taskData, depth) + 1;
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | functionEncodeLib.sml | 1165 fun perform_rewrite depth RR term rewrite = 1167 val (hyp_set,_) = (map (map (backchain_rewrite (depth + 1) RR)) ## I) 1178 (apply_rewrite depth RR p))) THENC 1187 and apply_rewrite depth RR conj = 1192 (backchain_rewrite (depth + 1) 1200 UNBOOL_RULE (tryfind_e Empty (backchain_rewrite (depth + 1) RR) 1207 and backchain_rewrite depth RR term = 1208 let val _ = trace 3 ("#" ^ int_to_string depth) 1209 val _ = if depth > !max_depth then raise Empty else () 1218 (backchain_rewrite depth [all...] |
H A D | tutorial.ml | 236 (* indicates the depth of search at each node, and whether the term given *) 635 (* depth-first order, as follows: *)
|
/seL4-l4v-master/seL4/src/arch/arm/32/kernel/ |
H A D | vspace.c | 2569 word_t index, depth; local 2592 depth = getSyscallArg(1, buffer); 2627 lu_ret = lookupTargetSlot(root, index, depth);
|
/seL4-l4v-master/seL4/src/arch/arm/64/kernel/ |
H A D | vspace.c | 2297 word_t index, depth; local 2319 depth = getSyscallArg(1, buffer); 2351 lu_ret = lookupTargetSlot(root, index, depth);
|
/seL4-l4v-master/HOL4/examples/fsub/ |
H A D | full_subtypingScript.sml | 62 (* define algorithmic sub-typing, with a depth of derivation parameter *)
|
/seL4-l4v-master/HOL4/src/proofman/ |
H A D | goalStack.sml | 85 fun depth(GSTK{stack,...}) = length stack; function
|
/seL4-l4v-master/HOL4/src/pattern_matches/ |
H A D | patternMatchesSyntax.sml | 795 fn gravs => fn d => sys {gravs = gravs, depth = d, binderp = true} 797 fn gravs => fn d => sys {gravs = gravs, depth = d, binderp = false}
|
/seL4-l4v-master/HOL4/src/probability/ |
H A D | hurdUtils.sml | 1221 fun ASM_MATCH_MP_TAC_N depth ths = 1223 (EVERY o map ASSUME_TAC o rev o MATCH_MP_DEPTH depth ths)
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | BasicStreamIO.sml | 749 fun prettyIn depth a (Committed { rest, ...}) = 750 prettyIn depth a rest
|
/seL4-l4v-master/HOL4/examples/decidable_separationLogic/doc/ |
H A D | presentation-content.tex | 479 \item trees are introduced considering their maximal depth
|
/seL4-l4v-master/HOL4/src/HolQbf/ |
H A D | QbfCertificate.sml | 400 (* depth-first recursion over the certificate (which represents a DAG),
|
/seL4-l4v-master/HOL4/src/pfl/ |
H A D | index.sml | 426 (* depth added results in this turning into two equations *)
|
/seL4-l4v-master/HOL4/examples/ARM/v4/ |
H A D | arm_evalLib.sml | 801 depth = d - 1, binderp = false})
|
/seL4-l4v-master/HOL4/src/TeX/ |
H A D | mungeTools.sml | 116 else if String.isPrefix "depth=" s then let
|
/seL4-l4v-master/HOL4/src/coalgebras/ |
H A D | ltreeScript.sml | 8 Note that this tree data structure allows for both infinite depth
|
/seL4-l4v-master/HOL4/src/quantHeuristics/ |
H A D | quantHeuristicsLibBase.sml | 2485 (* The main function with an explicit recursion depth argument, and a list of already visited arguments. The arguments are: 2487 n - recurion depth 2504 ((say_HOL_WARNING "BOUNDED_QUANT_INSTANTIATE_HEURISTIC___COMBINE" "Maximal recursion depth reached!");
|
/seL4-l4v-master/isabelle/src/Doc/Intro/document/ |
H A D | advanced.tex | 1162 \index{search!depth-first} 1221 Since Prolog uses depth-first search, this tactic is a (slow!)
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Intro/document/ |
H A D | advanced.tex | 1162 \index{search!depth-first} 1221 Since Prolog uses depth-first search, this tactic is a (slow!)
|
/seL4-l4v-master/HOL4/src/string/Manual/ |
H A D | description.tex | 391 \ml{ASCII\_{11}}\index{ASCII\_11@{\ptt ASCII\_11}}. The depth conversion
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | Holmake.sml | 273 performing a post-order depth-first traversal.)
|