Add lemmas about `list_to_map` (!199) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Simon Friis Vindum requested to merge simonfv/stdpp:add-lemma into master 4 years ago

All threads resolved!

Adds two lemmas about list_to_map that seem generally useful.

Activity

Simon Friis Vindum added 1 commit 4 years ago
added 1 commit

1b9b1ef7 - Add lemmas about list_to_map

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

Resolved 4 years ago by Simon Friis Vindum
Last reply by Robbert Krebbers 4 years ago

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

Resolved 4 years ago by Simon Friis Vindum

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

Resolved 4 years ago by Robbert Krebbers

Robbert Krebbers @robbertkrebbers · 4 years ago

Owner

Many thanks for the MR. Please lemmas are useful. I left some minor comments.

Simon Friis Vindum added 1 commit 4 years ago

added 1 commit

4f541628 - Refactor proof of list_to_map_snoc

Compare with previous version

Robbert Krebbers resolved all threads 4 years ago

resolved all threads

Robbert Krebbers merged 4 years ago

merged

Robbert Krebbers mentioned in commit 4 years ago

mentioned in commit dcfe9839

Robbert Krebbers @robbertkrebbers · 4 years ago

Owner

Merged. Many thanks.

Please register or sign in to reply