prove map_size_delete, map_size_insert_Some, map_to_list_delete (!208) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Ralf Jung requested to merge ralf/map-size into master 4 years ago

All threads resolved!

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

Activity

Robbert Krebbers @robbertkrebbers started a thread on an old version of the diff 4 years ago

Resolved 4 years ago by Ralf Jung
Last reply by Ralf Jung 4 years ago

Robbert Krebbers @robbertkrebbers started a thread on the diff 4 years ago

Resolved 4 years ago by Ralf Jung

Ralf Jung added 2 commits 4 years ago

added 2 commits

c4875672 - simplify proof (by Robbert)
83901f25 - adjust map_size_delete statement

Compare with previous version

Ralf Jung resolved all threads 4 years ago

resolved all threads

Ralf Jung resolved all threads 4 years ago

resolved all threads

Robbert Krebbers @robbertkrebbers · 4 years ago

Owner

Thanks. Merging.

Robbert Krebbers merged 4 years ago

merged

Robbert Krebbers mentioned in commit 4 years ago

mentioned in commit b55715d3

Please register or sign in to reply