Zulip Chat Archive
Stream: mathlib4
Topic: !4#2438 higher_order attribute
Chris Hughes (Mar 07 2023 at 17:49):
Can someone who understands tactics better than me review this. A lot of PRs depend on it.
Kyle Miller (Mar 08 2023 at 13:23):
@Chris Hughes It's merged now
Last updated: May 02 2025 at 03:31 UTC