fin-0.1.1: Nat and Fin: peano naturals and finite numbers

Safe HaskellSafe
LanguageHaskell2010

Data.Nat

Contents

Description

Nat numbers.

This module is designed to be imported qualified.

Synopsis

Natural, Nat numbers

data Nat Source #

Nat natural numbers.

Better than GHC's built-in Nat for some use cases.

Constructors

Z 
S Nat 
Instances
Enum Nat Source # 
Instance details

Defined in Data.Nat

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] #

Eq Nat Source # 
Instance details

Defined in Data.Nat

Methods

(==) :: Nat -> Nat -> Bool #

(/=) :: Nat -> Nat -> Bool #

Integral Nat Source # 
Instance details

Defined in Data.Nat

Methods

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 #

Data Nat Source # 
Instance details

Defined in Data.Nat

Methods

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 #

Num Nat Source # 
Instance details

Defined in Data.Nat

Methods

(+) :: Nat -> Nat -> Nat #

(-) :: Nat -> Nat -> Nat #

(*) :: Nat -> Nat -> Nat #

negate :: Nat -> Nat #

abs :: Nat -> Nat #

signum :: Nat -> Nat #

fromInteger :: Integer -> Nat #

Ord Nat Source # 
Instance details

Defined in Data.Nat

Methods

compare :: Nat -> Nat -> Ordering #

(<) :: Nat -> Nat -> Bool #

(<=) :: Nat -> Nat -> Bool #

(>) :: Nat -> Nat -> Bool #

(>=) :: Nat -> Nat -> Bool #

max :: Nat -> Nat -> Nat #

min :: Nat -> Nat -> Nat #

Real Nat Source # 
Instance details

Defined in Data.Nat

Methods

toRational :: Nat -> Rational #

Show Nat Source #

Nat is printed as Natural.

To see explicit structure, use explicitShow or explicitShowsPrec

Instance details

Defined in Data.Nat

Methods

showsPrec :: Int -> Nat -> ShowS #

show :: Nat -> String #

showList :: [Nat] -> ShowS #

Function Nat Source # 
Instance details

Defined in Data.Nat

Methods

function :: (Nat -> b) -> Nat :-> b #

Arbitrary Nat Source # 
Instance details

Defined in Data.Nat

Methods

arbitrary :: Gen Nat #

shrink :: Nat -> [Nat] #

CoArbitrary Nat Source # 
Instance details

Defined in Data.Nat

Methods

coarbitrary :: Nat -> Gen b -> Gen b #

NFData Nat Source # 
Instance details

Defined in Data.Nat

Methods

rnf :: Nat -> () #

Hashable Nat Source # 
Instance details

Defined in Data.Nat

Methods

hashWithSalt :: Int -> Nat -> Int #

hash :: Nat -> Int #

TestEquality SNat Source # 
Instance details

Defined in Data.Type.Nat

Methods

testEquality :: SNat a -> SNat b -> Maybe (a :~: b) #

toNatural :: Nat -> Natural Source #

Convert Nat to Natural

>>> toNatural 0
0
>>> toNatural 2
2
>>> toNatural $ S $ S $ Z
2

fromNatural :: Natural -> Nat Source #

Convert Natural to Nat

>>> fromNatural 4
4
>>> explicitShow (fromNatural 4)
"S (S (S (S Z)))"

cata :: a -> (a -> a) -> Nat -> a Source #

Fold Nat.

>>> cata [] ('x' :) 2
"xx"

Showing

explicitShow :: Nat -> String Source #

show displaying a structure of Nat.

>>> explicitShow 0
"Z"
>>> explicitShow 2
"S (S Z)"

explicitShowsPrec :: Int -> Nat -> ShowS Source #

showsPrec displaying a structure of Nat.

Aliases