legal namespace usage

Stream: new members

[Quinn]

namespace Real
  variable (T : Type)
end Real
#check Real.T

I can't get past "unknown identifier: Real.T".

[Ruben Van de Velde]

What do you think that would do? What are you trying to do?

[Quinn]

it seems like #check Real.T should just be Type

[Quinn]

cuz for the namespace's context that's what it is

[Kevin Buzzard]

Either the variable dies when you close the namespace or it stays being called T

[Quinn]

namespace Real
  variable (T : Type)
end Real
open Real
#check T

(also fails) i'm confused why i'm able to open a namespace without supplying values for the variables declared

[Eric Wieser]

namespaces are for declarations, not variables

[Kyle Miller]

If you're following Mathematics in Lean, this chapter mentions variable: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

[Kyle Miller]

It's for declaring parameters to definitions and theorems for the rest of the section. (They get removed from the definition or theorem if they are not used.) They are not definitions or theorems themselves.

[Kyle Miller]

If you want something in the Real namespace, you have to make definition or theorem.

namespace Real
def T := Type
end Real
#check Real.T
-- Real.T : Type 1

[Quinn]

great explanation thanks!

[Mario Carneiro]

Quinn said:

namespace Real
  variable (T : Type)
end Real
open Real
#check T

(also fails) i'm confused why i'm able to open a namespace without supplying values for the variables declared

It sounds like you are thinking of modules in the style of Coq or ML. Lean does not have a module system in this sense, so variable declarations have local effect only and theorems using them are generalized immediately after the definition, not at the end of the section. Once the section or namespace is closed or you go to a new file, the variable is completely gone and has no lasting effect.