module Stdlib.Data.Int.Ord;

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

import Stdlib.Data.Nat.Ord as Nat;

infix 4 ==;
--- Tests for equality.
builtin int-eq
== : Int -> Int -> Bool;
== (ofNat m) (ofNat n) := m Nat.== n;
== (negSuc m) (negSuc n) := m Nat.== n;
== _ _ := false;

infix 4 /=;
--- Tests for inequality.
/= : Int -> Int -> Bool;
/= m n := not (m == n);

infix 4 <=;
--- Returns ;true; iff the first element is less than or equal to the second.
builtin int-le
<= : Int -> Int -> Bool;
<= m n := nonNeg (n - m);

infix 4 <;
--- Returns ;true; iff the first element is less than the second.
builtin int-lt
< : Int -> Int -> Bool;
< m n := m + 1 <= n;

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

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

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

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

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