module Stdlib.Data.Nat.Base;

--- Inductive natural numbers. I.e. whole non-negative numbers.
builtin nat
type Nat :=
  | zero : Nat
  | suc : Nat → Nat;

infixl 6 +;
--- Addition for ;Nat;s.
builtin nat-plus
+ : Nat → Nat → Nat;
+ zero b := b;
+ (suc a) b := suc (a + b);

infixl 7 *;
--- Multiplication for ;Nat;s.
builtin nat-mul
* : Nat → Nat → Nat;
* zero _ := zero;
* (suc a) b := b + a * b;

--- Truncated subtraction for ;Nat;s.
builtin nat-sub
sub : Nat → Nat → Nat;
sub zero _ := zero;
sub n zero := n;
sub (suc n) (suc m) := sub n m;

--- Division for ;Nat;s. Returns ;zero; if the first element is ;zero;.
builtin nat-udiv
terminating
udiv : Nat → Nat → Nat;
udiv zero _ := zero;
udiv n m := suc (udiv (sub n m) m);

--- Division for ;Nat;s.
builtin nat-div
div : Nat → Nat → Nat;
div n m := udiv (sub (suc n) m) m;

--- Modulo for ;Nat;s.
builtin nat-mod
mod : Nat → Nat → Nat;
mod n m := sub n (div n m * m);