## Stream: Is there code for X?

### Topic: implication on bool

#### Kevin Buzzard (Sep 15 2020 at 14:02):

I am apparently going to tell my students that the truth table for boolean implication P -> Q is Q or not P. Is this function (on bool) in Lean? #find bool → bool → bool  doesn't seem to give it me (and does give me band, bor and bxor). Is implication not a thing in bool?

#### Johan Commelin (Sep 15 2020 at 14:03):

If it exists, it must be bimp, right?

#### Kevin Buzzard (Sep 15 2020 at 14:44):

Are you just saying that to make me type #check bimp?

#### Johan Commelin (Sep 15 2020 at 14:48):

Not really, but I think bimp is a funny name. I wonder what beep should do. Also, I would love to hear the bxor band. That must be some digital techno punk.

#### Kevin Buzzard (Sep 15 2020 at 14:49):

yeah my daughter has a few vinyls by them

Last updated: May 16 2021 at 05:21 UTC