module Stdlib.Data.Nat.Ord;

import Stdlib.Data.Fixity open;

import Stdlib.Data.Nat.Base open;
import Stdlib.Trait.Ord open using {Equal; LessThan; GreaterThan; Ordering};
import Stdlib.Data.Bool.Base open;

syntax operator == comparison;

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

syntax operator /= comparison;

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

syntax operator <= comparison;

--- 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;

syntax operator < comparison;

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

syntax operator > comparison;

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

syntax operator >= comparison;

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

--- Tests for ;Ordering;.
{-# inline: true #-}
compare (n m : Nat) : Ordering :=
  if 
    | n == m := Equal
    | n < m := LessThan
    | else := GreaterThan;

--- Returns the smaller ;Nat;.
min (x y : Nat) : Nat :=
  if 
    | x < y := x
    | else := y;

--- Returns the larger ;Nat;.
max (x y : Nat) : Nat :=
  if 
    | x > y := x
    | else := y;