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 回答