Add class `TopSet` for sets with ⊤ element (!111) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Robbert Krebbers requested to merge robbert/top_set into master 5 years ago

This closes issue #49 (closed). Some remarks:

It's called TopSet, which corresponds with SemiSet.
We now have a generic SetUnfoldElemOf for any TopSet.
The Hint Resolve coPset_top_subseteq : core no longer works because the lemma is generic in a type class. AFAIK it is only used for solve_ndisjoint, so I added a specialized version to the ndisj hint database. We already have specialized versions of other set lemmas there.

Approval is optional

Activity

Robbert Krebbers added 1 commit 5 years ago
added 1 commit

99774e1e - CHANGELOG entry.

Compare with previous version
Robbert Krebbers @robbertkrebbers 5 years ago

Author Owner

@swasey Could you review?
David Swasey @swasey 5 years ago

Contributor

I will take a look tomorrow (and at the cogset comments). Thanks!
Robbert Krebbers added 5 commits 5 years ago
added 5 commits

9a1b4cde - 1 commit from branch master

ddfcc76c - Move lattice related stuff up.

e09f7ce3 - Add class `TopSet` for sets with ⊤ element.

982e99e0 - CHANGELOG entry.

73b789ea - `TopSet` instance for `boolset`.

Compare with previous version
Toggle commit list
Robbert Krebbers added 2 commits 5 years ago
added 2 commits

2ad56b99 - `TopSet` instance for `boolset`.

ab51e3fd - CHANGELOG entry.

Compare with previous version
David Swasey @swasey 5 years ago

Contributor

LGTM.
David Swasey mentioned in merge request !108 (merged) 5 years ago

mentioned in merge request !108 (merged)
Robbert Krebbers merged 5 years ago

merged
Robbert Krebbers mentioned in commit af368a15 5 years ago

mentioned in commit af368a15

Please register or sign in to reply