module Stdlib.Data.Nat.Ord;

open import Stdlib.Data.Nat.Base;
open import Stdlib.Trait.Ord;
open import Stdlib.Data.Bool;

infix 4 ==;
--- Tests for equality.
builtin nat-eq
== : Nat → Nat → Bool;
== zero zero := true;
== zero _ := false;
== _ zero := false;
== (suc n) (suc m) := n == m;

infix 4 /=;
--- Tests for inequality.
/= : Nat → Nat → Bool;
/= x y := not (x == y);

infix 4 <=;
--- Returns ;true; iff the first element is less than or equal to the second.
builtin nat-le
<= : Nat → Nat → Bool;
<= zero _ := true;
<= _ zero := false;
<= (suc n) (suc m) := n <= m;

infix 4 <;
--- Returns ;true; iff the first element is less than the second.
builtin nat-lt
< : Nat → Nat → Bool;
< n m := suc n <= m;

infix 4 >;
--- Returns ;true; iff the first element is greater than the second.
> : Nat → Nat → Bool;
> n m := m < n;

infix 4 >=;
--- Returns ;true; iff the first element is greater than or equal to the second.
>= : Nat → Nat → Bool;
>= n m := m <= n;

--- Tests for ;Ordering;.
compare : Nat → Nat → Ordering;
compare n m := if (n == m) EQ (if (n < m) LT GT);

--- Returns the smallest ;Nat;.
min : Nat → Nat → Nat;
min x y := if (x < y) x y;

--- Returns the biggest ;Nat;.
max : Nat → Nat → Nat;
max x y := if (x > y) x y;