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