fin-0: Nat and Fin
Data.Nat
Contents
Description
Nat numbers.
Nat
This module is designed to be imported qualified.
Synopsis
data Nat Source #
Nat natural numbers.
Better than GHC's built-in Nat for some use cases.
Constructors
Instances
Methods
succ :: Nat -> Nat #
pred :: Nat -> Nat #
toEnum :: Int -> Nat #
fromEnum :: Nat -> Int #
enumFrom :: Nat -> [Nat] #
enumFromThen :: Nat -> Nat -> [Nat] #
enumFromTo :: Nat -> Nat -> [Nat] #
enumFromThenTo :: Nat -> Nat -> Nat -> [Nat] #
(==) :: Nat -> Nat -> Bool #
(/=) :: Nat -> Nat -> Bool #
quot :: Nat -> Nat -> Nat #
rem :: Nat -> Nat -> Nat #
div :: Nat -> Nat -> Nat #
mod :: Nat -> Nat -> Nat #
quotRem :: Nat -> Nat -> (Nat, Nat) #
divMod :: Nat -> Nat -> (Nat, Nat) #
toInteger :: Nat -> Integer #
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Nat -> c Nat #
gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Nat #
toConstr :: Nat -> Constr #
dataTypeOf :: Nat -> DataType #
dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Nat) #
dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat) #
gmapT :: (forall b. Data b => b -> b) -> Nat -> Nat #
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r #
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r #
gmapQ :: (forall d. Data d => d -> u) -> Nat -> [u] #
gmapQi :: Int -> (forall d. Data d => d -> u) -> Nat -> u #
gmapM :: Monad m => (forall d. Data d => d -> m d) -> Nat -> m Nat #
gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Nat -> m Nat #
gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Nat -> m Nat #
(+) :: Nat -> Nat -> Nat #
(-) :: Nat -> Nat -> Nat #
(*) :: Nat -> Nat -> Nat #
negate :: Nat -> Nat #
abs :: Nat -> Nat #
signum :: Nat -> Nat #
fromInteger :: Integer -> Nat #
compare :: Nat -> Nat -> Ordering #
(<) :: Nat -> Nat -> Bool #
(<=) :: Nat -> Nat -> Bool #
(>) :: Nat -> Nat -> Bool #
(>=) :: Nat -> Nat -> Bool #
max :: Nat -> Nat -> Nat #
min :: Nat -> Nat -> Nat #
toRational :: Nat -> Rational #
Nat is printed as Natural.
Natural
To see explicit structure, use explicitShow or explicitShowsPrec
explicitShow
explicitShowsPrec
showsPrec :: Int -> Nat -> ShowS #
show :: Nat -> String #
showList :: [Nat] -> ShowS #
rnf :: Nat -> () #
hashWithSalt :: Int -> Nat -> Int #
hash :: Nat -> Int #
toNatural :: Nat -> Natural Source #
Convert Nat to Natural
>>> toNatural 0 0
>>>
toNatural 0
>>> toNatural 2 2
toNatural 2
>>> toNatural $ S $ S $ Z 2
toNatural $ S $ S $ Z
fromNatural :: Natural -> Nat Source #
Convert Natural to Nat
>>> fromNatural 4 4
fromNatural 4
>>> explicitShow (fromNatural 4) "S (S (S (S Z)))"
explicitShow (fromNatural 4)
cata :: a -> (a -> a) -> Nat -> a Source #
Fold Nat.
>>> cata [] ('x' :) 2 "xx"
cata [] ('x' :) 2
explicitShow :: Nat -> String Source #
show displaying a structure of Nat.
show
>>> explicitShow 0 "Z"
explicitShow 0
>>> explicitShow 2 "S (S Z)"
explicitShow 2
explicitShowsPrec :: Int -> Nat -> ShowS Source #
showsPrec displaying a structure of Nat.
showsPrec
zero :: Nat Source #
one :: Nat Source #
two :: Nat Source #
three :: Nat Source #
four :: Nat Source #
five :: Nat Source #