局部進口數據類型的衝突定義一個，甚至改名

Question

用下面的阿格達代碼的時候，我在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₁，那麼爲何仍發生衝突？有沒有辦法解決它？

Answer 1

的問題是，數據類型定義模塊和一個名稱。您還需要重命名模塊。這工作：

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並將它，而不必去上班通過重命名詭計。

Answer 2

這好像是個錯誤阿格達我。您可以在http://code.google.com/p/agda/issues/list報告的bug。