failed to synthesize BEq

Stream: new members

[Benjamin]

I'm trying to run the following code:

def Sequence := List Int
def is_empty (a : Sequence) : Bool := a == []

I get an error saying "failed to synthesize BEq Sequence". This is strange, because the error goes away if I replace Sequence by its definition. How can I fix this?

[Kyle Miller]

Unless you want Sequence to have its own typeclass instances, you can do abbrev Sequence := List Int to make the definition become transparent for the purpose of typeclass inference.

[Benjamin]

Thanks. And if I wanted Sequence to have its own type class instances, what would I do?

[Eric Wieser]

You would define your own type class instance for BEq

[Kyle Miller]

Option 1: "delta deriving"

def Sequence := List Int
deriving BEq

def is_empty (a : Sequence) : Bool := a == []

Option 2: manually unfolding

def Sequence := List Int

instance : BEq Sequence := inferInstanceAs <| BEq (List Int)

def is_empty (a : Sequence) : Bool := a == []

The first is preferable, but it can be useful to know how to do the second.