mathlib4#550

Stream: PR reviews

[Scott Morrison]

The port of logic.equiv.defs is ready for review. It's part of the longest unported chain, and there are several PRs waiting on it, so it should be a priority.

[Yakov Pechersky]

What's the '?' commit about?

[Scott Morrison]

Sorry, left that in a weird state. I am getting PANICs from Lean 4 at that commit. Just reporting now.

[Scott Morrison]

https://github.com/leanprover/lean4/issues/1822