Searched refs:depth (Results 76 - 100 of 147) sorted by relevance

123456

/seL4-l4v-master/HOL4/src/prekernel/
H A DGlobals.sml79 * Controls depth of printing for terms. Since the pp recursively decrements *
/seL4-l4v-master/HOL4/src/n-bit/
H A Dwordspp.sml113 fun sys g d t = syspr {gravs = g, depth = d, binderp = false} t
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/
H A Djedit_rendering.scala403 case (depth, _) => Some(depth + 1)
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/
H A Djedit_rendering.scala403 case (depth, _) => Some(depth + 1)
/seL4-l4v-master/HOL4/examples/fsub/
H A Dkernel_subtypingScript.sml80 (* 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 DquantHeuristicsLibBase.sig252 "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 Dproblems.sml466 "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 Dproblems.sml466 "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 DFinalPolyML.sml115 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 DMATCH_COMPILER.sml614 (* 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 DpatriciaLib.sml156 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 DsptreeSyntax.sml216 fun sys gs d = syspr {gravs = gs, depth = d, binderp = false}
/seL4-l4v-master/seL4/src/arch/riscv/kernel/
H A Dvspace.c944 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 DTYPEIDCODE.sml99 (* 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 Dzero.sml47 (* Measure on recursion depth. *)
/seL4-l4v-master/isabelle/src/Doc/Logics/document/
H A DLK.tex615 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 Droot.tex164 for the maximal recursive depth. The semantics is not altered. The annotation
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics/document/
H A DLK.tex615 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 Droot.tex164 for the maximal recursive depth. The semantics is not altered. The annotation
/seL4-l4v-master/isabelle/src/Pure/PIDE/
H A Dheadless.scala270 val depth = dep_graph.node_depth(Load_State.count_file)
271 maximals.sortBy(node => - depth(node))
H A Drendering.scala422 case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) =>
424 depth % 4 match {
/seL4-l4v-master/l4v/isabelle/src/Pure/PIDE/
H A Dheadless.scala270 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 Dvspace.c1269 word_t depth; local
1291 depth = getSyscallArg(1, buffer);
1325 lu_ret = lookupTargetSlot(root, index, depth);
/seL4-l4v-master/HOL4/src/lite/
H A DliteLib.sml317 (* Faster depth conversions using failure rather than returning a REFL. *)
/seL4-l4v-master/HOL4/src/num/arith/Manual/
H A Ddescription.tex197 deep\index{depth conversion} within the goal:

Completed in 285 milliseconds

123456