Skip to content

prove map_size_delete, map_size_insert_Some, map_to_list_delete

Ralf Jung requested to merge ralf/map-size into master

map_size_insert_Some exists in Perennial as map_size_insert_overwrite, but with a very different proof.

Merge request reports