Chasing BottomsContentsIndex
Test.ChasingBottoms.Nat
Portabilitynon-portable (GHC-specific)
Stabilityexperimental
Maintainerhttp://www.cs.chalmers.se/~nad/
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
data Nat
isSucc :: Nat -> Bool
fromSucc :: Nat -> Maybe Nat
natrec :: a -> (Nat -> a -> a) -> Nat -> a
foldN :: a -> (a -> a) -> Nat -> a
Documentation
data Nat

Natural numbers.

No Data instance is provided since the implementation should be abstract.

show/hide Instances
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)
Produced by Haddock version 0.7