Fin-0.1.0.0: Data/Fin.hs

{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}

module Data.Fin where

import Data.Peano (Peano)
import qualified Data.Peano as P

data Fin :: Peano -> * where
    Zero :: Fin (P.Succ n)
    Succ :: Fin n -> Fin (P.Succ n)