data-fin-simple-0.1.0.0: Simple integral finite set

Data.Fin

Synopsis

# Documentation

newtype Fin s n Source

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) Source

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

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

````>>> ````(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 Source

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

fromFin :: Fin s n -> s Source

````>>> ````fromFin (finZ :: Fin Int 10)
```0
```
````>>> ````fromFin (finLast :: Fin Int 10)
```9
```

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

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

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

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

absurd :: Fin s 0 -> a Source

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

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

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

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

````>>> ````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) Source

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

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

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

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