Extending structure, problem with `this`

Stream: lean4

[Tomas Skrivan]

When extending a structure, I'm having a trouble that this is not transparent enough.

  structure A where
    type : Type

  structure B extends A where
    foo : A.type this → Nat

  def b : B :=
    B.mk (A.mk Nat) (λ n => n) -- type mismatch

The error is:

type mismatch
  n
has type
  this.type : Type
but is expected to have type
  ℕ : Type

In that context this is just some A and not A.mk Nat.

What is the intended way to define b ?

[Marcus Rossel]

What is this supposed to be? Do you happen to mean toA?

If I assume the meaning of your code correctly, you can also just write:

structure B extends A where
  foo : type → Nat

[Tomas Skrivan]

:face_palm: yes toA is what I want. Im just too used to object oriented programming and its this