Zulip Chat Archive

Stream: maths

Topic: localization


view this post on Zulip Johan Commelin (Mar 05 2019 at 08:58):

Currently we have

def loc := quotient $ localization.setoid α S

and the namespace is called localization. Should we change this so that both are called loc or both are called localization?

view this post on Zulip Johan Commelin (Mar 05 2019 at 08:58):

I don't think it will matter too much for projection notation (in this particular use case).

view this post on Zulip Patrick Massot (Mar 05 2019 at 08:59):

I vote for localization. You can still define an abbreviation (or even a local notation) in files where this is used a lot


Last updated: May 12 2021 at 08:14 UTC