porting data.bool.basic

Stream: mathlib4

[Kevin Buzzard]

I would like to claim data.bool.basic, which I will try to port over the next 24 hours. I am still a little confused about how this works. @Jakob von Raumer pointed me to https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status but this file says I should only change "no" to "yes" when the file is completely ported. @Scott Morrison mentioned announcing that I wanted to claim the port of this file in some thread in the mathlib4 stream but I can't find the thread. Do we not yet have a system? Anyway, I'm porting data.bool.basic on the tube home.

[Scott Morrison]

The status must begin with Yes or No, but you can write something after that. So No: WIP Kevin Buzzard is fine.

[Scott Morrison]

After someone merges #17056, when you run scripts/port_status.py this extra information will show up in the list.