在 Agda 中为假设添加定义

【问题标题】：Adding Definitions to Postulates in Agda在 Agda 中为假设添加定义
【发布时间】：2019-10-01 15:00:01
【问题描述】：

从只将类型定义为假设的 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

有没有办法在 Agda 中做到这一点？

【问题讨论】：

标签： module agda

【解决方案1】：

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

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

module M (U : Set) where

然后将U 实例化为Bool 或Nat。

【讨论】：