This adds a logic-level version of gmap_view
, dubbed ghost_map
(in parallel to the existing ghost_var
). The API mirrors that of gen_heap
. I think this also provides everything Perennial's auth_map
has, except for operations on "fragment maps" (for which we lack good support in gmap_view
). Cc @tchajed
This seems like something with many possible uses, so I went for full sealing and also added a notation for the elements: k ↪[γ]{dq} v
. Obviously, notation and naming are up for bikeshedding. Also for now this library enforces Leibniz equality, but I feel it might be worth supporting Equiv
(but it would probably help -- for client usability -- to not support arbitrary OFEs).
The notation follows @robbertkrebbers's proposal of using the shortest, "most desirable" notation for the general case of a discardable fraction, and using k ↪[γ]{#q} v
for q: frac
. I could also imagine doing this the other way around, i.e., letting #
indicate dfrac
. General lemmas should be written for dfrac
whenever possible, but clients that actually split this fraction will likely work with 1/2
and 1/4
and would have to add a #
everywhere currently.
Fixes #358 (closed)