------------------------------------------------------------------------
-- The Agda standard library
--
-- Instances for finite sets
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Fin.Instances where

open import Data.Fin.Base using (Fin)
open import Data.Fin.Properties using (≡-isDecEquivalence; ≤-isDecTotalOrder)

instance
  Fin-≡-isDecEquivalence = ≡-isDecEquivalence
  Fin-≤-isDecTotalOrder = ≤-isDecTotalOrder