agda - 如何在 agda 中使用 nat 属性

Question

在 agda 中有一个模块 Data.Nat.Properties。它包含许多有用的事实，这些事实隐藏在记录中，例如，isCommutativeSemiring。例如，我如何提取 * 关联性并使用它？

Answer 1

打开有问题的模块。例如:

open import Algebra
open import Data.Nat.Properties

open CommutativeSemiring commutativeSemiring

-- now you can use *-assoc, *-comm, etc.

如果您想浏览模块的内容，请尝试 C-c C-o 组合键，因为代数结构的递归打开和重新导出使得很难看到可用的内容。