在阿格达中为假设添加定义

Question

从一个仅将类型定义为假设的 Agda 模块开始

module M where 
postulate 
U : Set 

我希望能够以不同的方式定义U。例如：

module B where 
open M public 
-- define U as Bool 

和

module N where 
open M public 
-- define U as Nat 

有没有办法在阿格达做到这一点？

Answer 1

AFAIK，你不能，假设是抽象的。

您可以通过颠倒顺序来实现您想要的：而不是像您那样尝试在module B或N中定义U，而是

module M (U : Set) where

然后你实例化UBool或Nat.