Copyright	(c) Nils Anders Danielsson 2004-2021
License	See the file LICENCE.
Maintainer	http://www.cse.chalmers.se/~nad/
Stability	experimental
Portability	non-portable (GHC-specific)
Safe Haskell	None
Language	Haskell2010

Test.ChasingBottoms.Nat

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 Source #

Natural numbers.

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

Instances

Instances details

Enum Nat Source #
Instance details 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 Source #
Instance details Defined in Test.ChasingBottoms.Nat Methods (==) :: Nat -> Nat -> Bool # (/=) :: Nat -> Nat -> Bool #
Integral Nat Source #
Instance details 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 Source #
Instance details 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 Source #
Instance details 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 Source #
Instance details Defined in Test.ChasingBottoms.Nat Methods toRational :: Nat -> Rational #
Show Nat Source #
Instance details Defined in Test.ChasingBottoms.Nat Methods showsPrec :: Int -> Nat -> ShowS # show :: Nat -> String # showList :: [Nat] -> ShowS #
Arbitrary Nat Source #
Instance details Defined in Test.ChasingBottoms.Nat Methods arbitrary :: Gen Nat # shrink :: Nat -> [Nat] #
CoArbitrary Nat Source #
Instance details Defined in Test.ChasingBottoms.Nat Methods coarbitrary :: Nat -> Gen b -> Gen b #

isSucc :: Nat -> Bool Source #

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

fromSucc :: Nat -> Maybe Nat Source #

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

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

natrec performs primitive recursion on natural numbers.

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

foldN is a fold on natural numbers:

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