Data.Fin

1Lab
  • Finite sets - index🔗
This page was written by Amélia Liao and Reed Mullanix

back to index 
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.