module Stdlib.Data.Nat;
  open import Stdlib.Data.String;

  builtin nat inductive Nat {
    zero : Nat;
    suc : Nat  Nat;
  };

  infixl 6 +;
  builtin nat-plus + : Nat  Nat  Nat;
  + zero b := b;
  + (suc a) b := suc (a + b);

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

  one : Nat;
  one := suc zero;

  two : Nat;
  two := suc one;

  three : Nat;
  three := suc two;

  four : Nat;
  four := suc three;

  five : Nat;
  five := suc four;

  six : Nat;
  six := suc five;

  seven : Nat;
  seven := suc six;

  eight : Nat;
  eight := suc seven;

  nine : Nat;
  nine := suc eight;

  axiom natToStr : Nat  String;

  compile natToStr {
    c  "intToStr";
  };
end;