Zulip Chat Archive

Stream: general

Topic: open_locale scoping


view this post on Zulip Reid Barton (Oct 08 2019 at 22:34):

If open_locale appears inside a section/namespace, are its effects scoped to that section/namespace?

view this post on Zulip Floris van Doorn (Oct 09 2019 at 01:04):

Yes, it has the same effect as writing

local notation ...
local attribute ...

in that spot

view this post on Zulip Simon Hudon (Oct 09 2019 at 02:24):

How did you manage that?

view this post on Zulip Simon Hudon (Oct 09 2019 at 02:24):

Oh, I see, nevermind :P

view this post on Zulip Floris van Doorn (Oct 09 2019 at 17:40):

for others wondering the same: it's calling emit_code_here to run exactly those commands.


Last updated: May 09 2021 at 20:11 UTC