Zulip Chat Archive

Stream: lean4

Topic: Extending structure, problem with `this`


Tomas Skrivan (Oct 04 2022 at 18:14):

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 (Oct 04 2022 at 18:16):

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 (Oct 04 2022 at 19:00):

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


Last updated: Dec 20 2023 at 11:08 UTC