/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Heap.h | 36 vec<int> indices; // int -> index in heap member in class:Heap 43 indices[heap[i]] = i; 47 indices[x] = i; 57 indices[heap[i]] = i; 61 indices[x] = i; 64 bool ok(int n) { return n >= 0 && n < (int)indices.size(); } 69 void setBounds (int size) { assert(size >= 0); indices.growTo(size,0); } 70 bool inHeap (int n) { assert(ok(n)); return indices[n] != 0; } 71 void increase (int n) { assert(ok(n)); assert(inHeap(n)); percolateUp(indices[n]); } 76 indices[ [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | patternMatch.sml | 16 (* and a set of pattern indices representing the patterns that were still possibly *) 166 (* rule indices which label each successor of that test. Given a set of possible tests *) 167 (* tset and a set of live rule indices rset, the relevance heuristic searches for the *) 178 val indices = next_indices (test_set, rules) value 180 if null indices then 184 val test = hd indices 216 fun select_index(test_set, indices) = 217 if length indices = 1 then 218 hd indices 230 (0, length test_list) indices [all...] |
/seL4-l4v-10.1.1/HOL4/examples/computability/lambda/ |
H A D | recsetsScript.sml | 120 to mean there exists a function that returns values at successive indices. 536 val indices_def = Define`indices P = { i | P (Phi i) }` 540 ``indices ((~) o P) = COMPL (indices P)``, 564 ``recursive (indices P) ��� (indices P = {}) ��� (indices P = UNIV)``, 565 STRIP_TAC THEN Cases_on `indices P = {}` THEN SRW_TAC [][] THEN 566 Cases_on `indices P = UNIV` THEN SRW_TAC [][] THEN 567 `���Q. recursive (indices [all...] |
/seL4-l4v-10.1.1/HOL4/src/0/ |
H A D | KernelTypes.sml | 23 * HOL terms are represented internally using deBruijn indices and explicit *
|
H A D | Term.sml | 674 through the body and replace the dB indices of the prefix with the
|
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/ |
H A D | Dynarray.sig | 47 [bound a] returns an upper bound on the indices of non-default values.
|
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | OmegaSimple.sig | 38 witnesses for the variables. vm maps indices from the list of vars
|
/seL4-l4v-10.1.1/HOL4/src/HolQbf/ |
H A D | QDimacs.sml | 37 (* indices (i.e., positive integers). *) 165 (* 'varfn' must map QDIMACS variable indices (i.e., positive integers) *)
|
H A D | QbfCertificate.sml | 408 val (_, indices) = Redblackmap.find (dict, index) 413 val _ = if List.null indices then 418 val (c_dict, clauses) = Lib.foldl_map derive (c_dict, indices)
|
/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | OldPP.sml | 110 a stack of indices into the token buffer. The indices only point to 384 left_index catches up to right_index and we reset the indices to 0.
|
/seL4-l4v-10.1.1/HOL4/src/new-datatype/ |
H A D | NDatatype.sml | 232 val indices = map gen_tyvar vars value 234 (zip vars indices)
|
/seL4-l4v-10.1.1/HOL4/src/num/termination/ |
H A D | TotalDefn.sml | 393 val indices = Lib.upto 1 (length domtyl_2) value 398 end) indices domtyl_2 ([],[])
|
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/cbv-lc/ |
H A D | cbvScript.sml | 4 * De Bruijn indices for variables. *)
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | stringBinTree.sml | 57 (* this is so that char access for all keys is well-defined, for all indices < mxl *)
|
/seL4-l4v-10.1.1/isabelle/src/HOL/SPARK/Manual/document/ |
H A D | intro.tex | 43 states that all elements of the array \texttt{a} with indices greater or equal to
|
/seL4-l4v-10.1.1/l4v/isabelle/src/HOL/SPARK/Manual/document/ |
H A D | intro.tex | 43 states that all elements of the array \texttt{a} with indices greater or equal to
|
/seL4-l4v-10.1.1/HOL4/examples/lambda/other-models/ |
H A D | pure_dBScript.sml | 48 (* the set of free indices in a term *) 171 (* dFVs gives the free indices of a dB term as strings *)
|
/seL4-l4v-10.1.1/HOL4/src/datatype/ |
H A D | ind_types.sml | 609 val indices = map sucivate (upto (length rargs - 1)) value 610 val rindexed = map (curry mk_comb r) indices 614 val sargs' = map (curry mk_comb s) indices
|
H A D | Datatype.sml | 420 (* j and later indices are ok iff : *)
|
/seL4-l4v-10.1.1/HOL4/src/coalgebras/ |
H A D | pathScript.sml | 469 PL(p) returns the set of valid indices into a path, where the index 473 accepts indices {0, 1}.
|
/seL4-l4v-10.1.1/seL4/manual/parts/ |
H A D | cspace.tex | 31 of the indices of the \obj{CNode} capabilities forming the path to the
|
H A D | objects.tex | 75 address of a capability in a capability space is the concatenation of the indices
|
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | Z3_ProofReplay.sml | 44 updates when the indices are integer or word literals *)
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Nitpick/document/ |
H A D | root.tex | 1094 The $\textit{lift}~t~k$ function increments all variables with indices greater 1125 A substitution is a function that maps variable indices to terms. Observe that 1129 indices when moving under a \textit{Lam}.
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Nitpick/document/ |
H A D | root.tex | 1094 The $\textit{lift}~t~k$ function increments all variables with indices greater 1125 A substitution is a function that maps variable indices to terms. Observe that 1129 indices when moving under a \textit{Lam}.
|