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
bxor). Is implication not a thing in bool?
Johan Commelin (Sep 15 2020 at 14:03):
If it exists, it must be
Kevin Buzzard (Sep 15 2020 at 14:44):
Are you just saying that to make me type
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
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