module Stdlib.Data.Product;

import Stdlib.Data.Product.Base open public;
import Stdlib.Data.Bool.Base open;
import Stdlib.Data.String.Base open;

import Stdlib.Trait.Eq open;
import Stdlib.Trait.Ord open;
import Stdlib.Trait.Show open;

instance
eqProductI {A B} : {{Eq A}} -> {{Eq B}} -> Eq (A × B)
  | {{mkEq eq-a}} {{mkEq eq-b}} :=
    mkEq λ {(a1, b1) (a2, b2) := eq-a a1 a2 && eq-b b1 b2};

instance
ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (A × B)
  | {{mkOrd cmp-a}} {{mkOrd cmp-b}} :=
    mkOrd
      λ {(a1, b1) (a2, b2) :=
        case cmp-a a1 a2 of {
          | LT := LT
          | GT := GT
          | EQ := cmp-b b1 b2
        }};

instance
showProductI {A B} : {{Show A}} -> {{Show B}} -> Show (A × B)
  | {{mkShow show-a}} {{mkShow show-b}} :=
    mkShow
      λ {(a, b) := "(" ++str show-a a ++str " , " ++str show-b b ++str ")"};