Safe Haskell | None |
---|---|
Language | Haskell2010 |
Finite numbers.
This module is designed to be imported qualified.
- data Fin (n :: Nat) where
- cata :: forall a n. a -> (a -> a) -> Fin n -> a
- explicitShow :: Fin n -> String
- explicitShowsPrec :: Int -> Fin n -> ShowS
- toNat :: Fin n -> Nat
- fromNat :: SNatI n => Nat -> Maybe (Fin n)
- toNatural :: Fin n -> Natural
- toInteger :: Integral a => a -> Integer
- inverse :: forall n. SNatI n => Fin n -> Fin n
- universe :: SNatI n => [Fin n]
- inlineUniverse :: InlineInduction n => [Fin n]
- universe1 :: SNatI n => NonEmpty (Fin (S n))
- inlineUniverse1 :: InlineInduction n => NonEmpty (Fin (S n))
- absurd :: Fin Nat0 -> b
- boring :: Fin Nat1
- fin0 :: Fin (Plus Nat0 (S n))
- fin1 :: Fin (Plus Nat1 (S n))
- fin2 :: Fin (Plus Nat2 (S n))
- fin3 :: Fin (Plus Nat3 (S n))
- fin4 :: Fin (Plus Nat4 (S n))
- fin5 :: Fin (Plus Nat5 (S n))
- fin6 :: Fin (Plus Nat6 (S n))
- fin7 :: Fin (Plus Nat7 (S n))
- fin8 :: Fin (Plus Nat8 (S n))
- fin9 :: Fin (Plus Nat9 (S n))
Documentation
data Fin (n :: Nat) where Source #
Finite numbers: [0..n-1]
.
((~) Nat n (S m), SNatI m) => Bounded (Fin n) Source # | |
SNatI n => Enum (Fin n) Source # | |
Eq (Fin n) Source # | |
SNatI n => Integral (Fin n) Source # | |
SNatI n => Num (Fin n) Source # | Operations module
|
Ord (Fin n) Source # | |
SNatI n => Real (Fin n) Source # | |
Show (Fin n) Source # | To see explicit structure, use |
NFData (Fin n) Source # | |
Hashable (Fin n) Source # | |
Showing
explicitShow :: Fin n -> String Source #
Conversions
fromNat :: SNatI n => Nat -> Maybe (Fin n) Source #
Convert from Nat
.
>>>
fromNat N.nat1 :: Maybe (Fin N.Nat2)
Just 1
>>>
fromNat N.nat1 :: Maybe (Fin N.Nat1)
Nothing
Interesting
inverse :: forall n. SNatI n => Fin n -> Fin n Source #
Multiplicative inverse.
Works for
where Fin
nn
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
inlineUniverse :: InlineInduction n => [Fin n] Source #
universe
which will be fully inlined, if n
is known at compile time.
>>>
inlineUniverse :: [Fin N.Nat3]
[0,1,2]
inlineUniverse1 :: InlineInduction n => NonEmpty (Fin (S n)) Source #
>>>
inlineUniverse1 :: NonEmpty (Fin N.Nat3)
0 :| [1,2]