The implementations of all functions are supposed to be as non-strict as possible. This is non-trivial as for example a naive implementation of (*) yields O _|_ for the application I _|_ * O IHi while a least-strict version yields O (I _|_). Also the naive / standard implementations of (-), compare, (<), (<=), (>), (>=) are more strict than necessary.
Datatype
A binary representation of natural numbers which starts with the least significant bit.
Helper Functions
cmpNatLT :: Nat -> Nat -> OrderingSource
This function is used to implement lazy instances of compare and (<), (<=), (>), (>=). It is used to transfer information to more significant bits. Instead of yielding EQ it yields LT if the numbers are equal.
invOrd :: Ordering -> OrderingSource
Maps LT to GT and GT to LT. It is used instead of defining a function cmpNatGT.