Zulip Chat Archive
Stream: new members
Topic: private abbreviation
Alex Zhang (Jul 08 2021 at 08:33):
Is it possible to restrict an abbreviation into a section?
section test
private abbreviation S :set ℤ := {-1, 1, 0}
end test
section two
private abbreviation S :set ℤ := {-1, 1}
--#check S
end two
This check reports overload.
Johan Commelin (Jul 08 2021 at 08:35):
Use namespace instead of section
Last updated: Dec 20 2023 at 11:08 UTC