------------------------------------------------------------------------
-- Finite sets
------------------------------------------------------------------------

module Tools.Fin where

open import Data.Fin.Properties using () renaming (_≟_ to _≟ⱽ_) public
open import Data.Fin.Base using (Fin) renaming (zero to x0 ; suc to _+1) public

open import Tools.Nat

private variable
  n : Nat

-- One.

x1 : Fin (2 + n)
x1 = x0 +1

-- Two.

x2 : Fin (3 + n)
x2 = x1 +1

-- Three.

x3 : Fin (4 + n)
x3 = x2 +1

-- Four.

x4 : Fin (5 + n)
x4 = x3 +1

-- Five.

x5 : Fin (6 + n)
x5 = x4 +1

-- Six.

x6 : Fin (7 + n)
x6 = x5 +1