Zulip Chat Archive

Stream: general

Topic: localized notation


view this post on Zulip Jesse Michael Han (Jul 25 2019 at 15:16):

@Floris van Doorn what are the differences between the local and localized keywords? is the main feature being able to re-introduce localized things into the environment of a separate section?

view this post on Zulip Rob Lewis (Jul 25 2019 at 15:23):

Yes, that's the idea. localized basically stores local notation and attribute commands, and gives a convenient way to replay these commands.

view this post on Zulip Kevin Buzzard (Jul 25 2019 at 20:07):

Where is localized documented? I've never heard of it

view this post on Zulip Jesse Michael Han (Jul 25 2019 at 20:46):

it's at the bottom of tactics.md

view this post on Zulip Keeley Hoek (Jul 26 2019 at 02:38):

I just had the thought that perhaps Simon's "open all the parser namespaces" tactic could be unified into localized


Last updated: May 12 2021 at 22:15 UTC