1

私は次のコードを持っています (ほとんどの場合、emacs で idris-mode を使用して自動生成されます):

module Main

data Parity : Nat -> Type where
  even : (n : Nat) -> Parity (n + n)
  odd : (n : Nat) -> Parity (S (n + n))

parity : (n : Nat) -> Parity n
parity Z = ?parity_rhs_1
parity (S Z) = ?parity_rhs_3
parity (S (S k)) with (parity k)
  parity (S (S (plus n n))) | (even n) = ?(plus_1 n n)_rhs
  parity (S (S (S (plus n n)))) | (odd n) = ?(S_2 (plus n n))_rhs

---------- Proofs ----------
Main.parity_rhs_3 = proof
  exact (odd 0)

Main.parity_rhs_1 = proof
  exact (even 0)

ファイルを REPL (Cc Cl) にロードしようとすると、次のエラー メッセージが表示されます。

- + Errors (1)
 `-- ./Main.idr line 11 col 3:
      error: expected: "{",
         function declaration
       parity (S (S (plus n n))) | (even n) = ?(plus_1 n n)_rhs
       ^

私は何か間違ったことをしていると思いますが、何がわかりません。

$ idris --version
0.9.14.1-git:c6574b4
4

1 に答える 1

1

間違ったことをしたのはあなたではなく、イドリスです! ? の後のこと 有効な識別子である必要があるため?(plus_1 n n)_rhs、次のようなものに置き換えれば?plus_1_n_n_rhs問題ありません。

これは Idris のバグですが、これまでに見たことがない、または簡単に再現できるバグです。これをビルドしようとすると、適切な名前が生成されます。再現する手順をhttps://github.com/idris-lang/Idris-dev/issuesのイシュー トラッカーに投稿していただければ、調査いたします。

于 2014-08-09T09:07:44.673 に答える