Software Foundations: Functional Programming in Coq

Basics.v

Inductive bin : Type :=
  | bz
  | b0 (b : bin)
  | b1 (b : bin).

Fixpoint increment (b : bin) : bin :=
  match b with
  | bz => b1 bz
  | b0 b => b1 b
  | b1 b => b0 (increment b)
  end.

Fixpoint bin_to_nat (b : bin) : nat :=
  match b with
  | bz => O
  | b0 b => 2 * bin_to_nat b
  | b1 b => 1 + 2 * bin_to_nat b
  end.