peano-inf-0.3: Lazy Peano numbers including observable infinity value.

Portability portable experimental divip@aszt.inf.elte.hu

Number.Peano.Inf

Description

Lazy Peano numbers including observable infinity value.

Note that the following equation does not hold for this number type:

• `1 + a > a`, because `1 + infinity == infinity`.

The following operation is undefined:

• `infinity - infinity`

There are variants of `(-)` with different behaviour regarding this, see below.

The following operations are naturally undefined:

• `fromEnum infinity`
• `toInteger infinity`
• `0 - n`, if `n > 0`
• `fromInteger n`, if `n < 0`
• `toEnum n`, if `n < 0`
• `pred 0`

Synopsis

# Documentation

data Nat Source

Natural numbers and infinity.

Instances

 Bounded Nat Enum Nat Eq Nat Integral Nat Num Nat Ord Nat Real Nat Show Nat

Observable infinity value.

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.

Arguments

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

Variant of `diff`: `zeroDiff infinity infinity == Left 0`.

Arguments

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

Variant of `diff`: `infDiff infinity infinity == Left infinity`.

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

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