## Stream: new members

### Topic: bool.bxor_iff_eq

#### Donald Sebastian Leung (Jun 10 2020 at 13:38):

In data.bool, there is a lemma bool.bxor_iff_ne which states that bxor x y = bool.tt ↔ x ≠ y for all x, y; however, there doesn't seem to be bool.bxor_iff_eq stating that bxor x y = bool.ff ↔ x = y. Did I miss something?

#### Patrick Massot (Jun 10 2020 at 13:41):

I'm not too surprised that bool misses lemmas. Either you're proving stuff and work with Prop or you're programming and work with bool without needing lemmas.

#### Mario Carneiro (Jun 10 2020 at 13:43):

I would rather see this lemma proven by rewriting bxor x y = bool.ff to \neg \u (bxor x y) and from there to \neg (x != y) and then x = y

#### Mario Carneiro (Jun 10 2020 at 13:44):

in short, make everything a prop as soon as possible

#### Mario Carneiro (Jun 10 2020 at 13:44):

Also, every theorem about bool can be proven by dec_trivial

#### Patrick Massot (Jun 10 2020 at 13:44):

by \neg you mean \not, right?

yes

they both work

#### Mario Carneiro (Jun 10 2020 at 13:46):

it's also the actual LaTeX AFAIR so that's what my fingers know

#### Patrick Massot (Jun 10 2020 at 13:48):

Oh I see, they both triggered the same unicode translation. I though that you were saying -tt works.

#### Patrick Massot (Jun 10 2020 at 13:49):

It's a bit unfortunate since neg is lemma names means something completely different.

#### Mario Carneiro (Jun 10 2020 at 13:51):

why would you need a unicode hotkey for -?

#### Mario Carneiro (Jun 10 2020 at 13:51):

unless you are on a non-english keyboard that makes - hard to hit

No idea.

#### Patrick Massot (Jun 10 2020 at 13:56):

Why would you need a unicode hotkey for \not that would be anything other than \not or \non

#### Mario Carneiro (Jun 10 2020 at 13:59):

vscode says I could just use \n

#### Mario Carneiro (Jun 10 2020 at 13:59):

which neatly avoids the abbreviation question

Last updated: May 14 2021 at 00:42 UTC