Data.Binary

Definitions

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
Visibility: public export

toNat : Bin -> Nat

  Conversion from lists of bits to natural number.

Totality: total
Visibility: public export

suc : Bin -> Bin

  Successor function on binary numbers.
  Amortised constant time.

Totality: total
Visibility: public export

sucCorrect : toNat (suc bs) = S (toNat bs)

  Correctness proof of `suc` with respect to the semantics in terms of Nat

Totality: total
Visibility: export