Zulip Chat Archive
Stream: general
Topic: docs#equiv.empty
Yaël Dillies (Apr 07 2023 at 12:14):
I just stumbled upon docs#equiv.empty, docs#equiv.empty_to_equiv. Those are very general names to drop in the root namespace. @Aaron Anderson, thoughts?
Aaron Anderson (Apr 07 2023 at 12:55):
Perhaps it should be equiv.empty_language?
Yaël Dillies (Apr 07 2023 at 12:56):
That sounds better, yeah
Eric Wieser (Apr 07 2023 at 13:19):
Or first_order.language.empty.equiv.of_equiv?
Last updated: Dec 20 2023 at 11:08 UTC