Problem deriving LawfulBEq

Stream: new members

[aron]

I have this type defined:

structure UnificationVar where
  index : Nat
  deriving BEq, Hashable, LawfulBEq

but there's an error for LawfulBEq: default handlers have not been implemented yet, class: 'LawfulBEq' types: [UnificationVar]

What does this error mean and how can I fix it?

[Aaron Liu]

If you just do deriving DecidableEq then both BEq and LawfulBEq are available by typeclass synthesis.

[aron]

ah nice, that worked! thanks!

[aron]

but could you still help me understand what the original error means?

[Aaron Liu]

default handlers have not been implemented yet probably means no one has told Lean what to do when it encounters deriving LawfulBEq.

[Kyle Miller]

BEq tends to be misleading to new users. I can't think of any reason you wouldn't want DecidableEq instead of BEq + LawfulBEq. There are some tricky problems you can get into too if you have all three defined.