How to use nat properties in agda

Question

In agda there's a module Data.Nat.Properties. It contains a lot of useful facts, which are hidden inside of records, for example, isCommutativeSemiring. How can I extract, for example * associativity and use it?

Answer 1

Open the modules in question. For example:

open import Algebra
open import Data.Nat.Properties

open CommutativeSemiring commutativeSemiring

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

If you want to browse the contents of a module, try the C-c C-o key combination, since the recursive opening and re-exporting of algebraic structures makes it hard to see what's available.