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.