Remove existential quantifiers in swapping case of `iProto_le`. (!23) · Merge requests · Iris / Actris · GitLab

Snippets Groups Projects

Merged Robbert Krebbers requested to merge robbert/iProto_le_swap_tweak into master 4 years ago

Activity

Robbert Krebbers added 1 commit 4 years ago
added 1 commit

bab74e34 - Apply the same approach to `iProto_interp`.

Compare with previous version
Robbert Krebbers added 1 commit 4 years ago
added 1 commit

0d6a5514 - Tweak `iProto_interp`.

Compare with previous version
Robbert Krebbers added 1 commit 4 years ago
added 1 commit

2d731f1d - Avoid ⊑ in iProto_interp lemmas.

Compare with previous version
Jonas Kastberg added 5 commits 4 years ago
added 5 commits

2007d5b5 - 1 commit from branch master

7b4228f4 - Remove existential quantifiers in swapping case of `iProto_le`.

2446e9b6 - Apply the same approach to `iProto_interp`.

103e78a9 - Tweak `iProto_interp`.

7d85ab9a - Avoid ⊑ in iProto_interp lemmas.

Compare with previous version
Toggle commit list
Jonas Kastberg approved this merge request 4 years ago

approved this merge request
Jonas Kastberg merged 4 years ago

merged
Jonas Kastberg mentioned in commit d4aa324b 4 years ago

mentioned in commit d4aa324b

Please register or sign in to reply