CODEWITHSUNDEEP
agda
Konstantin Solomatov
Konstantin Solomatov

Reputation: 10352

How to use nat properties in agda

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?

Upvotes: 3

Views: 287

Answers (1)

Mysterious Dan
Mysterious Dan

Reputation: 1326

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.

Upvotes: 6

Related Questions