5 ms·
I'm pretty sure you can define commutive and associative relations in Coq.
by hopscotch 9y ago
I'm pretty sure you can define commutive and associative relations in Coq.
- seanwilson 9y agoWhat do you mean? You can write theorems that show plus is associative and commutative for example but that doesn't make the example I gave "equal" in Coq in the sense you normally mean. As I said, it's not intuitive as we're usually very loose in what we mean by "equal".