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

Data.Nat

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

Instances details
 Source # Instance detailsDefined in Data.Nat Methodssucc :: 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] # Source # Instance detailsDefined in Data.Nat Methods(==) :: Nat -> Nat -> Bool #(/=) :: Nat -> Nat -> Bool # Source # Instance detailsDefined in Data.Nat Methodsquot :: 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) # Source # Instance detailsDefined in Data.Nat Methodsgfoldl :: (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 #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 # Source # Instance detailsDefined in Data.Nat Methods(+) :: Nat -> Nat -> Nat #(-) :: Nat -> Nat -> Nat #(*) :: Nat -> Nat -> Nat #negate :: Nat -> Nat #abs :: Nat -> Nat #signum :: Nat -> Nat # Source # Instance detailsDefined in Data.Nat Methodscompare :: Nat -> Nat -> Ordering #(<) :: Nat -> Nat -> Bool #(<=) :: Nat -> Nat -> Bool #(>) :: Nat -> Nat -> Bool #(>=) :: Nat -> Nat -> Bool #max :: Nat -> Nat -> Nat #min :: Nat -> Nat -> Nat # Source # Instance detailsDefined in Data.Nat Methods Source # Nat is printed as Natural.To see explicit structure, use explicitShow or explicitShowsPrec Instance detailsDefined in Data.Nat MethodsshowsPrec :: Int -> Nat -> ShowS #show :: Nat -> String #showList :: [Nat] -> ShowS # Source # Instance detailsDefined in Data.Nat Methodsfunction :: (Nat -> b) -> Nat :-> b # Source # Instance detailsDefined in Data.Nat Methodsshrink :: Nat -> [Nat] # Source # Instance detailsDefined in Data.Nat Methodscoarbitrary :: Nat -> Gen b -> Gen b # Source # Instance detailsDefined in Data.Nat Methodsrnf :: Nat -> () # Source # Instance detailsDefined in Data.Nat MethodshashWithSalt :: Int -> Nat -> Int #hash :: Nat -> Int # Source # >>> 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 Instance detailsDefined in Data.Nat Methodsuniverse :: [Nat] # Source # The other variant (LEPRoof) isn't Category, because leRefl requires SNat evidence. Instance detailsDefined in Data.Type.Nat.LE.ReflStep Methodsid :: forall (a :: k). LEProof a a #(.) :: forall (b :: k) (c :: k) (a :: k). LEProof b c -> LEProof a b -> LEProof a c # Source # Instance detailsDefined in Data.Type.Nat MethodstestEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b) # Source # Since: 0.2.1 Instance detailsDefined in Data.Type.Nat MethodsgshowsPrec :: forall (a :: k). Int -> SNat a -> ShowS # Source # Since: 0.2.1 Instance detailsDefined in Data.Type.Nat Methodsgeq :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b) # Source # Since: 0.2.1 Instance detailsDefined in Data.Type.Nat Methodsgcompare :: forall (a :: k) (b :: k). SNat a -> SNat b -> GOrdering a b # Source # Since: 0.2.1 Instance detailsDefined in Data.Type.Nat Methodsgrnf :: forall (a :: k). SNat a -> () #

Convert Nat to Natural

>>> toNatural 0
0

>>> toNatural 2
2

>>> toNatural $S$ S \$ Z
2


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

show displaying a structure of Nat.

>>> explicitShow 0
"Z"

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


showsPrec displaying a structure of Nat.