Lazy Peano numbers including observable infinity value.
Nat can be found in the source of Number.Peano.Inf.Test.
Natural numbers and infinity.
Traditional infinity value:
let n = Succ n in n.
infinity is equal to
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
Difference of two natural numbers: the result is either positive or negative.
The following value is undefined:
diff infinity infinity
zeroDiff infinity infinity == Left 0.
infDiff infinity infinity == Left infinity.