mathlib4#511

Stream: mathlib4

[Scott Morrison]

I've started a port of Logic.Function.Basic at mathlib4#511. Please consider this a "please jump in and fix stuff" PR.

So far I've done the merge with the existing file, using previously ported proofs where the mathport proof is broken.

But I haven't attempted to

• fix the remaining broken proofs
• rename statements as appropriate (with #aligns)
• edit for style

[Kevin Buzzard]

I have ported all of data.bool.basic and the only jobs left are to #align everything and to add Yury's recent changes to the lean 3 file. I need to promise myself to do this before I start on the fun of jumping in!

[Jakob von Raumer]

Ah, I should look at the PR list instead of only at the wiki file before I start work on a file :rolling_eyes: Anyways, I created mathlib4#516 before I read your message, will see if I can contribute to yours.

[Scott Morrison]

@Jakob von Raumer, sorry about that, I should have edited the wiki. :-(