109 open Hints_declaration
129 val zoo : Pointers.offset -> Z.z
131 val boo : Z.z -> Pointers.offset
133 val block_decidable_eq :
134 Pointers.block -> Pointers.block -> (__, __) Types.sum
137 Pointers.block -> (Pointers.block, Pointers.offset) Types.prod Types.option
139 val offset_plus : Pointers.offset -> Pointers.offset -> Pointers.offset
141 val pointer_translation :
142 Pointers.pointer -> embedding -> Pointers.pointer Types.option
144 val memory_inj_rect_Type4 :
145 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
148 val memory_inj_rect_Type5 :
149 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
152 val memory_inj_rect_Type3 :
153 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
156 val memory_inj_rect_Type2 :
157 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
160 val memory_inj_rect_Type1 :
161 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
164 val memory_inj_rect_Type0 :
165 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
168 val memory_inj_inv_rect_Type4 :
169 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
170 -> __ -> __ -> 'a1) -> 'a1
172 val memory_inj_inv_rect_Type3 :
173 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
174 -> __ -> __ -> 'a1) -> 'a1
176 val memory_inj_inv_rect_Type2 :
177 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
178 -> __ -> __ -> 'a1) -> 'a1
180 val memory_inj_inv_rect_Type1 :
181 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
182 -> __ -> __ -> 'a1) -> 'a1
184 val memory_inj_inv_rect_Type0 :
185 embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ -> __
186 -> __ -> __ -> 'a1) -> 'a1
188 val memory_inj_jmdiscr : embedding -> GenMem.mem -> GenMem.mem -> __
190 val typesize' : Csyntax.type0 -> Nat.nat