make instance of decidable_eq

Stream: new members

[Patrick Thomas]

How does one make a type an instance of decidable_eq? For example, this type:

inductive term : Type
| var : string → term
| func : string → list term → term

[Patrick Thomas]

This does not seem to work:

@[derive decidable_eq] inductive term : Type
| var : string → term
| func : string → list term → term

[Kevin Buzzard]

You can look at how it's done for nat in the source code. Basically you have to write your own algorithm and prove it works

[Mario Carneiro]

The reason is because the derive handler for decidable_eq doesn't handle nested inductives

[Kevin Buzzard]

Does string have decidable_eq? If not then that's the problem

[Mario Carneiro]

it does

[Kevin Buzzard]

Ok then what Mario says is the problem :-)