simplicial set locale

Stream: general

[Ashwin Iyengar]

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.

[Johan Commelin]

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.

[Alex J. Best]

import algebraic_topology.simplicial_set
open sSet
open category_theory
open_locale simplicial

works for now

[Ashwin Iyengar]

Ah thanks, that makes sense

[Johan Commelin]

Feel free to PR a fix

[Ashwin Iyengar]

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

[Ashwin Iyengar]

So that

import algebraic_topology.simplicial_set
open_locale simplicial

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

[Johan Commelin]

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

[Johan Commelin]

So please use FQNs

[Ashwin Iyengar]

Ok this is done in #6838

[Scott Morrison]

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.)