Data.Nat

Nat numbers.

This module is designed to be imported qualified.

Natural, Nat numbers

data Nat

Nat natural numbers.

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

Constructors

Z

S Nat

Instances

Arbitrary Nat

Defined in Data.Nat

Methods

arbitrary :: Gen Nat

shrink :: Nat -> [Nat]

CoArbitrary Nat

Defined in Data.Nat

Methods

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

Function Nat

Defined in Data.Nat

Methods

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

Data Nat

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 :: forall r r'. (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

Enum Nat

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]

Num Nat

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

Integral Nat

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

Real Nat

Defined in Data.Nat

Methods

toRational :: Nat -> Rational

Show Nat

Nat is printed as Natural.

To see explicit structure, use explicitShow or explicitShowsPrec

Defined in Data.Nat

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

NFData Nat

Defined in Data.Nat

Methods

rnf :: Nat -> ()

Eq Nat

Defined in Data.Nat

Methods

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

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

Ord Nat

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

Hashable Nat

Defined in Data.Nat

Methods

hashWithSalt :: Int -> Nat -> Int

hash :: Nat -> Int

Universe Nat

>>> import qualified Data.Universe.Class as U
>>> take 10 (U.universe :: [Nat])
[0,1,2,3,4,5,6,7,8,9]

Since: 0.1.2

Defined in Data.Nat

Methods

universe :: [Nat]

Category LEProof

The other variant (LEPRoof) isn't Category, because leRefl requires SNat evidence.

Defined in Data.Type.Nat.LE.ReflStep

Methods

id :: forall (a :: k). LEProof a a

(.) :: forall (b :: k) (c :: k) (a :: k). LEProof b c -> LEProof a b -> LEProof a c

TestEquality SNat

Defined in Data.Type.Nat

Methods

testEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b)

EqP Fin

>>> eqp FZ FZ
True

>>> eqp FZ (FS FZ)
False

>>> let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ eqp x y | y <- ys ] | x <- xs ]
[True,False,False,False,False,False]
[False,True,False,False,False,False]
[False,False,True,False,False,False]
[False,False,False,True,False,False]

Since: 0.2.2

Defined in Data.Fin

Methods

eqp :: forall (a :: k) (b :: k). Fin a -> Fin b -> Bool

EqP SNat

Since: 0.2.2

Defined in Data.Type.Nat

Methods

eqp :: forall (a :: k) (b :: k). SNat a -> SNat b -> Bool

GNFData SNat

Since: 0.2.1

Defined in Data.Type.Nat

Methods

grnf :: forall (a :: k). SNat a -> ()

GCompare SNat

Since: 0.2.1

Defined in Data.Type.Nat

Methods

gcompare :: forall (a :: k) (b :: k). SNat a -> SNat b -> GOrdering a b

GEq SNat

Since: 0.2.1

Defined in Data.Type.Nat

Methods

geq :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b)

GShow Fin

Since: 0.2.2

Defined in Data.Fin

Methods

gshowsPrec :: forall (a :: k). Int -> Fin a -> ShowS

GShow SNat

Since: 0.2.1

Defined in Data.Type.Nat

Methods

gshowsPrec :: forall (a :: k). Int -> SNat a -> ShowS

OrdP Fin

>>> let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ comparep x y | y <- ys ] | x <- xs ]
[EQ,LT,LT,LT,LT,LT]
[GT,EQ,LT,LT,LT,LT]
[GT,GT,EQ,LT,LT,LT]
[GT,GT,GT,EQ,LT,LT]

Since: 0.2.2

Defined in Data.Fin

Methods

comparep :: forall (a :: k) (b :: k). Fin a -> Fin b -> Ordering

OrdP SNat

Since: 0.2.2

Defined in Data.Type.Nat

Methods

comparep :: forall (a :: k) (b :: k). SNat a -> SNat b -> Ordering

toNatural :: Nat -> Natural

Convert Nat to Natural

>>> toNatural 0
0

>>> toNatural 2
2

>>> toNatural $ S $ S $ Z
2

fromNatural :: Natural -> Nat

Convert Natural to Nat

>>> fromNatural 4
4

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

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

Fold Nat.

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

Showing

explicitShow :: Nat -> String

show displaying a structure of Nat.

>>> explicitShow 0
"Z"

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

explicitShowsPrec :: Int -> Nat -> ShowS

showsPrec displaying a structure of Nat.

Aliases

nat0 :: Nat

nat1 :: Nat

nat2 :: Nat

nat3 :: Nat

nat4 :: Nat

nat5 :: Nat

nat6 :: Nat

nat7 :: Nat

nat8 :: Nat

nat9 :: Nat