普通の再帰的なデータ型のインターフェイスを実装する

Question

私はIdrisの構文と戦っているようです。

module Test 

data Nat = Z | S Nat 

Eq Nat where 
    Z == Z = True 
    S n1 == S n2 = n1 == n2 
    _ == _ = False 

これは、次のエラー（V1.1.1）で文句を言う：

.\.\Test.idr:5:8: error: expected: "@", 
    "with", argument expression, 
    constraint argument, 
    function right hand side, 
    implicit function argument, 
    with pattern 
Eq Nat where 
    ^
Type checking .\.\Test.idr 

私は基本的にドキュメントと同じ構文を使用し、なぜ、私は理解していません。

のようなカスタム非再帰型のEq実装を書くと、うまくコンパイルされます。

Answer 1

括弧内にS nパターンを囲む必要があります。その後、Natが既にPreludeに定義されているため、コンパイラエラーが発生します。コードをコンパイルするには、NatをNatural（または他のもの）に置き換えてください。しかし、ZとSのコンストラクタもPreludeに定義されていますので、REPLで簡単にテストできるようにすべての名前を変更するか、%hide directiveを使用する必要があります。

しかし、少なくとも、このコードはコンパイルされます。

module Test 

data Natural = Z | S Natural 

Eq Natural where 
    Z == Z = True 
    (S n1) == (S n2) = n1 == n2 
    _ == _ = False