Add Qp lemmas (!187) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

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

All threads resolved!

Adds a two additional lemmas for Qp.

Also renames a few lemmas that accidentally had Qc in their name instead of Qp. These where introduced back in !179 (merged) so it's probably safe to assume that no one are using the misnamed ones.

Activity

Simon Friis Vindum @simonfv started a thread on the diff 4 years ago

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

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

Resolved 4 years ago by Robbert Krebbers

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

Resolved 4 years ago by Robbert Krebbers

Simon Friis Vindum added 1 commit 4 years ago

added 1 commit

94a98b3f - Change eapply to apply

Compare with previous version

Simon Friis Vindum added 1 commit 4 years ago

added 1 commit

028eb93c - Remove Qp_not_plus_q_ge_1

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 7ae77142

Robbert Krebbers @robbertkrebbers · 4 years ago

Owner

@iris-users This is a breaking change if you use Qp_not_plus_q_ge_1

Please register or sign in to reply