Zulip Chat Archive
Stream: mathlib4
Topic: multifile PRs
Jireh Loreaux (Nov 18 2022 at 21:59):
How do we feel about porting multiple files in one go? I have mathlib#641 open for data.nat.cast.defs, but I have data.int.cast.defs ready now too. Is it okay if I just combine them into mathlib#641, or should I make a separate PR?
Moritz Doll (Nov 18 2022 at 22:02):
This is totally fine.
Scott Morrison (Nov 19 2022 at 00:37):
Yes, please!
Last updated: Dec 20 2023 at 11:08 UTC