Closed patham9 closed 8 years ago
I guess commutative matching has a high price anyway, and is probably not compatible with core.unify. So I will generate permuted terms on matching now as it was the case in 1.5.x, this approach seems quite doable also for me.
this one is fixed since yesterday evening.
Internal representation for (<-> A B) should be (<-> #{A B}) in order to allow taking commutativity of <-> into account by the rule engine. Also for consistency: (--> [A B]) instead of (--> A B).
Motivation:
with
the derivation currently can not happen without additional rule.