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