    -- | See 'Peano'.

    module Data.Peano ( Peano (Zero, Succ), infinity ) where

    import Data.Data       ( Data )
    import Data.Ix         ( Ix( index, inRange, range, rangeSize ) )

    -- | The natural numbers in (lazy) unary notation.
    data Peano
      = Zero
      | Succ Peano
      deriving (Peano -> Peano -> Bool
    (Peano -> Peano -> Bool) -> (Peano -> Peano -> Bool) -> Eq Peano
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Peano -> Peano -> Bool
    == :: Peano -> Peano -> Bool
    $c/= :: Peano -> Peano -> Bool
    /= :: Peano -> Peano -> Bool
    Eq, Eq Peano
    Eq Peano =>
    (Peano -> Peano -> Ordering)
    -> (Peano -> Peano -> Bool)
    -> (Peano -> Peano -> Bool)
    -> (Peano -> Peano -> Bool)
    -> (Peano -> Peano -> Bool)
    -> (Peano -> Peano -> Peano)
    -> (Peano -> Peano -> Peano)
    -> Ord Peano
    Peano -> Peano -> Bool
    Peano -> Peano -> Ordering
    Peano -> Peano -> Peano
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Peano -> Peano -> Ordering
    compare :: Peano -> Peano -> Ordering
    $c< :: Peano -> Peano -> Bool
    < :: Peano -> Peano -> Bool
    $c<= :: Peano -> Peano -> Bool
    <= :: Peano -> Peano -> Bool
    $c> :: Peano -> Peano -> Bool
    > :: Peano -> Peano -> Bool
    $c>= :: Peano -> Peano -> Bool
    >= :: Peano -> Peano -> Bool
    $cmax :: Peano -> Peano -> Peano
    max :: Peano -> Peano -> Peano
    $cmin :: Peano -> Peano -> Peano
    min :: Peano -> Peano -> Peano
    Ord, Typeable Peano
    Typeable Peano =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> Peano -> c Peano)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Peano)
    -> (Peano -> Constr)
    -> (Peano -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Peano))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Peano))
    -> ((forall b. Data b => b -> b) -> Peano -> Peano)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Peano -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> Peano -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Peano -> m Peano)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Peano -> m Peano)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Peano -> m Peano)
    -> Data Peano
    Peano -> Constr
    Peano -> DataType
    (forall b. Data b => b -> b) -> Peano -> Peano
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Peano -> u
    forall u. (forall d. Data d => d -> u) -> Peano -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Peano -> m Peano
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Peano -> m Peano
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Peano
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Peano -> c Peano
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Peano)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Peano)
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Peano -> c Peano
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Peano -> c Peano
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Peano
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Peano
    $ctoConstr :: Peano -> Constr
    toConstr :: Peano -> Constr
    $cdataTypeOf :: Peano -> DataType
    dataTypeOf :: Peano -> DataType
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Peano)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Peano)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Peano)
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Peano)
    $cgmapT :: (forall b. Data b => b -> b) -> Peano -> Peano
    gmapT :: (forall b. Data b => b -> b) -> Peano -> Peano
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r
    gmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r
    gmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Peano -> [u]
    gmapQ :: forall u. (forall d. Data d => d -> u) -> Peano -> [u]
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Peano -> u
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Peano -> u
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Peano -> m Peano
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Peano -> m Peano
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Peano -> m Peano
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Peano -> m Peano
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Peano -> m Peano
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Peano -> m Peano
    Data, ReadPrec [Peano]
    ReadPrec Peano
    Int -> ReadS Peano
    ReadS [Peano]
    (Int -> ReadS Peano)
    -> ReadS [Peano]
    -> ReadPrec Peano
    -> ReadPrec [Peano]
    -> Read Peano
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    $creadsPrec :: Int -> ReadS Peano
    readsPrec :: Int -> ReadS Peano
    $creadList :: ReadS [Peano]
    readList :: ReadS [Peano]
    $creadPrec :: ReadPrec Peano
    readPrec :: ReadPrec Peano
    $creadListPrec :: ReadPrec [Peano]
    readListPrec :: ReadPrec [Peano]
    Read, Int -> Peano -> ShowS
    [Peano] -> ShowS
    Peano -> String
    (Int -> Peano -> ShowS)
    -> (Peano -> String) -> ([Peano] -> ShowS) -> Show Peano
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Peano -> ShowS
    showsPrec :: Int -> Peano -> ShowS
    $cshow :: Peano -> String
    show :: Peano -> String
    $cshowList :: [Peano] -> ShowS
    showList :: [Peano] -> ShowS
    Show)

    instance Enum Peano where
        succ :: Peano -> Peano
    succ = Peano -> Peano
    Succ

        pred :: Peano -> Peano
    pred (Succ Peano
    n) = Peano
    n
        pred Peano
    Zero     = String -> Peano
    forall a. HasCallStack => String -> a
    error String
    "Data.Peano.pred Zero"

        toEnum :: Int -> Peano
    toEnum   = Integer -> Peano
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Peano) -> (Int -> Integer) -> Int -> Peano
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Integer
    forall a. Enum a => Int -> a
    toEnum

        fromEnum :: Peano -> Int
    fromEnum = Integer -> Int
    forall a. Enum a => a -> Int
    fromEnum (Integer -> Int) -> (Peano -> Integer) -> Peano -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Peano -> Integer
    forall a. Integral a => a -> Integer
    toInteger

    instance Bounded Peano where
        minBound :: Peano
    minBound = Peano
    Zero
        maxBound :: Peano
    maxBound = Peano
    infinity

    instance Ix Peano where
        range :: (Peano, Peano) -> [Peano]
    range            = (Peano -> Peano -> [Peano]) -> (Peano, Peano) -> [Peano]
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Peano -> Peano -> [Peano]
    forall a. Enum a => a -> a -> [a]
    enumFromTo
        index :: (Peano, Peano) -> Peano -> Int
    index (Peano
    l, Peano
    _) Peano
    n   = Peano -> Int
    forall a. Enum a => a -> Int
    fromEnum (Peano
    n Peano -> Peano -> Peano
    forall a. Num a => a -> a -> a
    - Peano
    l)
        inRange :: (Peano, Peano) -> Peano -> Bool
    inRange (Peano
    l, Peano
    u) Peano
    n = Peano
    l Peano -> Peano -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Peano
    n Bool -> Bool -> Bool
    && Peano
    u Peano -> Peano -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Peano
    n
        rangeSize :: (Peano, Peano) -> Int
    rangeSize (Peano
    l, Peano
    u) = Peano -> Int
    forall a. Enum a => a -> Int
    fromEnum (Peano -> Peano
    Succ Peano
    u Peano -> Peano -> Peano
    forall a. Num a => a -> a -> a
    - Peano
    l)

    instance Num Peano where
        Peano
    Zero   + :: Peano -> Peano -> Peano
    + Peano
    n = Peano
    n
        Succ Peano
    m + Peano
    n = Peano -> Peano
    Succ (Peano
    m Peano -> Peano -> Peano
    forall a. Num a => a -> a -> a
    + Peano
    n)

        Peano
    m      - :: Peano -> Peano -> Peano
    - Peano
    Zero   = Peano
    m
        Succ Peano
    m - Succ Peano
    n = Peano
    m Peano -> Peano -> Peano
    forall a. Num a => a -> a -> a
    - Peano
    n
        Peano
    Zero   - Peano
    _      = String -> Peano
    forall a. HasCallStack => String -> a
    error String
    "Data.Peano.(-): underflow (negative)"

        Peano
    Zero   * :: Peano -> Peano -> Peano
    * Peano
    _ = Peano
    Zero
        Succ Peano
    m * Peano
    n = Peano
    n Peano -> Peano -> Peano
    forall a. Num a => a -> a -> a
    + Peano
    m Peano -> Peano -> Peano
    forall a. Num a => a -> a -> a
    * Peano
    n

        abs :: Peano -> Peano
    abs = Peano -> Peano
    forall a. a -> a
    id

        signum :: Peano -> Peano
    signum Peano
    Zero = Peano
    Zero
        signum Peano
    _    = Peano -> Peano
    Succ Peano
    Zero

        fromInteger :: Integer -> Peano
    fromInteger Integer
    n =
          case Integer -> Integer -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Integer
    n Integer
    0 of
            Ordering
    LT -> String -> Peano
    forall a. HasCallStack => String -> a
    error String
    "fromInteger n | n < 0"
            Ordering
    EQ -> Peano
    Zero
            Ordering
    GT -> Peano -> Peano
    Succ (Integer -> Peano
    forall a. Num a => Integer -> a
    fromInteger (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1))

    instance Real Peano where
        toRational :: Peano -> Rational
    toRational = Integer -> Rational
    forall a. Real a => a -> Rational
    toRational (Integer -> Rational) -> (Peano -> Integer) -> Peano -> Rational
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Peano -> Integer
    forall a. Integral a => a -> Integer
    toInteger

    instance Integral Peano where
        toInteger :: Peano -> Integer
    toInteger Peano
    Zero     = Integer
    0
        toInteger (Succ Peano
    n) = Peano -> Integer
    forall a. Integral a => a -> Integer
    toInteger Peano
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1

        Peano
    Zero quotRem :: Peano -> Peano -> (Peano, Peano)
    `quotRem` Peano
    Zero   = String -> (Peano, Peano)
    forall a. HasCallStack => String -> a
    error String
    "Data.Peano.quotRem: zero divided by zero"
        Peano
    m    `quotRem` Peano
    n      =
          case Peano -> Peano -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Peano
    m Peano
    n of
            Ordering
    LT -> (Peano
    Zero, Peano
    m)
            Ordering
    _  -> let (Peano
    q, Peano
    r) = Peano -> Peano -> (Peano, Peano)
    forall a. Integral a => a -> a -> (a, a)
    quotRem (Peano
    m Peano -> Peano -> Peano
    forall a. Num a => a -> a -> a
    - Peano
    n) Peano
    n in (Peano -> Peano
    Succ Peano
    q, Peano
    r)

        divMod :: Peano -> Peano -> (Peano, Peano)
    divMod = Peano -> Peano -> (Peano, Peano)
    forall a. Integral a => a -> a -> (a, a)
    quotRem

    -- | The infinite number (ω).
    infinity :: Peano
    infinity :: Peano
    infinity = Peano -> Peano
    Succ Peano
    infinity