/seL4-l4v-master/HOL4/examples/HolCheck/examples/ |
H A D | ambaScript.sml | 79 (* 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 D | computeRingScript.sml | 164 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 D | ipc.tex | 10 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 D | cspace.tex | 89 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 D | io.tex | 135 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 D | vspace.tex | 117 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 D | TYPECHECK_PARSETREE.sml | 815 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 D | tutorial.ml | 419 (* 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 D | VectorSpaceScript.sml | 199 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 D | OS.sml | 176 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 D | Array.sml | 131 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 D | necec2010.sml | 278 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 D | commonTools.sml | 92 (* 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 D | LTLScript.sml | 269 ; 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 D | ringMapScript.sml | 266 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 D | Net.sig | 39 one term may be indexed by the same path, i.e., the extraction
|
/seL4-l4v-master/HOL4/src/compute/Manual/ |
H A D | description.tex | 22 evaluator which have the same complexity (with a large slow down factor,
|
/seL4-l4v-master/HOL4/src/experimental-kernel/ |
H A D | Net.sig | 39 one term may be indexed by the same path, i.e., the extraction
|
/seL4-l4v-master/HOL4/src/integer/ |
H A D | OmegaShell.sml | 121 * conditional expressions that repeat the same guard should have
|
/seL4-l4v-master/HOL4/src/pattern_matches/ |
H A D | patternMatchesLib.sig | 58 (* 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 D | PIntMap.sml | 23 same data-structure. *)
|
H A D | Redblackmap.sig | 49 overwrite earlier entries for the same index.
|
H A D | Redblackset.sig | 62 same elements.
|
/seL4-l4v-master/HOL4/src/prekernel/ |
H A D | FinalNet-sig.sml | 29 one term may be indexed by the same path, i.e., the extraction
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | Traverse.sig | 46 * Note that this function is *not* the same as
|