{-# LANGUAGE CPP                  #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE EmptyCase            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE Safe                 #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
-- | Finite numbers.
--
-- This module is designed to be imported as
--
-- @
-- import Data.Fin (Fin (..))
-- import qualified Data.Fin as Fin
-- @
--
module Data.Fin (
    Fin (..),
    cata,
    -- * Showing
    explicitShow,
    explicitShowsPrec,
    -- * Conversions
    toNat,
    fromNat,
    toNatural,
    toInteger,
    -- * Interesting
    mirror,
    inverse,
    universe,
    inlineUniverse,
    universe1,
    inlineUniverse1,
    absurd,
    boring,
    -- * Plus
    weakenLeft,
    weakenLeft1,
    weakenRight,
    weakenRight1,
    append,
    split,
    -- * Min and max
    isMin,
    isMax,
    -- * Aliases
    fin0, fin1, fin2, fin3, fin4, fin5, fin6, fin7, fin8, fin9,
    ) where

import Control.DeepSeq    (NFData (..))
import Data.Bifunctor     (bimap)
import Data.GADT.Show     (GShow (..))
import Data.Hashable      (Hashable (..))
import Data.List.NonEmpty (NonEmpty (..))
import Data.Proxy         (Proxy (..))
import Data.Type.Nat      (Nat (..))
import Data.Typeable      (Typeable)
import GHC.Exception      (ArithException (..), throw)
import Numeric.Natural    (Natural)

#if MIN_VERSION_some(1,0,5)
import Data.EqP  (EqP (..))
import Data.OrdP (OrdP (..))
#endif

import qualified Data.Boring           as Boring
import qualified Data.List.NonEmpty    as NE
import qualified Data.Type.Nat         as N
import qualified Data.Universe.Class   as U
import qualified Data.Universe.Helpers as U
import qualified Test.QuickCheck       as QC

-- $setup
-- >>> import Data.List (genericLength)
-- >>> import Data.List.NonEmpty (NonEmpty (..))
-- >>> import Data.Foldable (traverse_)
-- >>> import Numeric.Natural (Natural)
-- >>> import qualified Data.Type.Nat as N
-- >>> import qualified Data.Universe.Class as U
-- >>> import qualified Data.Universe.Helpers as U
-- >>> import Data.EqP (eqp)
-- >>> import Data.OrdP (comparep)
-- >>> :set -XTypeApplications

-------------------------------------------------------------------------------
-- Type
-------------------------------------------------------------------------------

-- | Finite numbers: @[0..n-1]@.
data Fin (n :: Nat) where
    FZ :: Fin ('S n)
    FS :: Fin n -> Fin ('S n)
  deriving (Typeable)

-------------------------------------------------------------------------------
-- Instances
-------------------------------------------------------------------------------

deriving instance Eq (Fin n)
deriving instance Ord (Fin n)

#if MIN_VERSION_some(1,0,5)

-- |
--
-- >>> eqp FZ FZ
-- True
--
-- >>> eqp FZ (FS FZ)
-- False
--
-- >>> let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ eqp x y | y <- ys ] | x <- xs ]
-- [True,False,False,False,False,False]
-- [False,True,False,False,False,False]
-- [False,False,True,False,False,False]
-- [False,False,False,True,False,False]
--
-- @since 0.2.2
--
instance EqP Fin where
    eqp :: forall (a :: Nat) (b :: Nat). Fin a -> Fin b -> Bool
eqp Fin a
FZ     Fin b
FZ     = Bool
True
    eqp Fin a
FZ     (FS Fin n
_) = Bool
False
    eqp (FS Fin n
_) Fin b
FZ     = Bool
False
    eqp (FS Fin n
n) (FS Fin n
m) = forall k (f :: k -> *) (a :: k) (b :: k).
EqP @k f =>
f a -> f b -> Bool
eqp Fin n
n Fin n
m

-- |
--
-- >>> let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ comparep x y | y <- ys ] | x <- xs ]
-- [EQ,LT,LT,LT,LT,LT]
-- [GT,EQ,LT,LT,LT,LT]
-- [GT,GT,EQ,LT,LT,LT]
-- [GT,GT,GT,EQ,LT,LT]
--
-- @since 0.2.2
instance OrdP Fin where
    comparep :: forall (a :: Nat) (b :: Nat). Fin a -> Fin b -> Ordering
comparep Fin a
FZ     Fin b
FZ     = Ordering
EQ
    comparep Fin a
FZ     (FS Fin n
_) = Ordering
LT
    comparep (FS Fin n
_) Fin b
FZ     = Ordering
GT
    comparep (FS Fin n
n) (FS Fin n
m) = forall k (f :: k -> *) (a :: k) (b :: k).
OrdP @k f =>
f a -> f b -> Ordering
comparep Fin n
n Fin n
m

#endif

-- | 'Fin' is printed as 'Natural'.
--
-- To see explicit structure, use 'explicitShow' or 'explicitShowsPrec'
instance Show (Fin n) where
    showsPrec :: Int -> Fin n -> ShowS
showsPrec Int
d  = forall a. Show a => Int -> a -> ShowS
showsPrec Int
d forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). Fin n -> Natural
toNatural

-- | @since 0.2.2
instance GShow Fin where
    gshowsPrec :: forall (n :: Nat). Int -> Fin n -> ShowS
gshowsPrec = forall a. Show a => Int -> a -> ShowS
showsPrec

