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