Definitions that are only valid in certain sections.

Stream: Is there code for X?

[Asei Inoue]

section

-- definition in a section.
-- Could the code be rewritten so that the name is only valid within a section?
abbrev longLongName := Nat

end

-- test code. this code should success
#check_failure longLongName

[Yaël Dillies]

Have you thought of using namespaces?

[Yaël Dillies]

Or private?

[Asei Inoue]

This also fails....

namespace Sample

-- definition in a section.
-- Could the code be rewritten so that the name is only valid within a section?
private abbrev anotherNat := Nat

#check Sample.anotherNat

end Sample

-- test code. this code should success
#check_failure Sample.anotherNat

[Yaël Dillies]

It doesn't fail once you go to a different file

[Asei Inoue]

Is it possible to disable the section or namespace instead of the file?