peano-inf-0.6.5: 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

Variant of diff:

• zeroDiff infinity infinity == Left 0.

Variant of diff:

• infDiff infinity infinity == Left infinity.

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

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