implication on `bool`

Stream: Is there code for X?

[Kevin Buzzard]

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]

If it exists, it must be bimp, right?

[Kevin Buzzard]

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

[Johan Commelin]

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]

yeah my daughter has a few vinyls by them