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: Dec 20 2023 at 11:08 UTC