walker (Nov 21 2022 at 12:59): walker (Nov 21 2022 at 12:59):Paolo Giarrusso said:
Or the stronger
(A /\ ~B) \/ (B /\ ~A)...
This is how I did it but if A and B are very long, it looks ugly, so I thought maybe there was a nice built in syntax for that
Notification Bot (Nov 21 2022 at 12:59):walker has marked this topic as resolved.
Paolo Giarrusso (Nov 21 2022 at 17:55):@walker you can wrap that in a definition, or create a custom inductive. There's also (next to) nothing built-in about conjunction and disjunction, they're just inductives in the stdlib
Paolo Giarrusso (Nov 21 2022 at 17:56):(I won't be surprised if there's hardcoded behavior for conjunction and disjunction, but a pure library solution is good enough for xor)
Last updated: Feb 06 2023 at 12:04 UTC