如何在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鍵的組合，由於循環開啓和再出口的代數結構使得它很難看到有什麼可用。