Fin.lagda.md

```agda
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`].

[`Data.Fin.Base`]: Data.Fin.Base.html
[`Data.Fin.Properties`]: Data.Fin.Properties.html