/seL4-l4v-master/HOL4/src/prekernel/ |
H A D | Globals.sml | 79 * Controls depth of printing for terms. Since the pp recursively decrements *
|
/seL4-l4v-master/HOL4/src/n-bit/ |
H A D | wordspp.sml | 113 fun sys g d t = syspr {gravs = g, depth = d, binderp = false} t
|
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/ |
H A D | jedit_rendering.scala | 403 case (depth, _) => Some(depth + 1)
|
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | jedit_rendering.scala | 403 case (depth, _) => Some(depth + 1)
|
/seL4-l4v-master/HOL4/examples/fsub/ |
H A D | kernel_subtypingScript.sml | 80 (* define algorithmic sub-typing, with a depth of derivation parameter *) 125 (* set up syntax for algorithmic sub-typing relation without the depth
|
/seL4-l4v-master/HOL4/src/quantHeuristics/ |
H A D | quantHeuristicsLibBase.sig | 252 "QUANT_INST___REC_DEPTH" can set the maximal recursion depth, default is 250. 253 If the search is aborted, because the depth is not big enough, a warning
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | problems.sml | 466 "works at depth 45! [JRH]", 467 "Confirmed (depth=45, inferences=263702, time=148s), though if", 468 "lemmaizing is used then a lemma is discovered at depth 29 that allows", 469 "a much quicker proof (depth=30, inferences=10039, time=5.5s)."], 525 "- With lemmaizing: (depth=18, inferences=15632, time=21s)", 526 "- Without: gave up waiting after (depth=25, inferences=2125072, ...)"],
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | problems.sml | 466 "works at depth 45! [JRH]", 467 "Confirmed (depth=45, inferences=263702, time=148s), though if", 468 "lemmaizing is used then a lemma is discovered at depth 29 that allows", 469 "a much quicker proof (depth=30, inferences=10039, time=5.5s)."], 525 "- With lemmaizing: (depth=18, inferences=15632, time=21s)", 526 "- Without: gave up waiting after (depth=25, inferences=2125072, ...)"],
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | FinalPolyML.sml | 115 fun prettyProps depth _ l = 116 if depth <= 0 then PrettyString "..." 117 else prettyProp(l, depth-1) 208 (* This controls the depth of printing if the default CPResultFun is used. It 210 be called to get the print depth whenever that code is executed. 216 (* Controls the depth of context to produce in error messages. 332 stream: string->unit, depth: int) 380 prettyPrintWithOptionalMarkup (stream, !lineLength) (TypeConstrs.print(t, FixedInt.fromInt depth, SOME space)) 383 prettyPrintWithOptionalMarkup (stream, !lineLength) (Signatures.print(s, FixedInt.fromInt depth, SOME space)) 386 prettyPrintWithOptionalMarkup (stream, !lineLength) (Structures.print(s, FixedInt.fromInt depth, SOM [all...] |
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | MATCH_COMPILER.sml | 614 (* Find the "depth" of pattern i.e. the position of 616 tuple find the maximum depth of its fields, since 629 (* No default - the depth is the number of 643 fun findDeepest(column, bestcol, depth) = 651 if thisDepth > depth 653 else findDeepest (column + 1, bestcol, depth) 655 else findDeepest (column + 1, bestcol, depth)
|
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | patriciaLib.sml | 156 fun depth Empty = 0 function 157 | depth (Leaf (j, d)) = 1 158 | depth (Branch (p, m, l, r)) = 1 + (Int.max (depth l, depth r))
|
H A D | sptreeSyntax.sml | 216 fun sys gs d = syspr {gravs = gs, depth = d, binderp = false}
|
/seL4-l4v-master/seL4/src/arch/riscv/kernel/ |
H A D | vspace.c | 944 word_t depth; local 966 depth = getSyscallArg(1, buffer); 999 lu_ret = lookupTargetSlot(root, index, depth);
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | TYPEIDCODE.sml | 99 (* Generate code to check that the depth is not less than the allowedDepth 106 (* Subtract one from the current depth to produce the depth for sub-elements. *) 510 the reference and apply it the pair of the value and the depth. *) 518 base printer functions and then to the pair of the value and depth. *) 580 | asRecord(({name, typeof, ...}, offset) :: fields, depth) = 586 checkDepth(depthCode, depth, 596 asRecord(fields, depth+1)),
|
/seL4-l4v-master/HOL4/src/pfl/examples/ |
H A D | zero.sml | 47 (* Measure on recursion depth. *)
|
/seL4-l4v-master/isabelle/src/Doc/Logics/document/ |
H A D | LK.tex | 615 frequently fails to terminate. It is generally unsuitable for depth-first 664 The method is inherently depth-first. 677 applies {\tt repeat_goal_tac} using depth-first search to solve subgoal~$i$. 701 applies {\tt step_tac} using depth-first search to solve subgoal~$i$.
|
/seL4-l4v-master/isabelle/src/HOL/Bali/document/ |
H A D | root.tex | 164 for the maximal recursive depth. The semantics is not altered. The annotation
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics/document/ |
H A D | LK.tex | 615 frequently fails to terminate. It is generally unsuitable for depth-first 664 The method is inherently depth-first. 677 applies {\tt repeat_goal_tac} using depth-first search to solve subgoal~$i$. 701 applies {\tt step_tac} using depth-first search to solve subgoal~$i$.
|
/seL4-l4v-master/l4v/isabelle/src/HOL/Bali/document/ |
H A D | root.tex | 164 for the maximal recursive depth. The semantics is not altered. The annotation
|
/seL4-l4v-master/isabelle/src/Pure/PIDE/ |
H A D | headless.scala | 270 val depth = dep_graph.node_depth(Load_State.count_file) 271 maximals.sortBy(node => - depth(node))
|
H A D | rendering.scala | 422 case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) => 424 depth % 4 match {
|
/seL4-l4v-master/l4v/isabelle/src/Pure/PIDE/ |
H A D | headless.scala | 270 val depth = dep_graph.node_depth(Load_State.count_file) 271 maximals.sortBy(node => - depth(node))
|
/seL4-l4v-master/seL4/src/arch/x86/kernel/ |
H A D | vspace.c | 1269 word_t depth; local 1291 depth = getSyscallArg(1, buffer); 1325 lu_ret = lookupTargetSlot(root, index, depth);
|
/seL4-l4v-master/HOL4/src/lite/ |
H A D | liteLib.sml | 317 (* Faster depth conversions using failure rather than returning a REFL. *)
|
/seL4-l4v-master/HOL4/src/num/arith/Manual/ |
H A D | description.tex | 197 deep\index{depth conversion} within the goal:
|