Portability | portable |
---|---|
Stability | experimental |
Maintainer | divip@aszt.inf.elte.hu |
Lazy Peano numbers including observable infinity value.
Properties of Nat
can be found in the source of Number.Peano.Inf.Test.
Documentation
Natural numbers and infinity.
inductive_infinity :: NatSource
Traditional infinity value: let n = Succ n in n
.
infinity
is equal to inductive_infinity
but infinity
is lazier.
In other words:
For every function f :: Nat -> Bool
, either f inductive_infinity
is bottom or f inductive_infinity
is equal to f infinity
.
Difference of two natural numbers: the result is either positive or negative.
The following value is undefined:
diff infinity infinity
zeroDiff :: Nat -> Nat -> Either Nat NatSource
Variant of diff
:
-
zeroDiff infinity infinity == Left 0
.