module Stdlib.Data.Product;
import Stdlib.Trait.Eq as Eq;
open Eq using {Eq};
import Stdlib.Trait.Ord as Ord;
open Ord using {Ord};
import Stdlib.Trait.Show as Show;
open Show using {Show};
open import Stdlib.Data.Product.Base public;
open import Stdlib.Data.Bool.Base;
open import Stdlib.Data.String.Base;
module ProductTraits;
Eq : {A B : Type} -> Eq A -> Eq B -> Eq (A × B);
Eq (Eq.mkEq eq-a) (Eq.mkEq eq-b) :=
Eq.mkEq
λ {
| (a1, b1) (a2, b2) := eq-a a1 a2 && eq-b b1 b2
};
Ord : {A B : Type} -> Ord A -> Ord B -> Ord (A × B);
Ord (Ord.mkOrd cmp-a) (Ord.mkOrd cmp-b) :=
Ord.mkOrd
λ {
| (a1, b1) (a2, b2) :=
case cmp-a a1 a2
| Ord.LT := Ord.LT
| Ord.GT := Ord.GT
| Ord.EQ := cmp-b b1 b2
};
Show : {A B : Type} -> Show A -> Show B -> Show (A × B);
Show (Show.mkShow show-a) (Show.mkShow show-b) :=
Show.mkShow
λ {
| (a, b) := "(" ++str show-a a ++str " , " ++str show-b b ++str ")"
};
end;
Last modified on 2023-05-08 11:40 UTC