Portability  portable 

Stability  experimental 
Maintainer  divip@aszt.inf.elte.hu 
Lazy Peano numbers including observable infinity value.
Properties of Num
can be found in the source of Number.Peano.Inf.Test
.
The lazy operations of Num
makes it ideal for lazy list length computation. For example, (genericLength [1..] :: Nat) > 100
is True
.
Documentation
Natural numbers and infinity.
inductive_infinity :: NatSource
Traditional infinity value: let n = Succ n in n
.
For every function f :: Nat > Bool
, f infinity
and f inductive_infinity
gives the same result, provided that
the results are not bottom.
Use infinity
instead. Lots of the given properties of infinity
is not true for inductive_infinity
. For example,

inductive_infinity == inductive_infinity
is an endless computation instead ofTrue
.
However, the following values are True
:

n < inductive_infinity
,n
= 0, 1, 2,...
Note also:

inductive_infinity == infinity
is an endless computation instead ofTrue
.
Difference of two natural numbers: the result is either positive or negative.
implementation of ()
is based on diff
.
The following value is undefined:
diff infinity infinity
Variant of diff
:

zeroDiff infinity infinity == Left 0
.
Note that if the implementation of ()
would be based on zeroDiff
, the following equations would not hold:

(a  b)  (a  c) == c  b
,a >= c >= b
, because(infininty  5)  (infinity  10) == 0 /= 10  5
. 
a  (a  b) == b
,a >= b
, becauseinfininty  (infinity  5) == 0 /= 5
.
Variant of diff
:

infDiff infinity infinity == Left infinity
.
Note that if the implementation of ()
would be based on infDiff
, the following equations would not hold:

(a  b)  (a  c) == c  b
,a >= c >= b
, because(infininty  5)  (infinity  10) == infinity /= 10  5
. 
a  (a  b) == b
,a >= b
, becauseinfininty  (infinity  5) == infinity /= 5
.