Syntax about dot in typeclass?

Stream: new members

[Shanghe Chen]

Hi recently I found some syntax about dot in typeclass but cannot find references for this:

set_option autoImplicit false

class A where
  a : Int

class D where
  a : Int

variable [A]
variable [D]

class A.B : Prop where
  b : a==1

#check A.B.b

[Mario Carneiro]

This is the same as dot in any declaration, it is namespacing the definition

[Shanghe Chen]

The above code only works with A.B but not something like

class C.B : Prop where
  b : a==1

Is there some convention here?

[Mario Carneiro]

def Foo.bar : Nat := 1

is the same as

namespace Foo
def bar : Nat := 1
end Foo

[Mario Carneiro]

the reason it doesn't work with C.B is because entering namespace A means that you can refer to A.a unqualified

[Mario Carneiro]

It will work if you do

class C.B : Prop where
  b : A.a==1

[Shanghe Chen]

Oh it is very clear now. Once I thought it maybe some syntax sugar for class B extends A hahaha. Thank you very much Mario:tada: