Idris2Doc : Data.Binary

Data.Binary

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.
Totality: total
suc : Bin -> Bin
Successor function on binary numbers.
Amortised constant time.
Totality: total
sucCorrect : toNat (sucbs) = S (toNatbs)
Correctness proof of `suc` with respect to the semantics in terms of Nat
Totality: total
toNat : Bin -> Nat
Conversion from lists of bits to natural number.
Totality: total