Library defining natural numbers in Peano representation and some operations on this representation.
Author: Michael Hanus
Version: May 2016
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
|
Natural numbers defined in Peano representation.
Constructors:
Z
:: Nat
S
:: Nat -> Nat
Transforms a natural number into a standard integer.
|
Transforms a standard integer into a natural number.
|
Addition on natural numbers.
|
Subtraction defined by reversing addition. |
Multiplication on natural numbers.
|