Searched refs:same (Results 1 - 25 of 478) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/src/Boolify/src/
H A DEncode.sig4 (* Basically the same as Konrad Slind's code to generate size functions *)
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DSharing.sml83 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 DSharing.sml83 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 DFCNet.sig17 Provides a matching function that does the same.
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/ppc/
H A Dppc_astScript.sml48 | 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 DSingleAssignment.sml29 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 DLibrarySupport.sml31 (* 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 DForeignConstants.sml25 same as the size. *)
H A DWord8Array.sml23 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 DRecordType.sig20 which modifies a tyinfo in the same way as the result has just been
/seL4-l4v-master/HOL4/src/portableML/
H A DPEGParse.sig49 if repeated calls to the same input ('source) arguments always give
50 the same result.
/seL4-l4v-master/HOL4/developers/discussion/
H A Doverloading-extension.tex34 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 Dunquote-init.sml7 (* used to stand for "has double quote", but the same analysis is necessary
/seL4-l4v-master/HOL4/examples/simple_complexity/lib/
H A DcomplexityScript.sml193 (* 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 DsublistScript.sml193 <=> 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 DSanity.sig42 Turn checks whether the same theorem name is used in multiple theories.
/seL4-l4v-master/HOL4/src/1/theory_tests/
H A DmergeGrammarsA1Script.sml29 to equality, this should result in B's grammar being the same as
/seL4-l4v-master/HOL4/src/portableML/poly/
H A DDynarray.sig28 [subArray(a, m, n)] returns a new array with the same default
/seL4-l4v-master/HOL4/src/ring/src/
H A DringLib.sig32 * equivalent polynomial expressions sharing the same valuation.
/seL4-l4v-master/HOL4/Manual/Reference/
H A Dpreface.tex32 from the same database that is used by the help system. For an introduction to
/seL4-l4v-master/HOL4/examples/HolCheck/
H A DenvScript.sml34 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 Dx86assembly_gas32.S136 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 DLinearIndepScript.sml78 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 Dexample.sml158 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 Ddescription.tex21 since the same effect can be achieved by careful use of rewriting.
124 \item \ml{REDUCE\_TAC} performs the same reductions on a goal.

Completed in 149 milliseconds

1234567891011>>