Zulip Chat Archive

Stream: general

Topic: simplicial set locale


view this post on Zulip Ashwin Iyengar (Mar 23 2021 at 18:30):

The following gives me a strange error

import algebraic_topology.simplicial_set
open_locale simplicial

about how it doesn't know what horn is. Also, the top of simplicial_set.lean says that you can access notation viaopen_locale sSet, but this locale doesn't seem to exist.

view this post on Zulip Johan Commelin (Mar 23 2021 at 18:33):

I think the sSet locale was recently merged into simplicial, which means we should update that docstring.
And probably the notation for horn isn't using a fully qualified name.
So it says

localized "... := horn" in simplicial
-- instead of
localized "... := simplicial_object.horn" in simplicial

or something like that.

view this post on Zulip Alex J. Best (Mar 23 2021 at 18:33):

import algebraic_topology.simplicial_set
open sSet
open category_theory
open_locale simplicial

works for now

view this post on Zulip Ashwin Iyengar (Mar 23 2021 at 18:34):

Ah thanks, that makes sense

view this post on Zulip Johan Commelin (Mar 23 2021 at 18:34):

Feel free to PR a fix

view this post on Zulip Ashwin Iyengar (Mar 23 2021 at 18:37):

If I PR a fix, should I change the localized lines to fully qualified names so that we don't need the opens?

view this post on Zulip Ashwin Iyengar (Mar 23 2021 at 18:38):

So that

import algebraic_topology.simplicial_set
open_locale simplicial

works, or is @Alex J. Best 's suggestion the thing to use?

view this post on Zulip Johan Commelin (Mar 23 2021 at 18:40):

@Ashwin Iyengar No, it's better if it works without open

view this post on Zulip Johan Commelin (Mar 23 2021 at 18:40):

So please use FQNs

view this post on Zulip Ashwin Iyengar (Mar 23 2021 at 18:48):

Ok this is done in #6838

view this post on Zulip Scott Morrison (Mar 23 2021 at 21:45):

Is this something that we could lint? Create a file with no open namespaces, that opens all the locales? (Perhaps locales are not guaranteed to be compatible in the same file.)


Last updated: May 08 2021 at 09:11 UTC