private abbreviation

Stream: new members

[Alex Zhang]

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]

Use namespace instead of section