如何在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.

如果要浏览模块的内容,请尝试使用Cc Co组合键,因为代数结构的递归打开和重新导出使得很难看到可用的内容.