Idris - 枚举类型的Eq

Question

假设我有一个枚举类型

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

我想Eq为它实现接口.我可以这样做

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

但这看起来很单调乏味.

在伊德里斯这样做有更好,更巧合的方法吗？

Answer 1

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

有一个“派生所有实例”项目，该项目似乎为Eq提供了一个可行的解决方案（请参阅文件末尾的示例）。但是，将来可能不会维护它。工作中还有一个较新的项目，也涉及Eq，但仍需完成。