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

Defined in Test.ChasingBottoms.Nat

Methods

succ :: Nat -> Nat

pred :: Nat -> Nat

toEnum :: Int -> Nat

fromEnum :: Nat -> Int

enumFrom :: Nat -> [Nat]

enumFromThen :: Nat -> Nat -> [Nat]

enumFromTo :: Nat -> Nat -> [Nat]

enumFromThenTo :: Nat -> Nat -> Nat -> [Nat]

Eq Nat

Defined in Test.ChasingBottoms.Nat

Methods

(==) :: Nat -> Nat -> Bool

(/=) :: Nat -> Nat -> Bool

Integral Nat

Defined in Test.ChasingBottoms.Nat

Methods

quot :: Nat -> Nat -> Nat

rem :: Nat -> Nat -> Nat

div :: Nat -> Nat -> Nat

mod :: Nat -> Nat -> Nat

quotRem :: Nat -> Nat -> (Nat, Nat)

divMod :: Nat -> Nat -> (Nat, Nat)

toInteger :: Nat -> Integer

Num Nat

Defined in Test.ChasingBottoms.Nat

Methods

(+) :: Nat -> Nat -> Nat

(-) :: Nat -> Nat -> Nat

(*) :: Nat -> Nat -> Nat

negate :: Nat -> Nat

abs :: Nat -> Nat

signum :: Nat -> Nat

fromInteger :: Integer -> Nat

Ord Nat

Defined in Test.ChasingBottoms.Nat

Methods

compare :: Nat -> Nat -> Ordering

(<) :: Nat -> Nat -> Bool

(<=) :: Nat -> Nat -> Bool

(>) :: Nat -> Nat -> Bool

(>=) :: Nat -> Nat -> Bool

max :: Nat -> Nat -> Nat

min :: Nat -> Nat -> Nat

Real Nat

Defined in Test.ChasingBottoms.Nat

Methods

toRational :: Nat -> Rational

Show Nat

Defined in Test.ChasingBottoms.Nat

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

Arbitrary Nat

Defined in Test.ChasingBottoms.Nat

Methods

arbitrary :: Gen Nat

shrink :: Nat -> [Nat]

CoArbitrary Nat

Defined in Test.ChasingBottoms.Nat

Methods

coarbitrary :: Nat -> Gen b -> Gen b

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)