invalid field notation

Stream: lean4

[Kevin Buzzard]

def cardinal.setoid : Setoid Type := sorry

def cardinal := Quotient cardinal.setoid -- invalid field notation

def cardinal2 := Quotient cardinal.setoid -- works fine

Is this expected? I think this is a natural way to define cardinal but if the setoid needs to go in another namespace then so be it.

[Daniel Selsam]

Kevin Buzzard said:

Is this expected? I think this is a natural way to define cardinal but if the setoid needs to go in another namespace then so be it.

Currently, you cannot refer to a name that is inside the namespace of a local variable, i.e.:

abbrev Foo.bar : Type := Nat
#check Foo.bar -- works
#check fun (Foo : Unit) => Foo.bar -- fails

I am not sure if there is a reason for this limitation or if it is just an oversight. Note that as a workaround, you could write either:

def cardinal := Quotient _root_.cardinal.setoid
def cardinal := by clear cardinal; exact cardinal.setoid