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 Source
Eq Nat Source
Integral Nat Source
Num Nat Source
Ord Nat Source
Real Nat Source
Show Nat Source
Arbitrary Nat Source
CoArbitrary Nat 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)