ChasingBottoms- For testing partial and infinite values.

Portabilitynon-portable (GHC-specific)



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.



data Nat Source

Natural numbers.

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

isSucc :: Nat -> BoolSource

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

fromSucc :: Nat -> Maybe NatSource

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

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

natrec performs primitive recursion on natural numbers.

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

foldN is a fold on natural numbers:

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