ModuleChasingBottoms-1.3.1.16Haskell2010

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.

1 type
4 values

PackageChasingBottoms-1.3.1.16
Exports5
LanguageHaskell2010
LicenceMIT
SourceNat.hs

newtypenewtype Nat

Natural numbers.

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

Instances9Enum, Eq, Integral, Num, Ord, Real, …

Enum NatDefined in ChasingBottoms-1.3.1.16 · Test.ChasingBottoms.Nat
Eq NatDefined in ChasingBottoms-1.3.1.16 · Test.ChasingBottoms.Nat
Integral NatDefined in ChasingBottoms-1.3.1.16 · Test.ChasingBottoms.Nat
Num NatDefined in ChasingBottoms-1.3.1.16 · Test.ChasingBottoms.Nat
Ord NatDefined in ChasingBottoms-1.3.1.16 · Test.ChasingBottoms.Nat
Real NatDefined in ChasingBottoms-1.3.1.16 · Test.ChasingBottoms.Nat
Show NatDefined in ChasingBottoms-1.3.1.16 · Test.ChasingBottoms.Nat
Arbitrary NatDefined in ChasingBottoms-1.3.1.16 · Test.ChasingBottoms.Nat
CoArbitrary NatDefined in ChasingBottoms-1.3.1.16 · Test.ChasingBottoms.Nat

valueisSucc :: Nat -> Bool

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

valuefromSucc :: Nat -> Maybe Nat

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

valuenatrec :: a -> (Nat -> a -> a) -> Nat -> a

natrec performs primitive recursion on natural numbers.

valuefoldN :: a -> (a -> a) -> Nat -> a

foldN is a fold on natural numbers:

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