Typeclass synonyms

Stream: lean4

[Andrea Laretto]

I'd like to define a custom typeclass which is just a "more instantiated" case of another typeclass:

class Foo (A : Type) where
  val : A
open Foo

def Bar := Foo Int

Note that this seems to be perfectly valid:

instance : Bar where
  val := 3

However, in this case inferInstance fails

def Example : Bar := inferInstance

giving as error type class instance expected\nBar, suggesting to me that Bar isn't viewed as typeclass although definitionally equal to one. Is there any way to solve this and let inference go through?

[Eric Wieser]

Try using abbrev instead of def

[Andrea Laretto]

Nice, that works, thanks! Is abbrev just like def with some additional reducibility? I tried @[inline] with def but thst still didn't work. Would be nice to have some other examples where one cannot get anywhere without abbrev

[Alex J. Best]

abbrev is quite close to being @[reducible] def indeed. Inline on the other hand is only useful for programming and getting efficient code from the compiler, not for typeclass inference