Use local instance

Stream: lean4

[Marcus Rossel]

In the following setting, the HashMap a.type Nat declaration fails because failed to synthesize instance BEq a.type:

structure A where
  type : Type
  [beq : BEq a]
  [hashable : Hashable a]

structure B where
  a : A
  map : HashMap a.type Nat

What I'm trying to express in A is that type is some type which is equatable and hashable. Is this the right approach? If so, how do I make use of the local instances later on?

[Gabriel Ebner]

You're running into two issues here.

[Gabriel Ebner]

1) You need to write BEq type instead of BEq a. [beq : BEq a] means [beq : ∀ {a}, BEq a].

[Gabriel Ebner]

2) You need to mark A.beq and A.hashable as instances.

[Gabriel Ebner]

and 0) you need to import Std and open Std #mwe

[Gabriel Ebner]

import Std

structure A where
  type : Type
  [beq : BEq type]
  [hashable : Hashable type]

attribute [instance] A.beq A.hashable

structure B where
  a : A
  map : Std.HashMap a.type Nat

[Marcus Rossel]

Gabriel Ebner said:

You need to write BEq type instead of BEq a

Sorry, that was just bad copy paste.

[Marcus Rossel]

Thanks!