Zulip Chat Archive
Stream: std4
Topic: New alias syntax
François G. Dorais (Jul 31 2023 at 13:32):
The new alias syntax originally proposed by @Mario Carneiro is ready for review at std4#200! There is also a companion Mathlib patch at #6172.
Last updated: Dec 20 2023 at 11:08 UTC