Add list_subseteq_dec (!400) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Michael Sammler requested to merge ci/msammler/list_subseteq_dec into master 2 years ago

All threads resolved!

I am not sure where to put this instance in this file. The best place would probably be after elem_of_list_dec, but there the Decision instance for Forall is not yet there.

Activity

Michael Sammler assigned to @msammler 2 years ago

assigned to @msammler
Robbert Krebbers @robbertkrebbers · 2 years ago

Owner

Resolved 2 years ago by Robbert Krebbers

It looks like you can move the whole block with properties of ⊆ after the properties of Forall.

Would that make sense?

Last reply by Michael Sammler 2 years ago
Michael Sammler added 1 commit 2 years ago
added 1 commit

ef9d9dde - Add list_subseteq_dec

Compare with previous version
Robbert Krebbers resolved all threads 2 years ago

resolved all threads
Robbert Krebbers @robbertkrebbers · 2 years ago

Owner

LGTM!
Robbert Krebbers merged 2 years ago

merged
Robbert Krebbers mentioned in commit 9d78117d 2 years ago

mentioned in commit 9d78117d

Please register or sign in to reply