Add shuffle rule
Status | Pipeline | Created by | Stages | Actions |
---|---|---|---|---|
Passed 00:02:38
| Stage: build | No artifacts found |
This adds a shuffle rule to Alethe that can be used to change the order of arguments of commutative operators. Two remarks:
(step s1 (= (cl (+ a b c) (+ b a c)) :rule shuffle :args (2 1 3))
However, I am not certain of hard it is to generate this. I suggest we think about adding this after Hanna used this rule.
reordering
to shuffle_clause
. In the proofs meeting yesterday we said that "reorder" is not a good name, because it implies a specific order.Status | Pipeline | Created by | Stages | Actions |
---|---|---|---|---|
Passed 00:02:38
| Stage: build |
Download artifacts
No artifacts found |