-- | Operations module @n@.
--
-- >>> map fromInteger [0, 1, 2, 3, 4, -5] :: [Fin N.Nat3]
-- [0,1,2,0,1,1]
--
-- >>> fromInteger 42 :: Fin N.Nat0
-- *** Exception: divide by zero
-- ...
--
-- >>> signum (FZ :: Fin N.Nat1)
-- 0
--
-- >>> signum (3 :: Fin N.Nat4)
-- 1
--
-- >>> 2 + 3 :: Fin N.Nat4
-- 1
--
-- >>> 2 * 3 :: Fin N.Nat4
-- 2
--
instance N.SNatI n => Num (Fin n) where
    abs :: Fin n -> Fin n
abs = forall a. a -> a
id

    signum :: Fin n -> Fin n
signum Fin n
FZ          = forall (n :: Nat). Fin ('S n)
FZ
    signum (FS Fin n
FZ)     = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin ('S n)
FZ
    signum (FS (FS Fin n
_)) = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin ('S n)
FZ

    fromInteger :: Integer -> Fin n
fromInteger = forall (n :: Nat) i. (Num i, Ord i, SNatI n) => i -> Fin n
unsafeFromNum forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Integral a => a -> a -> a
`mod` forall (n :: Nat) m (proxy :: Nat -> *).
(SNatI n, Num m) =>
proxy n -> m
N.reflectToNum (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy n))

    Fin n
n + :: Fin n -> Fin n -> Fin n
+ Fin n
m = forall a. Num a => Integer -> a
fromInteger (forall a. Integral a => a -> Integer
toInteger Fin n
n forall a. Num a => a -> a -> a
+ forall a. Integral a => a -> Integer
toInteger Fin n
m)
    Fin n
n * :: Fin n -> Fin n -> Fin n
* Fin n
m = forall a. Num a => Integer -> a
fromInteger (forall a. Integral a => a -> Integer
toInteger Fin n
n forall a. Num a => a -> a -> a
* forall a. Integral a => a -> Integer
toInteger Fin n
m)
    Fin n
n - :: Fin n -> Fin n -> Fin n
- Fin n
m = forall a. Num a => Integer -> a
fromInteger (forall a. Integral a => a -> Integer
toInteger Fin n
n forall a. Num a => a -> a -> a
- forall a. Integral a => a -> Integer
toInteger Fin n
m)

    negate :: Fin n -> Fin n
negate = forall a. Num a => Integer -> a
fromInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
negate forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger

instance N.SNatI n => Real (Fin n) where
    toRational :: Fin n -> Rational
toRational = forall a (n :: Nat). a -> (a -> a) -> Fin n -> a
cata Rational
0 forall a. Enum a => a -> a
succ

-- | 'quot' works only on @'Fin' n@ where @n@ is prime.
instance N.SNatI n => Integral (Fin n) where
    toInteger :: Fin n -> Integer
toInteger = forall a (n :: Nat). a -> (a -> a) -> Fin n -> a
cata Integer
0 forall a. Enum a => a -> a
succ

    quotRem :: Fin n -> Fin n -> (Fin n, Fin n)
quotRem Fin n
a Fin n
b = (forall a. Integral a => a -> a -> a
quot Fin n
a Fin n
b, Fin n
0)
    quot :: Fin n -> Fin n -> Fin n
quot Fin n
a Fin n
b = Fin n
a forall a. Num a => a -> a -> a
* forall (n :: Nat). SNatI n => Fin n -> Fin n
inverse Fin n
b

-- | Mirror the values, 'minBound' becomes 'maxBound', etc.
--
-- >>> map mirror universe :: [Fin N.Nat4]
-- [3,2,1,0]
--
-- >>> reverse universe :: [Fin N.Nat4]
-- [3,2,1,0]
--
-- @since 0.1.1
--
mirror :: forall n. N.SNatI n => Fin n -> Fin n
mirror :: forall (n :: Nat). SNatI n => Fin n -> Fin n
mirror = forall (n :: Nat). Mirror n -> Fin n -> Fin n
getMirror (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Mirror 'Z
start forall (m :: Nat). SNatI m => Mirror m -> Mirror ('S m)
step) where
    start :: Mirror 'Z
    start :: Mirror 'Z
start = forall (n :: Nat). (Fin n -> Fin n) -> Mirror n
Mirror forall a. a -> a
id

    step :: forall m. N.SNatI m => Mirror m -> Mirror ('S m)
    step :: forall (m :: Nat). SNatI m => Mirror m -> Mirror ('S m)
step (Mirror Fin m -> Fin m
rec) = forall (n :: Nat). (Fin n -> Fin n) -> Mirror n
Mirror forall a b. (a -> b) -> a -> b
$ \Fin ('S m)
n -> case Fin ('S m)
n of
        Fin ('S m)
FZ   -> forall (n :: Nat). MaxBound n -> Fin ('S n)
getMaxBound (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (forall (n :: Nat). Fin ('S n) -> MaxBound n
MaxBound forall (n :: Nat). Fin ('S n)
FZ) (forall (n :: Nat). Fin ('S n) -> MaxBound n
MaxBound forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). Fin n -> Fin ('S n)
FS forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). MaxBound n -> Fin ('S n)
getMaxBound))
        FS Fin n
m -> forall (n :: Nat). SNatI n => Fin n -> Fin ('S n)
weakenLeft1 (Fin m -> Fin m
rec Fin n
m)

newtype Mirror n = Mirror { forall (n :: Nat). Mirror n -> Fin n -> Fin n
getMirror :: Fin n -> Fin n }

-- | Multiplicative inverse.
--
-- Works for @'Fin' n@ where @n@ is coprime with an argument, i.e. in general when @n@ is prime.
--
-- >>> map inverse universe :: [Fin N.Nat5]
-- [0,1,3,2,4]
--
-- >>> zipWith (*) universe (map inverse universe) :: [Fin N.Nat5]
-- [0,1,1,1,1]
--
-- Adaptation of [pseudo-code in Wikipedia](https://en.wikipedia.org/wiki/Extended_Euclidean_algorithm#Modular_integers)
--
inverse :: forall n. N.SNatI n => Fin n -> Fin n
inverse :: forall (n :: Nat). SNatI n => Fin n -> Fin n
inverse = forall a. Num a => Integer -> a
fromInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Integer -> Integer -> Integer
iter Integer
0 Integer
n Integer
1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger where
    n :: Integer
n = forall (n :: Nat) m (proxy :: Nat -> *).
(SNatI n, Num m) =>
proxy n -> m
N.reflectToNum (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy n)

    iter :: Integer -> Integer -> Integer -> Integer -> Integer
iter Integer
t Integer
_ Integer
_  Integer
0
        | Integer
t forall a. Ord a => a -> a -> Bool
< Integer
0     = Integer
t forall a. Num a => a -> a -> a
+ Integer
n
        | Bool
otherwise = Integer
t
    iter Integer
t Integer
r Integer
t' Integer
r' =
        let q :: Integer
q = Integer
r forall a. Integral a => a -> a -> a
`div` Integer
r'
        in Integer -> Integer -> Integer -> Integer -> Integer
iter Integer
t' Integer
r' (Integer
t forall a. Num a => a -> a -> a
- Integer
q forall a. Num a => a -> a -> a
* Integer
t') (Integer
r forall a. Num a => a -> a -> a
- Integer
q forall a. Num a => a -> a -> a
* Integer
r')

instance N.SNatI n => Enum (Fin n) where
    fromEnum :: Fin n -> Int
fromEnum = forall (m :: Nat). Fin m -> Int
go where
        go :: Fin m -> Int
        go :: forall (m :: Nat). Fin m -> Int
go Fin m
FZ     = Int
0
        go (FS Fin n
n) = forall a. Enum a => a -> a
succ (forall (m :: Nat). Fin m -> Int
go Fin n
n)

    toEnum :: Int -> Fin n
toEnum = forall (n :: Nat) i. (Num i, Ord i, SNatI n) => i -> Fin n
unsafeFromNum

instance (n ~ 'S m, N.SNatI m) => Bounded (Fin n) where
    minBound :: Fin n
minBound = forall (n :: Nat). Fin ('S n)
FZ
    maxBound :: Fin n
maxBound = forall (n :: Nat). MaxBound n -> Fin ('S n)
getMaxBound forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction
        (forall (n :: Nat). Fin ('S n) -> MaxBound n
MaxBound forall (n :: Nat). Fin ('S n)
FZ)
        (forall (n :: Nat). Fin ('S n) -> MaxBound n
MaxBound forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). Fin n -> Fin ('S n)
FS forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). MaxBound n -> Fin ('S n)
getMaxBound)

newtype MaxBound n = MaxBound { forall (n :: Nat). MaxBound n -> Fin ('S n)
getMaxBound :: Fin ('S n) }

instance NFData (Fin n) where
    rnf :: Fin n -> ()
rnf Fin n
FZ     = ()
    rnf (FS Fin n
n) = forall a. NFData a => a -> ()
rnf Fin n
n

instance Hashable (Fin n) where
    hashWithSalt :: Int -> Fin n -> Int
hashWithSalt Int
salt = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (n :: Nat). a -> (a -> a) -> Fin n -> a
cata (Integer
0 :: Integer) forall a. Enum a => a -> a
succ

-------------------------------------------------------------------------------
-- Boring
-------------------------------------------------------------------------------

-- | @since 0.2.1
instance n ~ 'Z => Boring.Absurd (Fin n) where
    absurd :: forall b. Fin n -> b
absurd = forall b. Fin 'Z -> b
absurd

-------------------------------------------------------------------------------
-- QuickCheck
-------------------------------------------------------------------------------

instance (n ~ 'S m, N.SNatI m) => QC.Arbitrary (Fin n) where
    arbitrary :: Gen (Fin n)
arbitrary = forall (n :: Nat). Arb n -> Gen (Fin ('S n))
getArb forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (forall (n :: Nat). Gen (Fin ('S n)) -> Arb n
Arb (forall (m :: * -> *) a. Monad m => a -> m a
return forall (n :: Nat). Fin ('S n)
FZ)) forall (p :: Nat). SNatI p => Arb p -> Arb ('S p)
step where
        step :: forall p. N.SNatI p => Arb p -> Arb ('S p)
        step :: forall (p :: Nat). SNatI p => Arb p -> Arb ('S p)
step (Arb Gen (Fin ('S p))
p) = forall (n :: Nat). Gen (Fin ('S n)) -> Arb n
Arb forall a b. (a -> b) -> a -> b
$ forall a. [(Int, Gen a)] -> Gen a
QC.frequency
            [ (Int
1,                                 forall (m :: * -> *) a. Monad m => a -> m a
return forall (n :: Nat). Fin ('S n)
FZ)
            , (forall (n :: Nat) m (proxy :: Nat -> *).
(SNatI n, Num m) =>
proxy n -> m
N.reflectToNum (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy p), forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (n :: Nat). Fin n -> Fin ('S n)
FS Gen (Fin ('S p))
p)
            ]

    shrink :: Fin n -> [Fin n]
shrink = forall (n :: Nat). Fin n -> [Fin n]
shrink

shrink :: Fin n -> [Fin n]
shrink :: forall (n :: Nat). Fin n -> [Fin n]
shrink Fin n
FZ      = []
shrink (FS Fin n
FZ) = [forall (n :: Nat). Fin ('S n)
FZ]
shrink (FS Fin n
n)  = forall a b. (a -> b) -> [a] -> [b]
map forall (n :: Nat). Fin n -> Fin ('S n)
FS (forall (n :: Nat). Fin n -> [Fin n]
shrink Fin n
n)

newtype Arb n = Arb { forall (n :: Nat). Arb n -> Gen (Fin ('S n))
getArb :: QC.Gen (Fin ('S n)) }

instance QC.CoArbitrary (Fin n) where
    coarbitrary :: forall b. Fin n -> Gen b -> Gen b
coarbitrary Fin n
FZ     = forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
0 :: Int)
    coarbitrary (FS Fin n
n) = forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
1 :: Int) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary Fin n
n

instance (n ~ 'S m, N.SNatI m) => QC.Function (Fin n) where
    function :: forall b. (Fin n -> b) -> Fin n :-> b
function = case forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat m of
        SNat m
N.SZ -> forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\Fin n
_ -> ()) (\() -> forall (n :: Nat). Fin ('S n)
FZ)
        SNat m
N.SS -> forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap forall (n :: Nat). Fin ('S n) -> Maybe (Fin n)
isMin      (forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall (n :: Nat). Fin ('S n)
FZ forall (n :: Nat). Fin n -> Fin ('S n)
FS)

-- TODO: https://github.com/nick8325/quickcheck/pull/283
-- newtype Fun b m = Fun { getFun :: (Fin ('S m) -> b) -> Fin ('S m) QC.:-> b }

-------------------------------------------------------------------------------
-- universe-base
-------------------------------------------------------------------------------

-- | @since 0.1.2
instance N.SNatI n => U.Universe (Fin n) where
    universe :: [Fin n]
universe = forall (n :: Nat). SNatI n => [Fin n]
universe

-- |
--
-- >>> (U.cardinality :: U.Tagged (Fin N.Nat3) Natural) == U.Tagged (genericLength (U.universeF :: [Fin N.Nat3]))
-- True
--
-- @since 0.1.2
--
instance N.SNatI n => U.Finite   (Fin n) where
    universeF :: [Fin n]
universeF   = forall a. Universe a => [a]
U.universe
    cardinality :: Tagged @(*) (Fin n) Natural
cardinality = forall {k} (s :: k) b. b -> Tagged @k s b
U.Tagged forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) m (proxy :: Nat -> *).
(SNatI n, Num m) =>
proxy n -> m
N.reflectToNum (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy n)

-------------------------------------------------------------------------------
-- Showing
-------------------------------------------------------------------------------

-- | 'show' displaying a structure of 'Fin'.
--
-- >>> explicitShow (0 :: Fin N.Nat1)
-- "FZ"
--
-- >>> explicitShow (2 :: Fin N.Nat3)
-- "FS (FS FZ)"
--
explicitShow :: Fin n -> String
explicitShow :: forall (n :: Nat). Fin n -> String
explicitShow Fin n
n = forall (n :: Nat). Int -> Fin n -> ShowS
explicitShowsPrec Int
0 Fin n
n String
""

-- | 'showsPrec' displaying a structure of 'Fin'.
explicitShowsPrec :: Int -> Fin n -> ShowS
explicitShowsPrec :: forall (n :: Nat). Int -> Fin n -> ShowS
explicitShowsPrec Int
_ Fin n
FZ     = String -> ShowS
showString String
"FZ"
explicitShowsPrec Int
d (FS Fin n
n) = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10)
    forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"FS "
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). Int -> Fin n -> ShowS
explicitShowsPrec Int
11 Fin n
n

-------------------------------------------------------------------------------
-- Conversions
-------------------------------------------------------------------------------

-- | Fold 'Fin'.
cata :: forall a n. a -> (a -> a) -> Fin n -> a
cata :: forall a (n :: Nat). a -> (a -> a) -> Fin n -> a
cata a
z a -> a
f = forall (m :: Nat). Fin m -> a
go where
    go :: Fin m -> a
    go :: forall (m :: Nat). Fin m -> a
go Fin m
FZ = a
z
    go (FS Fin n
n) = a -> a
f (forall (m :: Nat). Fin m -> a
go Fin n
n)

-- | Convert to 'Nat'.
toNat :: Fin n -> N.Nat
toNat :: forall (n :: Nat). Fin n -> Nat
toNat = forall a (n :: Nat). a -> (a -> a) -> Fin n -> a
cata Nat
Z Nat -> Nat
S

-- | Convert from 'Nat'.
--
-- >>> fromNat N.nat1 :: Maybe (Fin N.Nat2)
-- Just 1
--
-- >>> fromNat N.nat1 :: Maybe (Fin N.Nat1)
-- Nothing
--
fromNat :: N.SNatI n => N.Nat -> Maybe (Fin n)
fromNat :: forall (n :: Nat). SNatI n => Nat -> Maybe (Fin n)
fromNat = forall (n :: Nat). NatToFin n -> Nat -> Maybe (Fin n)
appNatToFin (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction NatToFin 'Z
start forall (n :: Nat). NatToFin n -> NatToFin ('S n)
step) where
    start :: NatToFin 'Z
    start :: NatToFin 'Z
start = forall (n :: Nat). (Nat -> Maybe (Fin n)) -> NatToFin n
NatToFin forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a. Maybe a
Nothing

    step :: NatToFin n -> NatToFin ('S n)
    step :: forall (n :: Nat). NatToFin n -> NatToFin ('S n)
step (NatToFin Nat -> Maybe (Fin n)
f) = forall (n :: Nat). (Nat -> Maybe (Fin n)) -> NatToFin n
NatToFin forall a b. (a -> b) -> a -> b
$ \Nat
n -> case Nat
n of
        Nat
Z   -> forall a. a -> Maybe a
Just forall (n :: Nat). Fin ('S n)
FZ
        S Nat
m -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (n :: Nat). Fin n -> Fin ('S n)
FS (Nat -> Maybe (Fin n)
f Nat
m)

newtype NatToFin n = NatToFin { forall (n :: Nat). NatToFin n -> Nat -> Maybe (Fin n)
appNatToFin :: N.Nat -> Maybe (Fin n) }

-- | Convert to 'Natural'.
toNatural :: Fin n -> Natural
toNatural :: forall (n :: Nat). Fin n -> Natural
toNatural = forall a (n :: Nat). a -> (a -> a) -> Fin n -> a
cata Natural
0 forall a. Enum a => a -> a
succ

-- | Convert from any 'Ord' 'Num'.
unsafeFromNum :: forall n i. (Num i, Ord i, N.SNatI n) => i -> Fin n
unsafeFromNum :: forall (n :: Nat) i. (Num i, Ord i, SNatI n) => i -> Fin n
unsafeFromNum = forall i (n :: Nat). UnsafeFromNum i n -> i -> Fin n
appUnsafeFromNum (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction UnsafeFromNum i 'Z
start forall (m :: Nat). UnsafeFromNum i m -> UnsafeFromNum i ('S m)
step) where
    start :: UnsafeFromNum i 'Z
    start :: UnsafeFromNum i 'Z
start = forall i (n :: Nat). (i -> Fin n) -> UnsafeFromNum i n
UnsafeFromNum forall a b. (a -> b) -> a -> b
$ \i
n -> case forall a. Ord a => a -> a -> Ordering
compare i
n i
0 of
        Ordering
LT -> forall a e. Exception e => e -> a
throw ArithException
Underflow
        Ordering
EQ -> forall a e. Exception e => e -> a
throw ArithException
Overflow
        Ordering
GT -> forall a e. Exception e => e -> a
throw ArithException
Overflow

    step :: UnsafeFromNum i m -> UnsafeFromNum i ('S m)
    step :: forall (m :: Nat). UnsafeFromNum i m -> UnsafeFromNum i ('S m)
step (UnsafeFromNum i -> Fin m
f) = forall i (n :: Nat). (i -> Fin n) -> UnsafeFromNum i n
UnsafeFromNum forall a b. (a -> b) -> a -> b
$ \i
n -> case forall a. Ord a => a -> a -> Ordering
compare i
n i
0 of
        Ordering
EQ -> forall (n :: Nat). Fin ('S n)
FZ
        Ordering
GT -> forall (n :: Nat). Fin n -> Fin ('S n)
FS (i -> Fin m
f (i
n forall a. Num a => a -> a -> a
- i
1))
        Ordering
LT -> forall a e. Exception e => e -> a
throw ArithException
Underflow

newtype UnsafeFromNum i n = UnsafeFromNum { forall i (n :: Nat). UnsafeFromNum i n -> i -> Fin n
appUnsafeFromNum :: i -> Fin n }

-------------------------------------------------------------------------------
-- "Interesting" stuff
-------------------------------------------------------------------------------

-- | All values. @[minBound .. maxBound]@ won't work for @'Fin' 'N.Nat0'@.
--
-- >>> universe :: [Fin N.Nat3]
-- [0,1,2]
universe :: N.SNatI n => [Fin n]
universe :: forall (n :: Nat). SNatI n => [Fin n]
universe = forall (n :: Nat). Universe n -> [Fin n]
getUniverse forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (forall (n :: Nat). [Fin n] -> Universe n
Universe []) forall (n :: Nat). Universe n -> Universe ('S n)
step where
    step :: Universe n -> Universe ('S n)
    step :: forall (n :: Nat). Universe n -> Universe ('S n)
step (Universe [Fin n]
xs) = forall (n :: Nat). [Fin n] -> Universe n
Universe (forall (n :: Nat). Fin ('S n)
FZ forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall (n :: Nat). Fin n -> Fin ('S n)
FS [Fin n]
xs)

-- | Like 'universe' but 'NonEmpty'.
--
-- >>> universe1 :: NonEmpty (Fin N.Nat3)
-- 0 :| [1,2]
universe1 :: N.SNatI n => NonEmpty (Fin ('S n))
universe1 :: forall (n :: Nat). SNatI n => NonEmpty (Fin ('S n))
universe1 = forall (n :: Nat). Universe1 n -> NonEmpty (Fin ('S n))
getUniverse1 forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (forall (n :: Nat). NonEmpty (Fin ('S n)) -> Universe1 n
Universe1 (forall (n :: Nat). Fin ('S n)
FZ forall a. a -> [a] -> NonEmpty a
:| [])) forall (n :: Nat). Universe1 n -> Universe1 ('S n)
step where
    step :: Universe1 n -> Universe1 ('S n)
    step :: forall (n :: Nat). Universe1 n -> Universe1 ('S n)
step (Universe1 NonEmpty (Fin ('S n))
xs) = forall (n :: Nat). NonEmpty (Fin ('S n)) -> Universe1 n
Universe1 (forall a. a -> NonEmpty a -> NonEmpty a
NE.cons forall (n :: Nat). Fin ('S n)
FZ (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (n :: Nat). Fin n -> Fin ('S n)
FS NonEmpty (Fin ('S n))
xs))

-- | 'universe' which will be fully inlined, if @n@ is known at compile time.
--
-- >>> inlineUniverse :: [Fin N.Nat3]
-- [0,1,2]
inlineUniverse :: N.SNatI n => [Fin n]
inlineUniverse :: forall (n :: Nat). SNatI n => [Fin n]
inlineUniverse = forall (n :: Nat). Universe n -> [Fin n]
getUniverse forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (forall (n :: Nat). [Fin n] -> Universe n
Universe []) forall (n :: Nat). Universe n -> Universe ('S n)
step where
    step :: Universe n -> Universe ('S n)
    step :: forall (n :: Nat). Universe n -> Universe ('S n)
step (Universe [Fin n]
xs) = forall (n :: Nat). [Fin n] -> Universe n
Universe (forall (n :: Nat). Fin ('S n)
FZ forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall (n :: Nat). Fin n -> Fin ('S n)
FS [Fin n]
xs)

-- | >>> inlineUniverse1 :: NonEmpty (Fin N.Nat3)
-- 0 :| [1,2]
inlineUniverse1 :: N.SNatI n => NonEmpty (Fin ('S n))
inlineUniverse1 :: forall (n :: Nat). SNatI n => NonEmpty (Fin ('S n))
inlineUniverse1 = forall (n :: Nat). Universe1 n -> NonEmpty (Fin ('S n))
getUniverse1 forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (forall (n :: Nat). NonEmpty (Fin ('S n)) -> Universe1 n
Universe1 (forall (n :: Nat). Fin ('S n)
FZ forall a. a -> [a] -> NonEmpty a
:| [])) forall (n :: Nat). Universe1 n -> Universe1 ('S n)
step where
    step :: Universe1 n -> Universe1 ('S n)
    step :: forall (n :: Nat). Universe1 n -> Universe1 ('S n)
step (Universe1 NonEmpty (Fin ('S n))
xs) = forall (n :: Nat). NonEmpty (Fin ('S n)) -> Universe1 n
Universe1 (forall a. a -> NonEmpty a -> NonEmpty a
NE.cons forall (n :: Nat). Fin ('S n)
FZ (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (n :: Nat). Fin n -> Fin ('S n)
FS NonEmpty (Fin ('S n))
xs))

newtype Universe  n = Universe  { forall (n :: Nat). Universe n -> [Fin n]
getUniverse  :: [Fin n] }
newtype Universe1 n = Universe1 { forall (n :: Nat). Universe1 n -> NonEmpty (Fin ('S n))
getUniverse1 :: NonEmpty (Fin ('S n)) }

-- | @'Fin' 'N.Nat0'@ is not inhabited.
absurd :: Fin N.Nat0 -> b
absurd :: forall b. Fin 'Z -> b
absurd Fin 'Z
n = case Fin 'Z
n of {}

-- | Counting to one is boring.
--
-- >>> boring
-- 0
boring :: Fin N.Nat1
boring :: Fin ('S 'Z)
boring = forall (n :: Nat). Fin ('S n)
FZ

-------------------------------------------------------------------------------
-- min and max
-------------------------------------------------------------------------------

-- | Return a one less.
--
-- >>> isMin (FZ :: Fin N.Nat1)
-- Nothing
--
-- >>> map isMin universe :: [Maybe (Fin N.Nat3)]
-- [Nothing,Just 0,Just 1,Just 2]
--
-- @since 0.1.1
--
isMin :: Fin ('S n) -> Maybe (Fin n)
isMin :: forall (n :: Nat). Fin ('S n) -> Maybe (Fin n)
isMin Fin ('S n)
FZ     = forall a. Maybe a
Nothing
isMin (FS Fin n
n) = forall a. a -> Maybe a
Just Fin n
n

-- | Return a one less.
--
-- >>> isMax (FZ :: Fin N.Nat1)
-- Nothing
--
-- >>> map isMax universe :: [Maybe (Fin N.Nat3)]
-- [Just 0,Just 1,Just 2,Nothing]
--
-- @since 0.1.1
--
isMax :: forall n. N.SNatI n => Fin ('S n) -> Maybe (Fin n)
isMax :: forall (n :: Nat). SNatI n => Fin ('S n) -> Maybe (Fin n)
isMax = forall (n :: Nat). IsMax n -> Fin ('S n) -> Maybe (Fin n)
getIsMax (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction IsMax 'Z
start forall (m :: Nat). IsMax m -> IsMax ('S m)
step) where
    start :: IsMax 'Z
    start :: IsMax 'Z
start = forall (n :: Nat). (Fin ('S n) -> Maybe (Fin n)) -> IsMax n
IsMax forall a b. (a -> b) -> a -> b
$ \Fin ('S 'Z)
_ -> forall a. Maybe a
Nothing

    step :: IsMax m -> IsMax ('S m)
    step :: forall (m :: Nat). IsMax m -> IsMax ('S m)
step (IsMax Fin ('S m) -> Maybe (Fin m)
rec) = forall (n :: Nat). (Fin ('S n) -> Maybe (Fin n)) -> IsMax n
IsMax forall a b. (a -> b) -> a -> b
$ \Fin ('S ('S m))
n -> case Fin ('S ('S m))
n of
        Fin ('S ('S m))
FZ   -> forall a. a -> Maybe a
Just forall (n :: Nat). Fin ('S n)
FZ
        FS Fin n
m -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (n :: Nat). Fin n -> Fin ('S n)
FS (Fin ('S m) -> Maybe (Fin m)
rec Fin n
m)

newtype IsMax n = IsMax { forall (n :: Nat). IsMax n -> Fin ('S n) -> Maybe (Fin n)
getIsMax :: Fin ('S n) -> Maybe (Fin n) }

-------------------------------------------------------------------------------
-- Append & Split
-------------------------------------------------------------------------------

-- | >>> map weakenRight1 universe :: [Fin N.Nat5]
-- [1,2,3,4]
--
-- @since 0.1.1
weakenRight1 :: Fin n -> Fin ('S n)
weakenRight1 :: forall (n :: Nat). Fin n -> Fin ('S n)
weakenRight1 = forall (n :: Nat). Fin n -> Fin ('S n)
FS

-- | >>> map weakenLeft1 universe :: [Fin N.Nat5]
-- [0,1,2,3]
--
-- @since 0.1.1
weakenLeft1 :: N.SNatI n => Fin n -> Fin ('S n)
weakenLeft1 :: forall (n :: Nat). SNatI n => Fin n -> Fin ('S n)
weakenLeft1 = forall (n :: Nat). Weaken1 n -> Fin n -> Fin ('S n)
getWeaken1 (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Weaken1 'Z
start forall (n :: Nat). Weaken1 n -> Weaken1 ('S n)
step) where
    start :: Weaken1 'Z
    start :: Weaken1 'Z
start = forall (n :: Nat). (Fin n -> Fin ('S n)) -> Weaken1 n
Weaken1 forall b. Fin 'Z -> b
absurd

    step :: Weaken1 n -> Weaken1 ('S n)
    step :: forall (n :: Nat). Weaken1 n -> Weaken1 ('S n)
step (Weaken1 Fin n -> Fin ('S n)
go) = forall (n :: Nat). (Fin n -> Fin ('S n)) -> Weaken1 n
Weaken1 forall a b. (a -> b) -> a -> b
$ \Fin ('S n)
n -> case Fin ('S n)
n of
        Fin ('S n)
FZ    -> forall (n :: Nat). Fin ('S n)
FZ
        FS Fin n
n' -> forall (n :: Nat). Fin n -> Fin ('S n)
FS (Fin n -> Fin ('S n)
go Fin n
n')

newtype Weaken1 n = Weaken1 { forall (n :: Nat). Weaken1 n -> Fin n -> Fin ('S n)
getWeaken1 :: Fin n -> Fin ('S n) }

-- | >>> map (weakenLeft (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3])
-- [0,1,2]
weakenLeft :: forall n m. N.SNatI n => Proxy m -> Fin n -> Fin (N.Plus n m)
weakenLeft :: forall (n :: Nat) (m :: Nat).
SNatI n =>
Proxy @Nat m -> Fin n -> Fin (Plus n m)
weakenLeft Proxy @Nat m
_ = forall (m :: Nat) (n :: Nat).
WeakenLeft m n -> Fin n -> Fin (Plus n m)
getWeakenLeft (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction WeakenLeft m 'Z
start forall (p :: Nat). WeakenLeft m p -> WeakenLeft m ('S p)
step :: WeakenLeft m n) where
    start :: WeakenLeft m 'Z
    start :: WeakenLeft m 'Z
start = forall (m :: Nat) (n :: Nat).
(Fin n -> Fin (Plus n m)) -> WeakenLeft m n
WeakenLeft forall b. Fin 'Z -> b
absurd

    step :: WeakenLeft m p -> WeakenLeft m ('S p)
    step :: forall (p :: Nat). WeakenLeft m p -> WeakenLeft m ('S p)
step (WeakenLeft Fin p -> Fin (Plus p m)
go) = forall (m :: Nat) (n :: Nat).
(Fin n -> Fin (Plus n m)) -> WeakenLeft m n
WeakenLeft forall a b. (a -> b) -> a -> b
$ \Fin ('S p)
n -> case Fin ('S p)
n of
        Fin ('S p)
FZ    -> forall (n :: Nat). Fin ('S n)
FZ
        FS Fin n
n' -> forall (n :: Nat). Fin n -> Fin ('S n)
FS (Fin p -> Fin (Plus p m)
go Fin n
n')

newtype WeakenLeft m n = WeakenLeft { forall (m :: Nat) (n :: Nat).
WeakenLeft m n -> Fin n -> Fin (Plus n m)
getWeakenLeft :: Fin n -> Fin (N.Plus n m) }

-- | >>> map (weakenRight (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3])
-- [2,3,4]
weakenRight :: forall n m. N.SNatI n => Proxy n -> Fin m -> Fin (N.Plus n m)
weakenRight :: forall (n :: Nat) (m :: Nat).
SNatI n =>
Proxy @Nat n -> Fin m -> Fin (Plus n m)
weakenRight Proxy @Nat n
_ = forall (m :: Nat) (n :: Nat).
WeakenRight m n -> Fin m -> Fin (Plus n m)
getWeakenRight (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction WeakenRight m 'Z
start forall {n :: Nat} {m :: Nat} {n :: Nat}.
((Plus n m :: Nat) ~ ('S (Plus n m) :: Nat)) =>
WeakenRight m n -> WeakenRight m n
step :: WeakenRight m n) where
    start :: WeakenRight m 'Z
start = forall (m :: Nat) (n :: Nat).
(Fin m -> Fin (Plus n m)) -> WeakenRight m n
WeakenRight forall a. a -> a
id
    step :: WeakenRight m n -> WeakenRight m n
step (WeakenRight Fin m -> Fin (Plus n m)
go) = forall (m :: Nat) (n :: Nat).
(Fin m -> Fin (Plus n m)) -> WeakenRight m n
WeakenRight forall a b. (a -> b) -> a -> b
$ \Fin m
x -> forall (n :: Nat). Fin n -> Fin ('S n)
FS forall a b. (a -> b) -> a -> b
$ Fin m -> Fin (Plus n m)
go Fin m
x

newtype WeakenRight m n = WeakenRight { forall (m :: Nat) (n :: Nat).
WeakenRight m n -> Fin m -> Fin (Plus n m)
getWeakenRight :: Fin m -> Fin (N.Plus n m) }

-- | Append two 'Fin's together.
--
-- >>> append (Left fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))
-- 2
--
-- >>> append (Right fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))
-- 7
--
append :: forall n m. N.SNatI n => Either (Fin n) (Fin m) -> Fin (N.Plus n m)
append :: forall (n :: Nat) (m :: Nat).
SNatI n =>
Either (Fin n) (Fin m) -> Fin (Plus n m)
append (Left Fin n
n)  = forall (n :: Nat) (m :: Nat).
SNatI n =>
Proxy @Nat m -> Fin n -> Fin (Plus n m)
weakenLeft (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy m) Fin n
n
append (Right Fin m
m) = forall (n :: Nat) (m :: Nat).
SNatI n =>
Proxy @Nat n -> Fin m -> Fin (Plus n m)
weakenRight (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy n) Fin m
m

-- | Inverse of 'append'.
--
-- >>> split fin2 :: Either (Fin N.Nat2) (Fin N.Nat3)
-- Right 0
--
-- >>> split fin1 :: Either (Fin N.Nat2) (Fin N.Nat3)
-- Left 1
--
-- >>> map split universe :: [Either (Fin N.Nat2) (Fin N.Nat3)]
-- [Left 0,Left 1,Right 0,Right 1,Right 2]
--
split :: forall n m. N.SNatI n => Fin (N.Plus n m) -> Either (Fin n) (Fin m)
split :: forall (n :: Nat) (m :: Nat).
SNatI n =>
Fin (Plus n m) -> Either (Fin n) (Fin m)
split = forall (m :: Nat) (n :: Nat).
Split m n -> Fin (Plus n m) -> Either (Fin n) (Fin m)
getSplit (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Split m 'Z
start forall (p :: Nat). Split m p -> Split m ('S p)
step) where
    start :: Split m 'Z
    start :: Split m 'Z
start = forall (m :: Nat) (n :: Nat).
(Fin (Plus n m) -> Either (Fin n) (Fin m)) -> Split m n
Split forall a b. b -> Either a b
Right

    step :: Split m p -> Split m ('S p)
    step :: forall (p :: Nat). Split m p -> Split m ('S p)
step (Split Fin (Plus p m) -> Either (Fin p) (Fin m)
go) = forall (m :: Nat) (n :: Nat).
(Fin (Plus n m) -> Either (Fin n) (Fin m)) -> Split m n
Split forall a b. (a -> b) -> a -> b
$ \Fin (Plus ('S p) m)
x -> case Fin (Plus ('S p) m)
x of
        Fin (Plus ('S p) m)
FZ    -> forall a b. a -> Either a b
Left forall (n :: Nat). Fin ('S n)
FZ
        FS Fin n
x' -> forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap forall (n :: Nat). Fin n -> Fin ('S n)
FS forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ Fin (Plus p m) -> Either (Fin p) (Fin m)
go Fin n
x'

newtype Split m n = Split { forall (m :: Nat) (n :: Nat).
Split m n -> Fin (Plus n m) -> Either (Fin n) (Fin m)
getSplit :: Fin (N.Plus n m) -> Either (Fin n) (Fin m) }

-------------------------------------------------------------------------------
-- Aliases
-------------------------------------------------------------------------------

fin0 :: Fin (N.Plus N.Nat0 ('S n))
fin1 :: Fin (N.Plus N.Nat1 ('S n))
fin2 :: Fin (N.Plus N.Nat2 ('S n))
fin3 :: Fin (N.Plus N.Nat3 ('S n))
fin4 :: Fin (N.Plus N.Nat4 ('S n))
fin5 :: Fin (N.Plus N.Nat5 ('S n))
fin6 :: Fin (N.Plus N.Nat6 ('S n))
fin7 :: Fin (N.Plus N.Nat7 ('S n))
fin8 :: Fin (N.Plus N.Nat8 ('S n))
fin9 :: Fin (N.Plus N.Nat9 ('S n))

fin0 :: forall (n :: Nat). Fin (Plus 'Z ('S n))
fin0 = forall (n :: Nat). Fin ('S n)
FZ
fin1 :: forall (n :: Nat). Fin (Plus ('S 'Z) ('S n))
fin1 = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin (Plus 'Z ('S n))
fin0
fin2 :: forall (n :: Nat). Fin (Plus Nat2 ('S n))
fin2 = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin (Plus ('S 'Z) ('S n))
fin1
fin3 :: forall (n :: Nat). Fin (Plus Nat3 ('S n))
fin3 = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin (Plus Nat2 ('S n))
fin2
fin4 :: forall (n :: Nat). Fin (Plus Nat4 ('S n))
fin4 = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin (Plus Nat3 ('S n))
fin3
fin5 :: forall (n :: Nat). Fin (Plus Nat5 ('S n))
fin5 = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin (Plus Nat4 ('S n))
fin4
fin6 :: forall (n :: Nat). Fin (Plus Nat6 ('S n))
fin6 = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin (Plus Nat5 ('S n))
fin5
fin7 :: forall (n :: Nat). Fin (Plus Nat7 ('S n))
fin7 = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin (Plus Nat6 ('S n))
fin6
fin8 :: forall (n :: Nat). Fin (Plus Nat8 ('S n))
fin8 = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin (Plus Nat7 ('S n))
fin7
fin9 :: forall (n :: Nat). Fin (Plus Nat9 ('S n))
fin9 = forall (n :: Nat). Fin n -> Fin ('S n)
FS forall (n :: Nat). Fin (Plus Nat8 ('S n))
fin8