peano-inf-0.6.1: 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.

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

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 Serial Nat

Observable infinity value.

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`.

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`

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`.