Data.Fin

Documentation

newtype Fin s n

Constructors

Fin s

Instances

Eq s => Eq (Fin s n)

Ord s => Ord (Fin s n)

Show s => Show (Fin s n)

Typeable (* -> Nat -> *) Fin

natToFin :: (Integral s, KnownNat n, KnownNat (m + 1), n <= m) => proxy n -> Fin s (m + 1)

>>> (natToFin (Proxy :: Proxy 10) :: Fin Int 11)
Fin 10

toFin :: forall s n. (Integral s, KnownNat (n :: Nat)) => s -> Maybe (Fin s n)

>>> (toFin 0 :: Maybe (Fin Int 4))
Just (Fin 0)

>>> (toFin 4 :: Maybe (Fin Int 4))
Nothing

unsafeToFin :: (Integral s, KnownNat n) => s -> Fin s n

>>> (unsafeToFin 10 :: Fin Int 5)
Fin 10

fromFin :: Fin s n -> s

>>> fromFin (finZ :: Fin Int 10)
0

>>> fromFin (finLast :: Fin Int 10)
9

finZ :: (Integral s, KnownNat (n + 1)) => Fin s (n + 1)

finS :: (Integral s, KnownNat n, KnownNat (n + 1)) => Fin s n -> Fin s (n + 1)

finLast :: forall s n. (Integral s, KnownNat n, KnownNat (n + 1)) => Fin s (n + 1)

>>> (finLast :: Fin Int 5)
Fin 4

absurd :: Fin s 0 -> a

weaken :: (Integral s, KnownNat (n + 1)) => Fin s n -> Fin s (n + 1)

weakenN :: (Integral s, KnownNat (n + m)) => proxy m -> Fin s n -> Fin s (n + m)

strengthen :: forall n s. (KnownNat n, Integral s, Ord s) => Fin s (n + 1) -> Either (Fin s (n + 1)) (Fin s n)

shift :: (KnownNat (m + n), Integral s) => proxy m -> Fin s n -> Fin s (m + n)

>>> shift (Proxy :: Proxy 1) (finZ :: Fin Int 20)
Fin 0

>>> (shift (Proxy :: Proxy 10) (finLast :: Fin Int 10) :: Fin Int 20)
Fin 9

finAdd :: (Integral s, KnownNat (n + m)) => Fin s n -> Fin s m -> Fin s (n + m)

finAddN :: forall n s. (KnownNat n, Integral s, Ord s) => Fin s n -> s -> Either (Fin s n) (Fin s n)

finSub :: (KnownNat n, Ord s, Integral s) => Fin s n -> Fin s m -> Either (Fin s n) (Fin s n)

finSubN :: (KnownNat n, Ord s, Integral s) => Fin s n -> s -> Either (Fin s n) (Fin s n)

finMult :: (KnownNat (n * m), Integral s) => Fin s n -> Fin s m -> Fin s (n * m)