# Module Data.Nat

Library defining natural numbers in Peano representation and some operations on this representation.

Author: Michael Hanus

Version: January 2019

## Summary of exported operations:

 ```fromNat :: Nat -> Int```    Transforms a natural number into a standard integer. ```toNat :: Int -> Nat```    Transforms a standard integer into a natural number. ```add :: Nat -> Nat -> Nat```    Addition on natural numbers. ```sub :: Nat -> Nat -> Nat```    Subtraction defined by reversing addition. ```mul :: Nat -> Nat -> Nat```    Multiplication on natural numbers. ```leq :: Nat -> Nat -> Bool```

## Exported datatypes:

Nat

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```

## Exported operations:

 ```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)
 ```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