Data.Nat

datadata Nat

#

Nat natural numbers.

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

Constructors

Z
S Nat

Instances25Enum, Eq, Integral, Data, Num, Ord, …

Enum NatDefined in fin-0.3.2 · Data.Nat
Eq NatDefined in fin-0.3.2 · Data.Nat
Integral NatDefined in fin-0.3.2 · Data.Nat
Data NatDefined in fin-0.3.2 · Data.Nat
Num NatDefined in fin-0.3.2 · Data.Nat
Ord NatDefined in fin-0.3.2 · Data.Nat
Real NatDefined in fin-0.3.2 · Data.Nat
Show NatDefined in fin-0.3.2 · Data.Nat
Nat is printed as Natural.
To see explicit structure, use explicitShow or explicitShowsPrec
NFData NatDefined in fin-0.3.2 · Data.Nat
Arbitrary NatDefined in fin-0.3.2 · Data.Nat
CoArbitrary NatDefined in fin-0.3.2 · Data.Nat
Function NatDefined in fin-0.3.2 · Data.Nat
Hashable NatDefined in fin-0.3.2 · Data.Nat

Universe NatDefined in fin-0.3.2 · Data.Nat

Example2 expressions

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

Category LEProofDefined in fin-0.3.2 · Data.Type.Nat.LE.ReflStep
The other variant (Data.Type.Nat.LE.LEPRoof) isn't Category, because leRefl requires SNat evidence.
TestEquality SNatDefined in fin-0.3.2 · Data.Type.Nat

EqP FinDefined in fin-0.3.2 · Data.Fin

Example1 expression

>>> eqp FZ FZTrue

Example1 expression

>>> eqp FZ (FS FZ)False

Example1 expression

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

EqP SNatDefined in fin-0.3.2 · Data.Type.Nat
GCompare SNatDefined in fin-0.3.2 · Data.Type.Nat
GEq SNatDefined in fin-0.3.2 · Data.Type.Nat
GNFData SNatDefined in fin-0.3.2 · Data.Type.Nat
GShow FinDefined in fin-0.3.2 · Data.Fin
GShow SNatDefined in fin-0.3.2 · Data.Type.Nat

OrdP FinDefined in fin-0.3.2 · Data.Fin

Example1 expression

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

OrdP SNatDefined in fin-0.3.2 · Data.Type.Nat

valuetoNatural :: Nat -> Natural

#

Convert Nat to Natural

Example1 expression

>>> toNatural 00

Example1 expression

>>> toNatural 22

Example1 expression

>>> toNatural $ S $ S $ Z2

valuefromNatural :: Natural -> Nat

#

Convert Natural to Nat

Example1 expression

>>> fromNatural 44

Example1 expression

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

valuecata :: a -> (a -> a) -> Nat -> a

#

Fold Nat.

Example1 expression

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

Natural, Nat numbers

Constructors

Showing

Aliases