aac-tactics icon indicating copy to clipboard operation
aac-tactics copied to clipboard

Published 20 hours ago • verified publisher icon coq-community

aac_congruence

Open aa755 opened this issue 9 months ago • 20 comments

I recently found this library and found it to be very useful and wish I knew about it years ago. Is it possible/easy to implement aac_congruence using the machinery defined here? For example, before calling congruence, one could put in some uniquish normal form expressions containing associative and commutative operators, similar to what ring_simplify does. If anyone has thought about writing aac_congruence or aac_normalize I would love to know their thoughts and experiences.

aa755 avatar May 23 '24 13:05 aa755