Searched refs:same (Results 51 - 75 of 478) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/examples/HolCheck/examples/
H A DambaScript.sml79 (* APB is the same as APB with bridge instead of master whose ahb signals are hidden *)
98 (* AHB is the same as AHB with bridge as a generic slave whose apb signals are hidden *)
/seL4-l4v-master/HOL4/examples/AKS/compute/
H A DcomputeRingScript.sml164 val _ = set_fixity "+z" (Infixl 500); (* same as + in arithmeticScript.sml *)
172 val _ = set_fixity "oz" (Infixl 600); (* same as * in arithmeticScript.sml *)
188 val _ = set_fixity "*z" (Infixl 600); (* same as * in arithmeticScript.sml *)
223 val _ = set_fixity "**z" (Infixr 700); (* same as EXP in arithmeticScript.sml *)
269 val _ = set_fixity "zwadd" (Infixl 500); (* same as add *)
271 val _ = set_fixity "zcmult" (Infixl 600); (* same as multiply *)
273 val _ = set_fixity "zpmult" (Infixl 600); (* same as multiply *)
275 val _ = set_fixity "zpmod" (Infixl 650); (* same as MOD *)
/seL4-l4v-master/seL4/manual/parts/
H A Dipc.tex10 between threads. The same mechanism is also used for communication with
72 \texttt{badges} and \texttt{caps} use the same area of memory in
232 some specific actions are taken. First a call will do exactly the same action as
260 A reply capability is invoked in the same way as a normal send on a
263 if the reply capability has the Grant right and is done in exactly the same way
H A Dcspace.tex89 capability has the same badge and guard as the original.
103 same, in which case the capability in it is swapped with the
118 any outstanding sends that use the same badge and object as the
133 capabilities will be placed in the same \obj{CNode}.
238 created (see \autoref{s:ep-badge}, \autoref{s:notif-badge}). This new, badged capability to the same object is treated as
461 the L2 and L3 CNode Caps are the same, but that their depth limits
475 IPC buffer. The format of the description is always the same but may
H A Dio.tex135 either a \obj{VSpace} or an \obj{IOSpace} but never into both at the same time.
197 with the same context bank and it is possible to share address translation
199 of translation is the same.
241 SMMU fault interrupts can be handled the same as other platform level interrupts.
324 The SMMU-v2 uses the same paging structure as the MMU (AArch\_64 and AArch\_32
430 Ideally, the SMMU shares the same ASID or VMID name space with the rest of the
471 \item SMMU interrupts are handled as same as other IRQs, i,e, the kernel does not
H A Dvspace.tex117 RISC-V provides the same paging structure for all levels, \texttt{PageTable}. The VSpace is then
285 for IA-32 are shown in \autoref{tbl:vmattr_ia32}\fi. Mapping attributtes can be updated on existing mappings using the Map invocation with the same virtual address.
331 address space. Attempting to map the same capability
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DTYPECHECK_PARSETREE.sml815 same. The result is either of these two once they have been
881 (* We have to be careful because open A B is not the same as
885 we have the same name in multiple structures. *)
997 giving a new name to a type constructor we use the same type
1048 value constructors from the same structure. *)
1058 (* Create a new constructor with the same unique ID. *)
1275 (* The result is an exception with the same type. *)
1475 link it to any type variable with the same name in an outer
1625 link it to any type variable with the same name in an outer
1644 should declare the same functio
[all...]
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A Dtutorial.ml419 (* Instantiated Higher Order functions are translated in the same manner as *)
421 (* the function definition as an instantiation, so the same technique works *)
448 (* Polymorphic functions are translated in exactly the same way as *)
487 (* All of these functions are translated in exactly the same manner as their *)
526 (* The propagation theorems have the same form as the monomorphic propgation *)
684 (* Conditional and limit functions are translated in exactly the same manner.*)
778 (* This functions in the same way as the flattening of normal types, except *)
/seL4-l4v-master/HOL4/examples/algebra/linear/
H A DVectorSpaceScript.sml199 val _ = set_fixity "||" (Infixl 500); (* same as + in arithmeticScript.sml *)
800 (* Adding same-length sticks give another stick of the same length *)
849 (* Negating a stick gives another stick of the same length *)
897 (* Multiply a stick by a scalar gives another stick of the same length *)
977 (* Subtracting same-length sticks give another stick of the same length *)
/seL4-l4v-master/HOL4/polyml/basis/
H A DOS.sml176 be the same as the Posix.Error functions. Those are
567 contains a volume name, refer to the same volume as the first. *)
575 (i.e. concat("a/", "b") is the same as concat("a", "b") *)
605 same as the absolute path. *)
630 (* Are they the same arc? Note: When arcs are
646 same as the absolute path. *)
1014 the same IO descriptor with the same or different flags. On Cygwin, at
1083 different bits for the same file descriptor. *)
H A DArray.sml131 to be the same but in that case di would have to be zero otherwise the length
250 to be the same and for the source and destinations to overlap so we
251 have to take care of that. If they are not the same we could simply
/seL4-l4v-master/HOL4/examples/imperative/
H A Dnecec2010.sml278 the other for the right-hand side. EQ_TAC was not used in the example, but does the same for equations.
294 where s is free provided that s x and s y exist and are of the same type.
297 We wish to show that provided $s x$, $s' x$, $s y$ and $s' y$ are the same type, the following are valid implementatons:
/seL4-l4v-master/HOL4/examples/HolCheck/
H A DcommonTools.sml92 (* both lists should be same length, otherwise exception *)
228 (* push outermost quantifier inwards n times through same quants. Will fail if there aren't enough quants or if they are not the same *)
/seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/
H A DLTLScript.sml269 ; n has the same set of successor states (with respect to vars).
273 ; vice-versa, where we consider two states to be the same if
274 ; they are the same when restricted to vars.
/seL4-l4v-master/HOL4/examples/algebra/ring/
H A DringMapScript.sml266 val _ = set_fixity "~r~" (Infix(NONASSOC, 450)); (* same as relation *)
267 val _ = set_fixity "=r=" (Infix(NONASSOC, 450)); (* same as relation *)
285 val _ = set_fixity "+_" (Infixl 500); (* same as + in arithmeticScript.sml *)
286 val _ = set_fixity "-_" (Infixl 500); (* same as - in arithmeticScript.sml *)
287 val _ = set_fixity "*_" (Infixl 600); (* same as * in arithmeticScript.sml *)
288 val _ = set_fixity "**_" (Infixr 700); (* same as EXP in arithmeticScript.sml, infix right *)
556 (* This is the same as ring_homo_trans *)
583 (* This is the same as ring_homo_sym, direct proof. *)
929 (* This is the same as ring_iso_trans. *)
986 (* This is the same a
[all...]
/seL4-l4v-master/HOL4/src/0/
H A DNet.sig39 one term may be indexed by the same path, i.e., the extraction
/seL4-l4v-master/HOL4/src/compute/Manual/
H A Ddescription.tex22 evaluator which have the same complexity (with a large slow down factor,
/seL4-l4v-master/HOL4/src/experimental-kernel/
H A DNet.sig39 one term may be indexed by the same path, i.e., the extraction
/seL4-l4v-master/HOL4/src/integer/
H A DOmegaShell.sml121 * conditional expressions that repeat the same guard should have
/seL4-l4v-master/HOL4/src/pattern_matches/
H A DpatternMatchesLib.sig58 (* Use same variable names for pattern, guard and rhs *)
65 (* Enforce each pattern to have the same number of columns, i.e.
87 either the same constructor or a variable. *)
328 numbers are preferred. If two columns have the same
/seL4-l4v-master/HOL4/src/portableML/
H A DPIntMap.sml23 same data-structure. *)
H A DRedblackmap.sig49 overwrite earlier entries for the same index.
H A DRedblackset.sig62 same elements.
/seL4-l4v-master/HOL4/src/prekernel/
H A DFinalNet-sig.sml29 one term may be indexed by the same path, i.e., the extraction
/seL4-l4v-master/HOL4/src/simp/src/
H A DTraverse.sig46 * Note that this function is *not* the same as

Completed in 186 milliseconds

1234567891011>>