Zulip Chat Archive

Stream: Is there code for X?

Topic: implication on `bool`


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

view this post on Zulip Johan Commelin (Sep 15 2020 at 14:03):

If it exists, it must be bimp, right?

view this post on Zulip Kevin Buzzard (Sep 15 2020 at 14:44):

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

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

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