[Chore] Add some optimization rules
Side note: DROP n ; DROP
would work by the same principle, but the issue with that is we'd need KnownList
constraint on DROP
's input, and that one's used extensively in a lot of places, some of those aren't trivial to extend with the constraint.
Description
Problem: While working on another project (context), we found some optimization rules are missing. Those with proofs (or not requiring proofs) can be added to morley.
Solution: Add those rules. Some PeanoSing utilities were needed, so
those are added as well. One caveat is that DIG
now requires
KnownList
constraint on its input.
Related issue(s)
None
✅ Checklist for your Merge Request
Related changes (conditional)
-
Tests (see short guidelines)
-
If I added new functionality, I added tests covering it. -
If I fixed a bug, I added a regression test to prevent the bug from silently reappearing again.
-
-
Documentation
Stylistic guide (mandatory)
-
My commits comply with the following policy. -
My code complies with the style guide.
Edited by Nikolay Yakimov