使用视图时语法错误
使用视图时语法错误
提问于 2014-08-09 08:58:42
我有以下代码(主要是通过在emacs中使用idris模式自动生成的)：
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 (C)时，我会得到以下错误消息：
- + 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回答 1
Stack Overflow用户
回答已采纳
发布于 2014-08-09 09:07:44
不是你做错了什么，而是伊德里斯！之后的事情？需要是一个有效的标识符，所以如果用类似于?(plus_1 n n)_rhs的东西替换?plus_1_n_n_rhs，应该可以。
这是Idris中的一个bug，但不是我以前见过的，也不是我可以轻松复制的--当我试图构建它时，它会生成合理的名称。如果您可以将复制步骤发布到https://github.com/idris-lang/Idris-dev/issues的问题跟踪器，那么我将对其进行调查！
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/25216905
复制相关文章
相似问题
腾讯云开发者
