- Bin : Type
Bin represents binary numbers right-to-left.
For instance `4` can be represented as `OOI`.
Note that representations are not unique: one may append arbitrarily
many Os to the right of the representation without changing the meaning.
- suc : Bin -> Bin
Successor function on binary numbers.
Amortised constant time.
- sucCorrect : toNat (suc bs) = S (toNat bs)
Correctness proof of `suc` with respect to the semantics in terms of Nat
- toNat : Bin -> Nat
Conversion from lists of bits to natural number.