Add more lemmas for FinMaps (for union, filter, difference) (!245) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Hai Dang requested to merge hai/more_finmaps into master 4 years ago

Some lemmas that I believe worth upstreaming.

Edited 4 years ago by Hai Dang

Activity

Hai Dang changed the description 4 years ago

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

Resolved 4 years ago by Hai Dang
Last reply by Hai Dang 4 years ago

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

Resolved 4 years ago by Hai Dang

Hai Dang added 1 commit 4 years ago

added 1 commit

03f3428b - Cleanup some proofs for FinMaps

Compare with previous version

Hai Dang resolved all threads 4 years ago

resolved all threads

Hai Dang added 1 commit 4 years ago

added 1 commit

33a02fc6 - Add some more lemmas for difference

Compare with previous version

Hai Dang @haidang · 4 years ago

Author Owner

I added two more lemmas for map difference. PTAL.

Hai Dang changed title from Add more lemmas for FinMaps (for union and filter) to Add more lemmas for FinMaps (for union, filter, difference) 4 years ago

changed title from Add more lemmas for FinMaps (for union and filter) to Add more lemmas for FinMaps (for union, filter, difference)

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

Resolved 4 years ago by Hai Dang

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

Resolved 3 years ago by Ralf Jung

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

Resolved 4 years ago by Hai Dang

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

Resolved 4 years ago by Hai Dang

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

Resolved 3 years ago by Ralf Jung

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

Resolved 4 years ago by Hai Dang

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

Resolved 4 years ago by Hai Dang

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

Resolved 4 years ago by Hai Dang

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

Resolved 4 years ago by Hai Dang

Hai Dang added 1 commit 4 years ago

added 1 commit

2bf388cc - Apply 2 suggestion(s) to 1 file(s)

Compare with previous version

Hai Dang added 1 commit 4 years ago

added 1 commit

62ce48ff - Strengthen, rename, and move some lemmas

Compare with previous version

Hai Dang added 2 commits 4 years ago

added 2 commits

91705526 - Generalize insert_difference
7d0a7027 - Some proof cleanup

Compare with previous version

Please register or sign in to reply