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

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

最佳答案

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

open import Algebra
open import Data.Nat.Properties

open CommutativeSemiring commutativeSemiring

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

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

关于agda - 如何在 agda 中使用 nat 属性，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/22342848/