Copyright	(c) Nils Anders Danielsson 2004-2015
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 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
Eq Nat
Integral Nat
Num Nat
Ord Nat
Real Nat
Show Nat
CoArbitrary Nat
Arbitrary Nat
Typeable * Nat

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)