Changeset 2773 for extracted/memoryInjections.mli
- Timestamp:
- Mar 4, 2013, 10:03:33 AM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
extracted/memoryInjections.mli
r2717 r2773 47 47 open Csem 48 48 49 open BitVectorTrie50 51 49 open CostLabel 52 50 … … 67 65 open Extralib 68 66 69 open Setoids70 71 open Monad72 73 open Option74 75 67 open Lists 76 68 … … 87 79 open Div_and_mod 88 80 81 open Util 82 83 open FoldStuff 84 85 open BitVector 86 89 87 open Jmeq 90 88 … … 93 91 open List 94 92 95 open Util93 open Setoids 96 94 97 open FoldStuff95 open Monad 98 96 99 open BitVector97 open Option 100 98 101 99 open Extranat … … 145 143 146 144 val memory_inj_rect_Type4 : 147 embedding -> GenMem.mem 1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->148 __-> __ -> 'a1) -> 'a1145 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __ 146 -> __ -> 'a1) -> 'a1 149 147 150 148 val memory_inj_rect_Type5 : 151 embedding -> GenMem.mem 1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->152 __-> __ -> 'a1) -> 'a1149 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __ 150 -> __ -> 'a1) -> 'a1 153 151 154 152 val memory_inj_rect_Type3 : 155 embedding -> GenMem.mem 1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->156 __-> __ -> 'a1) -> 'a1153 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __ 154 -> __ -> 'a1) -> 'a1 157 155 158 156 val memory_inj_rect_Type2 : 159 embedding -> GenMem.mem 1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->160 __-> __ -> 'a1) -> 'a1157 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __ 158 -> __ -> 'a1) -> 'a1 161 159 162 160 val memory_inj_rect_Type1 : 163 embedding -> GenMem.mem 1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->164 __-> __ -> 'a1) -> 'a1161 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __ 162 -> __ -> 'a1) -> 'a1 165 163 166 164 val memory_inj_rect_Type0 : 167 embedding -> GenMem.mem 1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->168 __-> __ -> 'a1) -> 'a1165 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __ 166 -> __ -> 'a1) -> 'a1 169 167 170 168 val memory_inj_inv_rect_Type4 : 171 embedding -> GenMem.mem 1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->172 __-> __ -> __ -> 'a1) -> 'a1169 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __ 170 -> __ -> __ -> 'a1) -> 'a1 173 171 174 172 val memory_inj_inv_rect_Type3 : 175 embedding -> GenMem.mem 1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->176 __-> __ -> __ -> 'a1) -> 'a1173 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __ 174 -> __ -> __ -> 'a1) -> 'a1 177 175 178 176 val memory_inj_inv_rect_Type2 : 179 embedding -> GenMem.mem 1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->180 __-> __ -> __ -> 'a1) -> 'a1177 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __ 178 -> __ -> __ -> 'a1) -> 'a1 181 179 182 180 val memory_inj_inv_rect_Type1 : 183 embedding -> GenMem.mem 1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->184 __-> __ -> __ -> 'a1) -> 'a1181 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __ 182 -> __ -> __ -> 'a1) -> 'a1 185 183 186 184 val memory_inj_inv_rect_Type0 : 187 embedding -> GenMem.mem 1 -> GenMem.mem1 -> (__ -> __ -> __ -> __ -> __ ->188 __-> __ -> __ -> 'a1) -> 'a1185 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __ 186 -> __ -> __ -> 'a1) -> 'a1 189 187 190 val memory_inj_jmdiscr : embedding -> GenMem.mem 1 -> GenMem.mem1-> __188 val memory_inj_jmdiscr : embedding -> GenMem.mem -> GenMem.mem -> __ 191 189 192 190 val typesize' : Csyntax.type0 -> Nat.nat
Note: See TracChangeset
for help on using the changeset viewer.