ChasingBottoms-1.3.1.6: For testing partial and infinite values.

Copyright | (c) Nils Anders Danielsson 2004-2019
License | See the file LICENCE.
Maintainer | http://www.cse.chalmers.se/~nad/
Stability | experimental
Portability | non-portable (GHC-specific)
Safe Haskell | None
Language | Haskell98

Test.ChasingBottoms.Nat

Description

A simple implementation of natural numbers on top of `Integer`s. Note that since `Integer`s are used there is no infinite natural number; in other words, `succ` is strict.

Synopsis

- data Nat
- isSucc :: Nat -> Bool
- fromSucc :: Nat -> Maybe Nat
- natrec :: a -> (Nat -> a -> a) -> Nat -> a
- foldN :: a -> (a -> a) -> Nat -> a

# Documentation

data Nat Source #

Natural numbers.

No `Data` instance is provided, because the implementation should be abstract.

Instances

Enum Nat Source # |
Instance details Defined in Test.ChasingBottoms.Nat Methods succ :: Nat -> Nat Source # pred :: Nat -> Nat Source # toEnum :: Int -> Nat Source # fromEnum :: Nat -> Int Source # enumFrom :: Nat -> [Nat] Source # enumFromThen :: Nat -> Nat -> [Nat] Source # enumFromTo :: Nat -> Nat -> [Nat] Source # enumFromThenTo :: Nat -> Nat -> Nat -> [Nat] Source #
Eq Nat Source # |
Instance details Defined in Test.ChasingBottoms.Nat Methods (==) :: Nat -> Nat -> Bool Source # (/=) :: Nat -> Nat -> Bool Source #
Integral Nat Source # |
Instance details Defined in Test.ChasingBottoms.Nat Methods quot :: Nat -> Nat -> Nat Source # rem :: Nat -> Nat -> Nat Source # div :: Nat -> Nat -> Nat Source # mod :: Nat -> Nat -> Nat Source # quotRem :: Nat -> Nat -> (Nat, Nat) Source # divMod :: Nat -> Nat -> (Nat, Nat) Source # toInteger :: Nat -> Integer Source #
Num Nat Source # |
Instance details Defined in Test.ChasingBottoms.Nat Methods (+) :: Nat -> Nat -> Nat Source # (-) :: Nat -> Nat -> Nat Source # (*) :: Nat -> Nat -> Nat Source # negate :: Nat -> Nat Source # abs :: Nat -> Nat Source # signum :: Nat -> Nat Source # fromInteger :: Integer -> Nat Source #
Ord Nat Source # |
Instance details Defined in Test.ChasingBottoms.Nat Methods compare :: Nat -> Nat -> Ordering Source # (<) :: Nat -> Nat -> Bool Source # (<=) :: Nat -> Nat -> Bool Source # (>) :: Nat -> Nat -> Bool Source # (>=) :: Nat -> Nat -> Bool Source # max :: Nat -> Nat -> Nat Source # min :: Nat -> Nat -> Nat Source #
Real Nat Source # |
Instance details Defined in Test.ChasingBottoms.Nat Methods toRational :: Nat -> Rational Source #
Show Nat Source # |
Instance details Defined in Test.ChasingBottoms.Nat Methods showsPrec :: Int -> Nat -> ShowS Source # show :: Nat -> String Source # showList :: [Nat] -> ShowS Source #
Arbitrary Nat Source # |
Instance details Defined in Test.ChasingBottoms.Nat Methods arbitrary :: Gen Nat Source # shrink :: Nat -> [Nat] Source #
CoArbitrary Nat Source # |
Instance details Defined in Test.ChasingBottoms.Nat Methods coarbitrary :: Nat -> Gen b -> Gen b Source #

isSucc :: Nat -> Bool Source #

``isSucc` 0 == `False``, for other total natural numbers it is `True`.

fromSucc :: Nat -> Maybe Nat Source #

``fromSucc` 0 == `Nothing``, ``fromSucc` (n+1) == `Just` n` for a total natural number `n`.

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

`natrec` performs primitive recursion on natural numbers.

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

`foldN` is a fold on natural numbers:

     foldN g h = natrec g (curry $ h . snd)