-- | Finite totally-ordered sets
module Data.Fin (Fin (..), enum, inj₁, proj₁, lift₁, fromFin, toFin, toFinMay, pred) where

import Prelude ()
import Data.Maybe (Maybe (..))
import Data.Fin.Private
import qualified Data.Peano as P

pred :: Fin (P.Succ n) -> Maybe (Fin n)
pred :: Fin ('Succ n) -> Maybe (Fin n)
pred = \ case
    Zero -> Maybe (Fin n)
forall a. Maybe a
Nothing
    Succ n :: Fin n
n -> Fin n -> Maybe (Fin n)
forall a. a -> Maybe a
Just Fin n
n