module Data.Fin where open import Data.Fin.Base public open import Data.Fin.Properties public
Finite Sets - Index🔗
The natural numbers are constructed in the module Data.Fin.Base
. Their arithmetical properties are proved in Data.Fin.Properties
.