Zulip Chat Archive
Stream: PR reviews
Topic: mathlib4#804 Order.Hom.Basic
Scott Morrison (Dec 06 2022 at 01:39):
This is ready for review, and I think is the current bottleneck on the port.
Gabriel Ebner (Dec 06 2022 at 02:07):
There's still linting errors.
Scott Morrison (Dec 06 2022 at 02:49):
Fixed
Last updated: May 02 2025 at 03:31 UTC