what does a . in a def's declId really do?

Stream: new members

[JJ]

I ran into the following unexpected-to-me behavior:

inductive Foo where
| Unit

-- type mismatch: argument Unit has type Foo : Type but expected Type α : Type (α + 1)
def Foo.foo : Option Unit := ()

I would have expected Unit to be resolved as the Unit in the prelude, not Foo.Unit. Clearly, there's something up with the Foo. prefix on the def that I didn't know about -- I thought it was just a namespacing sorta thing, but that seems to not be the case. What is up here with the declId and what does my code currently do? I went hunting in the reference, but could not find it documented.

(It's probably there and I'm just missing it, but it's a bit hard to search for.)

[Henrik Böving]

It does just do nanespacing, that's why the error happens. Within the deck you are in the Foo namespace so unit resolves as you observe

[Kenny Lau]

@JJ well, arguably there's a "bad practice" in the code, which is using capital letter for terms

[JJ]

Ah, but these are types :-D
(this is part of a dependent typechecker)

[JJ]

Henrik Böving said:

It does just do nanespacing, that's why the error happens. Within the deck you are in the Foo namespace so unit resolves as you observe

Interesting, huh, weird. So there's an implicit open Foo or something?

[Kenny Lau]

yeah

[Henrik Böving]

JJ said:

Henrik Böving said:

It does just do nanespacing, that's why the error happens. Within the deck you are in the Foo namespace so unit resolves as you observe

Interesting, huh, weird. So there's an implicit open Foo or something?

Almost, the syntax

def Foo.bar ...

simply desugars to

namespace Foo

def bar ...

end Foo

[JJ]

Hm, okay, I see. I was unaware that namespace T opened the terms of the constructors of T, but that makes sense.