Deriving Eq

Stdlib/Data/Bool.juvix

@@ -8,15 +8,8 @@ import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 
 {-# specialize: true, inline: case #-}
-instance
-eqBoolI : Eq Bool :=
-  mkEq@{
-    eq (x y : Bool) : Bool :=
-      case x, y of
-        | true, true := true
-        | false, false := true
-        | _ := false;
-  };
+deriving instance
+eqBoolI : Eq Bool;
 
 {-# specialize: true, inline: case #-}
 instance

Stdlib/Data/Maybe.juvix

@@ -14,15 +14,8 @@ import Stdlib.Data.String.Base open;
 import Stdlib.Data.Pair.Base open;
 
 {-# specialize: true, inline: case #-}
-instance
-eqMaybeI {A} {{Eq A}} : Eq (Maybe A) :=
-  mkEq@{
-    eq (m1 m2 : Maybe A) : Bool :=
-      case m1, m2 of
-        | nothing, nothing := true
-        | just a1, just a2 := Eq.eq a1 a2
-        | _ := false;
-  };
+deriving instance
+eqMaybeI {A} {{Eq A}} : Eq (Maybe A);
 
 instance
 showMaybeI {A} {{Show A}} : Show (Maybe A) :=

Stdlib/Data/Pair.juvix

@@ -9,13 +9,8 @@ import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 
 {-# specialize: true, inline: case #-}
-instance
-eqProductI {A B} : {{Eq A}} -> {{Eq B}} -> Eq (Pair A B)
-  | {{mkEq eqA}} {{mkEq eqB}} :=
-    mkEq@{
-      eq (p1 p2 : Pair A B) : Bool :=
-        case p1, p2 of (a1, b1), a2, b2 := eqA a1 a2 && eqB b1 b2;
-    };
+deriving instance
+eqProductI {A B} {{Eq A}} {{Eq B}} : Eq (Pair A B);
 
 {-# specialize: true, inline: case #-}
 instance

Stdlib/Data/Result.juvix

@@ -24,15 +24,8 @@ ordResultI
   };
 
 {-# specialize: true, inline: case #-}
-instance
-eqResultI {Error Value} {{Eq Error}} {{Eq Value}} : Eq (Result Error Value) :=
-  mkEq@{
-    eq (result1 result2 : Result Error Value) : Bool :=
-      case result1, result2 of
-        | error a1, error a2 := a1 == a2
-        | ok b1, ok b2 := b1 == b2
-        | _, _ := false;
-  };
+deriving instance
+eqResultI {Error Value} {{Eq Error}} {{Eq Value}} : Eq (Result Error Value);
 
 instance
 showResultI

Stdlib/Data/Unit.juvix

@@ -10,11 +10,8 @@ import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 import Stdlib.Trait.Foldable open;
 
-instance
-eqUnitI : Eq Unit :=
-  mkEq@{
-    eq (_ _ : Unit) : Bool := true;
-  };
+deriving instance
+eqUnitI : Eq Unit;
 
 instance
 ordUnitI : Ord Unit :=

Stdlib/Trait/Eq.juvix

@@ -4,8 +4,9 @@ import Stdlib.Data.Bool.Base open;
 import Stdlib.Data.Fixity open;
 
 --- A trait defining equality
+builtin eq
 trait
-type Eq A := mkEq@{eq : A -> A -> Bool};
+type Eq A := mkEq@{builtin isEqual eq : A -> A -> Bool};
 
 syntax operator == comparison;
 syntax operator /= comparison;

Stdlib/Trait/Ord.juvix

@@ -24,15 +24,8 @@ isGreaterThan (ordering : Ordering) : Bool :=
     | GreaterThan := true
     | _ := false;
 
-instance
-orderingEqI : Eq Ordering :=
-  mkEq@{
-    eq (ordering1 ordering2 : Ordering) : Bool :=
-      case ordering2 of
-        | LessThan := isLessThan ordering1
-        | Equal := isEqual ordering1
-        | GreaterThan := isGreaterThan ordering1;
-  };
+deriving instance
+orderingEqI : Eq Ordering;
 
 --- A trait for defining a total order
 trait