An error occurred while fetching folder content.
Forked from
Iris / Actris
Source project has a limited visibility.
Robbert Krebbers
authored
This reverts commit 24fa20e5f8a2042caa19f1f6505102c5434cce54. Although these symmetric variants sometimes look "better", they are really annoying and should IMHO never be used: 1.) For lemmas there is now a choice between >= and <=. Since there is no longer a canonical choice, it is very easy to introduce a lot of inconsistencies in statements of lemmas. 2.) For automation the situation becomes annoying, you have to built in stuff for both >= and <=. That is very error-prone. 3.) For N and Z the notions x <= y and y >= x are not even convertible! That means that done/by does not solve x <= y if you have y >= x and if avoids you applying certain lemmas.
Name | Last commit | Last update |
---|