| /seL4-l4v-master/HOL4/examples/STE/Examples/ |
| H A D | Comparator-for-STE-Reduction.sml | 83 val a0 = (T, "a0", ``a0:bool``, 0, 1); value
[all...] |
| H A D | Mux.sml | 140 val a0 = (T, "a0", value
165 val a0 = (T, "a0", ``va0:bool``, 0, 1); value
188 val a0 = (T, "a0", ``va0:bool``, 0, 1); value
[all...] |
| H A D | Comparator.sml | 95 val a0 = (T, "a0", ``a0 value
115 val a0 = (T, "a0", ``T:bool``, 0, 1); value
135 val a0 = (T, "a0", ``a0:bool``, 0, 1); value
155 val a0 = (T, "a0", ``v0:bool``, 0, 1); value
175 val a0 = (T, "a0", ``T:bool``, 0, 1); value
195 val a0 = (T, "a0", ``T:bool``, 0, 1); value
215 val a0 = (T, "a0", ``T:bool``, 0, 1); value
235 val a0 = (T, "a0", ``T:bool``, 0, 1); value
[all...] |
| /seL4-l4v-master/seL4/libsel4/arch_include/riscv/sel4/arch/ |
| H A D | types.h | 47 seL4_Word a0; member in struct:seL4_UserContext_
|
| /seL4-l4v-master/HOL4/src/AI/sml_inspection/ |
| H A D | smlParser.sml | 195 val (a0,ainf,a1) = dest_infix a value
|
| /seL4-l4v-master/seL4/include/arch/riscv/arch/machine/ |
| H A D | registerset.h | 37 a0 = 9, capRegister = 9, badgeRegister = 9, enumerator in enum:_register
|
| /seL4-l4v-master/HOL4/src/integer/ |
| H A D | CooperShell.sml | 407 val (a0,b0) = Binarymap.find(map, v) value
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
| H A D | stateLib.sml | 396 val a0 = define_assert0 sthy pred_ty value
|
| /seL4-l4v-master/HOL4/src/bool/ |
| H A D | boolScript.sml | 3821 val a0 = TRANS (ASSUME fT_eq_T) (SYM (BETA_CONV (mk_comb(KT,T)))) value
3913 val a0 = SPEC f BOOL_FUN_CASES_THM value
|