Zulip Chat Archive
Stream: PR reviews
Topic: mathlib4/433
Scott Morrison (Oct 07 2022 at 04:37):
Could I have https://github.com/leanprover-community/mathlib4/pull/433 reviewed/merged? I'd like to finish off porting fin_cases
and this will be helpful.
Last updated: Dec 20 2023 at 11:08 UTC