More lemmas for list's prefix_of and suffix_of (!239) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Hai Dang requested to merge improve_prefix_suffix into master 4 years ago

All threads resolved!

More properties of prefix_of and suffix_of:

they are partial orders, not just pre orders
prefix_nil_inv and prefix_of_down_total.

Approval is optional

Activity

Ralf Jung @jung 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

Hai Dang mentioned in merge request iris!661 (merged) 4 years ago

mentioned in merge request iris!661 (merged)

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 · 4 years ago

Owner

Resolved 4 years ago by Hai Dang

These are very useful lemmas, thanks! I shortened the proofs a bit.
Last reply by Hai Dang 4 years ago

Hai Dang added 1 commit 4 years ago

added 1 commit

7624e5fe - Shorten proofs

Compare with previous version

Hai Dang added 1 commit 4 years ago

added 1 commit

ea318202 - Rename down_total to weak_total; Add a counterpart for suffix

Compare with previous version

Hai Dang 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 abee55c9

Robbert Krebbers @robbertkrebbers · 4 years ago

Owner

LGTM. Thanks!

Please register or sign in to reply