# 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)
 ```add :: Nat -> Nat -> Nat```    Addition on natural numbers. Further infos: solution complete, i.e., able to compute all solutions
 ```sub :: Nat -> Nat -> Nat```    Subtraction defined by reversing addition.
 ```mul :: Nat -> Nat -> Nat```    Multiplication on natural numbers. Further infos: solution complete, i.e., able to compute all solutions
 ```leq :: Nat -> Nat -> Bool```    Further infos: solution complete, i.e., able to compute all solutions