Module Data.Nat

Exported Datatypes

Natural numbers defined in Peano representation. Thus, each natural number is constructor by a Z (zero) or S (successor) constructor.

Constructors:

• Z :: Nat
• S :: Nat -> Nat

Known instances:

• Show Nat
• Read Nat
• Num Nat
• Eq Nat

Exported Functions

fromNat :: Nat -> Int   

Transforms a natural number into a standard integer.

Postcondition:

n = fromNat _ satisfies n >= 0(fromNat'post)

toNat :: Int -> Nat   

Transforms a standard integer into a natural number.

Precondition:

(toNat n) requires n >= 0(toNat'pre)

Properties:

toNat (fromNat n) -=- n(fromToNat)
(n >= 0) ==> (fromNat (toNat n) -=- n)(toFromNat)

Further infos:

• partially defined

add :: Nat -> Nat -> Nat   

Addition on natural numbers.

Properties:

add x y -=- add y x(addIsCommutative)
add (add x y) z -=- add x (add y z)(addIsAssociative)

Further infos:

• solution complete, i.e., able to compute all solutions

sub :: Nat -> Nat -> Nat   

Subtraction defined by reversing addition.

Properties:

sub (add x y) x -=- y(subAddL)
sub (add x y) y -=- x(subAddR)

mul :: Nat -> Nat -> Nat   

Multiplication on natural numbers.

Properties:

mul x y -=- mul y x(mulIsCommutative)
mul (mul x y) z -=- mul x (mul y z)(mulIsAssociative)
mul x (add y z) -=- add (mul x y) (mul x z)(distMulAddL)
mul (add y z) x -=- add (mul y x) (mul z x)(distMulAddR)

Further infos:

• solution complete, i.e., able to compute all solutions

leq :: Nat -> Nat -> Bool   

Properties:

always $ leq x (add x y)(leqAdd)

Further infos:

• solution complete, i.e., able to compute all solutions