Number.Peano.Inf

Lazy Peano numbers including observable infinity value.

Properties of Nat can be found in the source of Number.Peano.Inf.Test.

Documentation

data Nat

Natural numbers and infinity.

Instances

Bounded Nat

Enum Nat

Eq Nat

Integral Nat

Num Nat

Ord Nat

Real Nat

Show Nat

Serial Nat

infinity :: Nat

Observable infinity value.

inductive_infinity :: Nat

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.

diff

Arguments

:: Nat

n

-> Nat

m

-> Either Nat Nat

n >= m: Left (n-m), n < m: Right (m-n)

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 Nat

Variant of diff:

• zeroDiff infinity infinity == Left 0.

infDiff :: Nat -> Nat -> Either Nat Nat

Variant of diff:

• infDiff infinity infinity == Left infinity.

(-|) :: Nat -> Nat -> Nat

Non-negative subtraction. For example, 5 -| 8 == 0.