module Data.Nat;
  inductive ℕ  {
    zero : ℕ;
    suc : ℕ → ℕ;
  };

  infixl 6 +;
  + : ℕ → ℕ → ℕ;
  + zero b := b;
  + (suc a) b := suc (a + b);

  infixl 7 *;
  * : ℕ → ℕ → ℕ;
  * zero b := zero;
  * (suc a) b := b + a * b;

end;