Stream: Coq users

Topic: ✔ logical xor


view this post on Zulip 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

view this post on Zulip Notification Bot (Nov 21 2022 at 12:59):

walker has marked this topic as resolved.

view this post on Zulip 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

view this post on Zulip 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