beginner equality question

Stream: general

[dan pittman]

I'm attempting to assert whether two elements of a list are equal, and then act on that assertion in an if-then-else manner, but for my x = y assertion, there is no decidable instance. Perhaps there's a different approach I ought to be taking?

[Chris Hughes]

Using the line local attribute [instance] classical.prop_decidable should help, but it will stop your functions being computable. What type do x and y have? You could also make [decidable_eq α] an argument to your function, if it's defined on an arbitrary type.

[dan pittman]

Thanks! decidable_eq is what I was looking for! I'd written this in Haskell first, and was of course using Eq a => ....