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.
A binary representation of natural numbers which starts with the least significant bit.
This constructor represents the most significant bit. There are no leading zero bits.
A zero bit
A one bit
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.
Maps LT to GT and GT to LT. It is used instead of defining a function cmpNat1GT.
minusNat1 x y yields x - y + 1. This is used to implement (-) for natural numbers.