Test.ChasingBottoms.Nat

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.

Documentation

data Nat

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

Typeable Nat

Arbitrary Nat

CoArbitrary Nat

isSucc :: Nat -> Bool

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

fromSucc :: Nat -> Maybe Nat

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

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

natrec performs primitive recursion on natural numbers.

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

foldN is a fold on natural numbers:

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