/seL4-l4v-master/HOL4/src/Boolify/src/ |
H A D | Encode.sig | 4 (* Basically the same as Konrad Slind's code to generate size functions *)
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Sharing.sml | 83 fun m ys same xxss = 89 val same = same andalso x == y value 90 val ys = if same then xs else y :: ys 92 m ys same xxss 100 fun m acc ys same xxss = 106 val same = same andalso x == y value 107 val ys = if same then xs else y :: ys 109 m acc ys same xxs [all...] |
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Sharing.sml | 83 fun m ys same xxss = 89 val same = same andalso x == y value 90 val ys = if same then xs else y :: ys 92 m ys same xxss 100 fun m acc ys same xxss = 106 val same = same andalso x == y value 107 val ys = if same then xs else y :: ys 109 m acc ys same xxs [all...] |
/seL4-l4v-master/HOL4/src/parse/ |
H A D | FCNet.sig | 17 Provides a matching function that does the same.
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/ppc/ |
H A D | ppc_astScript.sml | 48 | Pcmplwi of ireg => ppc_constant (* same, with immediate argument *) 50 | Pcmpwi of ireg => ppc_constant (* same, with immediate argument *) 72 | Plbzx of ireg => ireg => ireg (* same, with 2 index regs *) 74 | Plfdx of freg => ireg => ireg (* same, with 2 index regs *) 76 | Plfsx of freg => ireg => ireg (* same, with 2 index regs *) 78 | Plhax of ireg => ireg => ireg (* same, with 2 index regs *) 80 | Plhzx of ireg => ireg => ireg (* same, with 2 index regs *) 82 | Plwzx of ireg => ireg => ireg (* same, with 2 index regs *) 102 | Pstbx of ireg => ireg => ireg (* same, with 2 index regs *) 104 | Pstfdx of freg => ireg => ireg (* same, wit [all...] |
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | SingleAssignment.sml | 29 to the same reference.*) 36 threads may attempt to assign to the same reference.*) 66 They are given a value when they are created in the same way as immutable data 69 structures are considered equal if their contents are the same, mutable cells 70 are considered equal only if they are the pointers to the same cell. 75 possible to reduce the heap size by merging immutable cells that have the same
|
H A D | LibrarySupport.sml | 31 (* This is the same as wordSize in native 32-bit and 64-bit but different in 32-in-64. *) 109 (* The representation of Word8Vector.vector is the same as that of string. We 110 define it as "string" here so that it inherits the same equality function. 166 It seems best to use the same maximum size for CharArray/Word8Array. *) 187 merge strings that are otherwise the same. *) 217 (* syserror is the same as SysWord.word and these are needed in Posix at least. *)
|
H A D | ForeignConstants.sml | 25 same as the size. *)
|
H A D | Word8Array.sml | 23 of handling this. We could implement byte vectors in the same 26 course, treat arrays in the same way. Implementing vectors as 70 as a byte all these functions have the same implementation in 73 conversion of Word8.word from char to an opaque type at the same 207 same but in that case di must be zero (since len = dlen) and the copy is 370 (* Copy a slice into an array. N.B. The arrays could be the same. *) 379 on the index whether the source and destination are the same or not.
|
/seL4-l4v-master/HOL4/src/datatype/record/ |
H A D | RecordType.sig | 20 which modifies a tyinfo in the same way as the result has just been
|
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | PEGParse.sig | 49 if repeated calls to the same input ('source) arguments always give 50 the same result.
|
/seL4-l4v-master/HOL4/developers/discussion/ |
H A D | overloading-extension.tex | 34 definition must be for a term of the same type and name of an existing 54 different refinements of the same constant in different branches off 55 the same root. This can be emulated in our existing systems by 73 be exactly the same as that given in the constant's declaration. 82 the same name but different types. Without the monomorphism 133 really one from name-type pairs to lists of the same. 139 reject it. But this same circular dependency test would probably
|
/seL4-l4v-master/HOL4/tools/ |
H A D | unquote-init.sml | 7 (* used to stand for "has double quote", but the same analysis is necessary
|
/seL4-l4v-master/HOL4/examples/simple_complexity/lib/ |
H A D | complexityScript.sml | 193 (* Proof: by big_O_def, take same k and c. *) 237 val _ = set_fixity ".+." (Infixl 500); (* same as addition *) 246 val _ = set_fixity ".*." (Infixl 600); (* same as multiplication *) 258 val _ = set_fixity "|+|" (Infixl 500); (* same as numeric addition *) 288 val _ = set_fixity "|*|" (Infixl 600); (* same as numeric multiplication *) 589 Take the same k, but use (c' + c) for c''. 611 Take the same k, but use (c' * c) for c''. 647 Take the same k and (2 * c). 677 Take the same k and (3 * c'). 721 Take the same [all...] |
/seL4-l4v-master/HOL4/examples/algebra/lib/ |
H A D | sublistScript.sml | 193 <=> t <= q by sublist_def, same heads 245 <=> (t <= q) and (q <= t) by sublist_def, same heads 333 Then t <= q by sublist_def, same heads 527 If h' = h, t <= y by sublist_def, same heads 588 By induction on list p, and note that p and (p ++ q) have the same head. 648 Then t ++ h::q <= q by sublist_def, same heads 726 Then t ++ [h'] <= q ++ [h'] by sublist_def, same heads 795 For this case, choose x=[], y=q, and sublist (h::t) (h::q) = sublist t q, by SUBLIST same head. 801 hence sublist t y = sublist t q ==> sublist (h::t) (h::q) by SUBLIST same head. 859 Then t <= q by sublist_def, same head [all...] |
/seL4-l4v-master/HOL4/src/1/ |
H A D | Sanity.sig | 42 Turn checks whether the same theorem name is used in multiple theories.
|
/seL4-l4v-master/HOL4/src/1/theory_tests/ |
H A D | mergeGrammarsA1Script.sml | 29 to equality, this should result in B's grammar being the same as
|
/seL4-l4v-master/HOL4/src/portableML/poly/ |
H A D | Dynarray.sig | 28 [subArray(a, m, n)] returns a new array with the same default
|
/seL4-l4v-master/HOL4/src/ring/src/ |
H A D | ringLib.sig | 32 * equivalent polynomial expressions sharing the same valuation.
|
/seL4-l4v-master/HOL4/Manual/Reference/ |
H A D | preface.tex | 32 from the same database that is used by the help system. For an introduction to
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | envScript.sml | 34 environments to evaluate to the same thing, rather than not evaluate at all. Using {} is not as satisfactory theoretically but more
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | x86assembly_gas32.S | 136 fldcw Arg_SaveFP(%ebp) # ...load because we need the same rounding mode in the RTS 172 # This implements atomic addition in the same way as atomic_increment
|
/seL4-l4v-master/HOL4/examples/algebra/linear/ |
H A D | LinearIndepScript.sml | 78 val _ = set_fixity "||" (Infixl 500); (* same as + in arithmeticScript.sml *) 244 If n is nonzero at index k, the basis b at same index k, after deletion (from list), 245 will span the same subspace. 275 and it is almost simple to argue that its inverse should be in the same carrier. 346 If h is already spanned by b (or b'), (h::b) spans the same space. 347 If h is not spanned by b (or b'), (h::b) gives another dimension, same as (h::b'). 358 i.e. there is another sticks of the same length giving a nonzero representation of zero vector.
|
/seL4-l4v-master/HOL4/src/datatype/mutrec/examples/ |
H A D | example.sml | 158 appear in the same mutually recursive function definition, type 159 inference will attempt to make the types of both "rst" be the same. This
|
/seL4-l4v-master/HOL4/src/num/reduce/Manual/ |
H A D | description.tex | 21 since the same effect can be achieved by careful use of rewriting. 124 \item \ml{REDUCE\_TAC} performs the same reductions on a goal.
|