Bytelist-bytelist-map
Fixtype of maps from byte arrays to byte arrays.
An MMP tree represents a finite map from byte arrays to byte arrays,
as described by \mathfrak{I} [YP:(188)].
The type we introduce here models these finite maps.
Note that there are no constraints on the lengths of the keys or values,
because the construction of MMP trees from these finite maps
(which is described in [YP:D])
does not depend on any such length constraints.
Subtopics
- Bytelist-bytelist-mfix
- (bytelist-bytelist-mfix x) is a usual ACL2::fty omap fixing function.
- Bytelist-bytelist-mapp
- Recognizer for bytelist-bytelist-map.
- Bytelist-bytelist-mequiv
- Basic equivalence relation for bytelist-bytelist-map structures.
