types - Idris - 枚举类型的 Eq

Question

假设我有一个枚举类型，例如

data MyType
    = One
    | Two
    | Three
    ...
    | Ten

我想为其实现 Eq 接口(interface)。我可以这样做

Eq MyType where
    One == One = True
    Two == Two = True
    ...
    Ten == Ten = True
    _ == _ = False

但这看起来很乏味。

在 Idris 中是否有更好、更巧合的方法来做到这一点？

Answer 1

您正在寻找 Idris 的实例/实现派生。

有一个“派生所有实例”项目，其中似乎有 working solution for Eq (请参阅文件末尾的示例)。但是，将来可能不会维护它。有a newer project in the works它也跨越了 Eq，但仍然需要完成。