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)