/seL4-l4v-master/l4v/isabelle/src/Pure/Isar/ |
H A D | line_structure.scala | 19 depth: Int = 0,
|
/seL4-l4v-master/seL4/libsel4/arch_include/x86/sel4/arch/ |
H A D | bootinfo_types.h | 85 seL4_Uint8 depth; member in struct:seL4_VBEInfo30
|
/seL4-l4v-master/HOL4/examples/miller/ho_prover/ |
H A D | ho_proverTools.sml | 1201 | meson depth res 1204 else meson depth (f :: res) others 1205 | meson depth res 1211 trace "meson: (depth, state, length others)" 1212 (fn () => printVal ((depth, state, length others))) 1215 val _ = assert (depth > 0) (CUT "hit bottom") 1227 prune_subfacts_wrt (snd lit) (meson (depth - 1) [] subgoals) 1242 meson depth res (newgoals @ others) 1244 handle CUT _ => meson depth res others 1246 fn depth [all...] |
/seL4-l4v-master/HOL4/src/meson/src/ |
H A D | mesonLib.sml | 89 val depth = ref false;; (* Use depth not inference bound. *) value 413 insts=insts' andalso (size <= size' orelse !depth)) 520 fun exp_goal depth (state as ((g,_),(insts,offset,size))) cont = 521 if depth < 0 then failwith "expand_goal: too deep" 525 exp_goals (depth-1) newstate 539 exp_goals depth (gl, tup as (insts,offset,size)) cont = 542 | [g] => exp_goal depth (g,tup) (fn (g',stup) => cont([g'],stup)) 549 exp_goals depth (lgoals,(insts,offset,lsize)) 551 exp_goals depth (rgoal [all...] |
/seL4-l4v-master/HOL4/src/num/theories/ |
H A D | DecimalFractionPP.sml | 28 fun fraction {Thy,Division,fromNum} Gs backend sysp ppfns gravs depth t = let
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | term_pp_types.sml | 14 depth : int } -> Term.term -> uprinter
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | Satisfy.sig | 4 * depth-1 prolog unification for finding existential variables.
|
H A D | simpLib.sig | 147 * conversion uses a top-depth strategy for rewriting. It sets both 165 * tactic uses a top-depth strategy for rewriting, and will be recursively 208 * rule uses a top-depth strategy for rewriting.
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | ImperativeIO.sml | 170 fun prettyIn depth _ (InStream{ fStream = ref(SOME s), ...}) = 171 PolyML.prettyRepresentation(s, depth) 173 fun prettyOut depth _ (OutStream { fStream = ref(SOME s), ...}) = 174 PolyML.prettyRepresentation(s, depth)
|
H A D | Array.sml | 169 fun pretty(depth: FixedInt.int) 187 (if depth <= 0 then [PrettyString "...]"] 188 else #1 (foldri put_elem ([PrettyString "]"], depth - FixedInt.fromInt last) x) ) 315 fun pretty(depth: FixedInt.int) 333 (if depth <= 0 then [PrettyString "...]"] 334 else #1 (foldri put_elem ([PrettyString "]"], depth - FixedInt.fromInt last) x) )
|
H A D | Vector.sml | 211 fun pretty(depth: FixedInt.int) 229 (if depth <= 0 then [PrettyString "...]"] 230 else #1 (foldri put_elem ([PrettyString "]"], depth - FixedInt.fromInt last) x) ) 389 fun pretty(depth: FixedInt.int) 407 (if depth <= 0 then [PrettyString "...]"] 408 else #1 (foldri put_elem ([PrettyString "]"], depth - FixedInt.fromInt last) x) )
|
H A D | BoolArray.sml | 328 fun pretty(depth: FixedInt.int) _ (x: vector) = 344 (if depth <= 0 then [PrettyString "...]"] 345 else #1 (foldri put_elem ([PrettyString "]"], depth - FixedInt.fromInt last) x) ) 493 fun pretty(depth: FixedInt.int) _ (x: array) = 509 (if depth <= 0 then [PrettyString "...]"] 510 else #1 (foldri put_elem ([PrettyString "]"], depth - FixedInt.fromInt last) x) )
|
/seL4-l4v-master/HOL4/examples/miller/subtypes/ |
H A D | subtypeTools.sml | 187 fun set_prove_depth db depth vgoal = 188 meson_prove_reduce_depth db (set_meson_frule db) depth vgoal; 313 fun subtype_check ccache congs stricttypechecking depth = 320 ((tm, depth), fn () => basic_subtypes facts tm) 363 val pre_results = set_prove_depth facts'' depth (before_vars, goal) 373 fun SUBTYPE_CHECK stricttypechecking depth sc tm = 375 stricttypechecking depth (subtype_context_facts sc) tm; 405 fun SUBTYPE_MATCH depth sc (vars, goal) = 408 val subtypes = SUBTYPE_CHECK false depth sc elt 410 val res = set_prove_depth facts depth (var [all...] |
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | SIGNATURES.sml | 184 | displayList ([v], _, depth) dodisplay = 185 if depth <= 0 187 else [dodisplay (v, depth)] 189 | displayList (v::vs, separator, depth) dodisplay = 190 if depth <= 0 198 dodisplay (v, depth), 204 displayList (vs, separator, depth - 1) dodisplay 207 fun displaySigs (str, depth) = 208 if depth <= 0 (* elide further text. *) 220 displayList (structList, "", depth) displaySpec [all...] |
/seL4-l4v-master/isabelle/src/Pure/Thy/ |
H A D | bibtex.scala | 407 case class Delimited(quoted: Boolean, depth: Int) 443 require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0) 452 var d = delim.depth 512 if (ctxt.delim.depth > 0)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Thy/ |
H A D | bibtex.scala | 407 case class Delimited(quoted: Boolean, depth: Int) 443 require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0) 452 var d = delim.depth 512 if (ctxt.delim.depth > 0)
|
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | patriciaLib.sig | 25 val depth : term_ptree -> int value
|
/seL4-l4v-master/HOL4/src/num/reduce/src/ |
H A D | reduceLib.sml | 29 (* REDUCE_CONV - Perform above reductions at any depth. *)
|
/seL4-l4v-master/HOL4/src/monad/ |
H A D | parmonadsyntax.sml | 167 fun print_monads (tyg, tmg) backend sysprinter ppfns (p,l,r) depth t = let 179 sysprinter {gravs = gravs, depth = depth - 1, binderp = bp} t
|
H A D | monadsyntax.sml | 277 fun print_monads (tyg, tmg) backend sysprinter ppfns (p,l,r) depth t = let 286 sysprinter {gravs = gravs, binderp = bp, depth = depth - 1} t
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | Holmake_types.sml | 32 fun recurse (count, depth, ss) = 38 if depth = 0 then (count, slice(ss, 1, NONE)) 39 else recurse (count + 1, depth - 1, ss') 41 recurse (count + 1, depth + 1, ss') 42 else recurse (count + 1, depth, ss')
|
/seL4-l4v-master/HOL4/src/transfer/ |
H A D | transferLib.sml | 472 fun search_for P depth sq = 478 if i > depth then default 526 fun transfer_tm depth cleftp ruledb t = 527 base_transfer cleftp ruledb t |> search_for is_eq depth 529 fun transfer_thm depth cleftp ruledb th = 535 |> search_for goodconcl depth
|
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfoot_pp_print.sml | 74 fun sys gravs d' = sys_raw {gravs = gravs, depth = d', binderp = false} 118 fun sys gravs d' = sys_raw {gravs = gravs, depth = d', binderp = false} 597 fun sys gravs d' = sys_raw {gravs = gravs, depth = d', binderp = false} 624 fun sys gravs d' = sys_raw {gravs = gravs, depth = d', binderp = false} 721 fun sys gravs d' = sys_raw {gravs = gravs, depth = d', binderp = false} 1030 fun sys gravs d' = sys_raw {gravs = gravs, depth = d', binderp = false} 1191 fun sys gravs d' = sys_raw {gravs = gravs, depth = d', binderp = false} 1265 fun sys gravs d' = sys_raw {gravs = gravs, depth = d', binderp = false}
|
/seL4-l4v-master/seL4/manual/parts/ |
H A D | cspace.tex | 235 additional layer of depth though \emph{badging}. 403 translated, called the \emph{depth limit}. 452 the depth limit, which is the maximum number of bits to be 455 with a depth limit of 12 bits. 460 0x00F00000 with a depth limit of 24 bits. Note that the addresses of 461 the L2 and L3 CNode Caps are the same, but that their depth limits 467 user must also supply a depth limit. To specify a range of capability
|
/seL4-l4v-master/HOL4/src/pfl/examples/ |
H A D | tree.sml | 95 (* Measure on recursion depth. *)
|