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