导入的数据类型与本地定义的数据类型冲突，即使重命名也是如此
导入的数据类型与本地定义的数据类型冲突，即使重命名也是如此
提问于 2013-04-23 22:14:43
使用下面的Agda代码，我在A₂中得到了一个关于B定义的错误：
module Whatever where
module A₁ where
data B : Set where
module A₂ where
open A₁ renaming (B to B₁)
data B : Set where错误消息为：
Duplicate definition of module B. Previous definition of datatype
module B at /home/cactus/prog/agda/modules.agda:4,8-9
when scope checking the declaration
data B where但是我在导入上将B重命名为B₁，为什么它仍然冲突？有什么办法可以绕过它吗？
回答 2
Stack Overflow用户
回答已采纳
发布于 2013-04-24 11:27:36
问题是数据类型定义了一个模块和一个名称。您还需要重命名模块。这是可行的：
module Cactus where
module A₁ where
data B : Set where
module A₂ where
open A₁ renaming (B to B₁; module B to B₁)
data B : Set where这允许你以一种模块化的方式引用构造函数，所以如果你在Level.suc和你的ℕ之间有冲突，你可以只编写ℕ.suc并让它工作，而不需要通过重命名恶作剧。
Stack Overflow用户
发布于 2013-04-24 00:26:42
对我来说，这似乎是Agda的一个bug。您可以在http://code.google.com/p/agda/issues/list中报告该错误。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/16171670
复制相关文章
相似问题
腾讯云开发者
