error: 'Id' has already been declared

Stream: lean4

[Yuri de Wit]

I have created a structure named 'Id' in a plain project I created with lake new, but got 'Id' has already been declared out of the bat. It is obvious why this is happening and it is easy enough to work around.

However, I am wondering:

• is there a way to hide a namespace or a specific identifier,
• Should Init.Core be imported automatically in all files?

[Horatiu Cheval]

You can use namespace Hidden for this.

namespace Hidden

  def Id := 37

end Hidden

[Horatiu Cheval]

That's for the first point. For the second, I think starting a file with prelude prevents the import

prelude

#check Id
/-
unknown identifier 'Id'
-/

[Kevin Buzzard]

I think that whenever someone points out that starting a file with prelude solves a certain problem, it should also be pointed out that starting a file with prelude causes all sorts of other problems (eg probably you can't import most things now)

[Yuri de Wit]

Horatiu Cheval said:

You can use namespace Hidden for this.

Nice to know, thanks! But it does feel like another workaround.

[Yuri de Wit]

Maybe tangentially related is the ability to qualify imports or selectively import, which I think has been discussed here in the past.