ChasingBottoms-1.3.1.2: For testing partial and infinite values.

Copyright(c) Nils Anders Danielsson 2004-2016
LicenseSee the file LICENCE.
Maintainerhttp://www.cse.chalmers.se/~nad/
Stabilityexperimental
Portabilitynon-portable (GHC-specific)
Safe HaskellNone
LanguageHaskell98

Test.ChasingBottoms.Nat

Description

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

Synopsis

Documentation

data Nat Source #

Natural numbers.

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

Instances

Enum Nat Source # 

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

Eq Nat Source # 

Methods

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

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

Integral Nat Source # 

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 #

Num Nat Source # 

Methods

(+) :: Nat -> Nat -> Nat #

(-) :: Nat -> Nat -> Nat #

(*) :: Nat -> Nat -> Nat #

negate :: Nat -> Nat #

abs :: Nat -> Nat #

signum :: Nat -> Nat #

fromInteger :: Integer -> Nat #

Ord Nat Source # 

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 #

Real Nat Source # 

Methods

toRational :: Nat -> Rational #

Show Nat Source # 

Methods

showsPrec :: Int -> Nat -> ShowS #

show :: Nat -> String #

showList :: [Nat] -> ShowS #

Arbitrary Nat Source # 

Methods

arbitrary :: Gen Nat #

shrink :: Nat -> [Nat] #

CoArbitrary Nat Source # 

Methods

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

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)