This repository was archived by the owner on Feb 8, 2022. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 64
WIP: Switch laws to cats-core encoding #206
Closed
Closed
Changes from all commits
Commits
Show all changes
3 commits
Select commit
Hold shift + click to select a range
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
13 changes: 13 additions & 0 deletions
13
laws/src/main/scala/algebra/laws/AdditiveCommutativeGroupLaws.scala
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| package algebra | ||
| package laws | ||
|
|
||
| import algebra.ring._ | ||
|
|
||
| trait AdditiveCommutativeGroupLaws[A] extends AdditiveGroupLaws[A] with AdditiveCommutativeMonoidLaws[A] { | ||
| override implicit def S: AdditiveCommutativeGroup[A] | ||
| } | ||
|
|
||
| object AdditiveCommutativeGroupLaws { | ||
| def apply[A](implicit ev: AdditiveCommutativeGroup[A]): AdditiveCommutativeGroupLaws[A] = | ||
| new AdditiveCommutativeGroupLaws[A] { def S: AdditiveCommutativeGroup[A] = ev } | ||
| } |
13 changes: 13 additions & 0 deletions
13
laws/src/main/scala/algebra/laws/AdditiveCommutativeMonoidLaws.scala
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| package algebra | ||
| package laws | ||
|
|
||
| import algebra.ring._ | ||
|
|
||
| trait AdditiveCommutativeMonoidLaws[A] extends AdditiveMonoidLaws[A] with AdditiveCommutativeSemigroupLaws[A] { | ||
| override implicit def S: AdditiveCommutativeMonoid[A] | ||
| } | ||
|
|
||
| object AdditiveCommutativeMonoidLaws { | ||
| def apply[A](implicit ev: AdditiveCommutativeMonoid[A]): AdditiveCommutativeMonoidLaws[A] = | ||
| new AdditiveCommutativeMonoidLaws[A] { def S: AdditiveCommutativeMonoid[A] = ev } | ||
| } |
19 changes: 19 additions & 0 deletions
19
laws/src/main/scala/algebra/laws/AdditiveCommutativeSemigroupLaws.scala
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,19 @@ | ||
| package algebra | ||
| package laws | ||
|
|
||
| import algebra.ring._ | ||
| import cats.kernel.laws._ | ||
|
|
||
|
|
||
| trait AdditiveCommutativeSemigroupLaws[A] extends AdditiveSemigroupLaws[A] { | ||
| override implicit def S: AdditiveCommutativeSemigroup[A] | ||
|
|
||
| def plusCommutative(x: A, y: A): IsEq[A] = | ||
| S.plus(x, y) <-> S.plus(y, x) | ||
|
|
||
| } | ||
|
|
||
| object AdditiveCommutativeSemigroupLaws { | ||
| def apply[A](implicit ev: AdditiveCommutativeSemigroup[A]): AdditiveCommutativeSemigroupLaws[A] = | ||
| new AdditiveCommutativeSemigroupLaws[A] { def S: AdditiveCommutativeSemigroup[A] = ev } | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,25 @@ | ||
| package algebra | ||
| package laws | ||
|
|
||
| import algebra.ring._ | ||
| import cats.kernel.laws._ | ||
|
|
||
|
|
||
| trait AdditiveGroupLaws[A] extends AdditiveMonoidLaws[A] { | ||
| override implicit def S: AdditiveGroup[A] | ||
|
|
||
| def leftNegate(x: A): IsEq[A] = | ||
| S.plus(S.negate(x), x) <-> S.zero | ||
|
|
||
| def rightNegate(x: A): IsEq[A] = | ||
| S.plus(x, S.negate(x)) <-> S.zero | ||
|
|
||
| def consistentMinus(x: A, y: A): IsEq[A] = | ||
| S.minus(x, y) <-> S.plus(x, S.negate(y)) | ||
|
|
||
| } | ||
|
|
||
| object AdditiveGroupLaws { | ||
| def apply[A](implicit ev: AdditiveGroup[A]): AdditiveGroupLaws[A] = | ||
| new AdditiveGroupLaws[A] { def S: AdditiveGroup[A] = ev } | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,29 @@ | ||
| package algebra.laws | ||
|
|
||
| import algebra.ring._ | ||
| import cats.kernel.Eq | ||
| import cats.kernel.laws._ | ||
|
|
||
| trait AdditiveMonoidLaws[A] extends AdditiveSemigroupLaws[A] { | ||
| override implicit def S: AdditiveMonoid[A] | ||
|
|
||
| def leftZero(a: A): IsEq[A] = | ||
| S.plus(S.zero, a) <-> a | ||
|
|
||
| def rightZero(a: A): IsEq[A] = | ||
| S.plus(a, S.zero) <-> a | ||
|
|
||
| def sumN0(a: A): IsEq[A] = | ||
| S.sumN(a, 0) <-> S.zero | ||
|
|
||
| def sumAll: IsEq[A] = | ||
| S.sum(Nil) <-> S.zero | ||
|
|
||
| def isZero(a: A, eqv: Eq[A]): IsEq[Boolean] = | ||
| eqv.eqv(a, S.zero) <-> S.isZero(a)(eqv) | ||
| } | ||
|
|
||
| object AdditiveMonoidLaws { | ||
| def apply[A](implicit ev: AdditiveMonoid[A]): AdditiveMonoidLaws[A] = | ||
| new AdditiveMonoidLaws[A] { def S: AdditiveMonoid[A] = ev } | ||
| } |
29 changes: 29 additions & 0 deletions
29
laws/src/main/scala/algebra/laws/AdditiveSemigroupLaws.scala
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,29 @@ | ||
| package algebra | ||
| package laws | ||
|
|
||
| import algebra.ring._ | ||
| import cats.kernel.laws._ | ||
|
|
||
| trait AdditiveSemigroupLaws[A] { | ||
| implicit def S: AdditiveSemigroup[A] | ||
|
|
||
| def plusAssociative(x: A, y: A, z: A): IsEq[A] = | ||
| S.plus(S.plus(x, y), z) <-> S.plus(x, S.plus(y, z)) | ||
|
|
||
| def sumN1(a: A): IsEq[A] = | ||
| S.sumN(a, 1) <-> a | ||
|
|
||
| def sumN2(a: A): IsEq[A] = | ||
| S.sumN(a, 2) <-> S.plus(a, a) | ||
|
|
||
| def sumN3(a: A): IsEq[A] = | ||
| S.sumN(a, 3) <-> S.plus(S.plus(a, a), a) | ||
|
|
||
| def trySum(xs: Vector[A]): IsEq[Option[A]] = | ||
| S.trySum(xs) <-> xs.reduceOption(S.plus) | ||
| } | ||
|
|
||
| object AdditiveSemigroupLaws { | ||
| def apply[A](implicit ev: AdditiveSemigroup[A]): AdditiveSemigroupLaws[A] = | ||
| new AdditiveSemigroupLaws[A] { def S: AdditiveSemigroup[A] = ev } | ||
| } |
13 changes: 13 additions & 0 deletions
13
laws/src/main/scala/algebra/laws/BoundedDistributiveLatticeLaws.scala
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| package algebra | ||
| package laws | ||
|
|
||
| import algebra.lattice._ | ||
|
|
||
| trait BoundedDistributiveLatticeLaws[A] extends BoundedLatticeLaws[A] with DistributiveLatticeLaws[A] { | ||
| override implicit def S: BoundedDistributiveLattice[A] | ||
| } | ||
|
|
||
| object BoundedDistributiveLatticeLaws { | ||
| def apply[A](implicit ev: BoundedDistributiveLattice[A]): BoundedDistributiveLatticeLaws[A] = | ||
| new BoundedDistributiveLatticeLaws[A] { def S: BoundedDistributiveLattice[A] = ev } | ||
| } |
13 changes: 13 additions & 0 deletions
13
laws/src/main/scala/algebra/laws/BoundedJoinLatticeLaws.scala
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| package algebra | ||
| package laws | ||
|
|
||
| import algebra.lattice._ | ||
|
|
||
| trait BoundedJoinLatticeLaws[A] extends LatticeLaws[A] with BoundedJoinSemilatticeLaws[A] { | ||
| override implicit def S: Lattice[A] with BoundedJoinSemilattice[A] | ||
| } | ||
|
|
||
| object BoundedJoinLatticeLaws { | ||
| def apply[A](implicit ev: Lattice[A] with BoundedJoinSemilattice[A]): BoundedJoinLatticeLaws[A] = | ||
| new BoundedJoinLatticeLaws[A] { def S: Lattice[A] with BoundedJoinSemilattice[A] = ev } | ||
| } |
13 changes: 13 additions & 0 deletions
13
laws/src/main/scala/algebra/laws/BoundedJoinSemilatticeLaws.scala
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| package algebra.laws | ||
|
|
||
| import algebra.lattice._ | ||
| import cats.kernel.laws.BoundedSemilatticeLaws | ||
|
|
||
| trait BoundedJoinSemilatticeLaws[A] extends JoinSemilatticeLaws[A] with BoundedSemilatticeLaws[A] { | ||
| override implicit def S: BoundedJoinSemilattice[A] | ||
| } | ||
|
|
||
| object BoundedJoinSemilatticeLaws { | ||
| def apply[A](implicit ev: BoundedJoinSemilattice[A]): BoundedJoinSemilatticeLaws[A] = | ||
| new BoundedJoinSemilatticeLaws[A] { def S: BoundedJoinSemilattice[A] = ev } | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,14 @@ | ||
| package algebra | ||
| package laws | ||
|
|
||
| import algebra.lattice._ | ||
|
|
||
| trait BoundedLatticeLaws[A] extends LatticeLaws[A] with BoundedMeetLatticeLaws[A] with BoundedJoinLatticeLaws[A] { | ||
| override implicit def S: BoundedLattice[A] | ||
| } | ||
|
|
||
| object BoundedLatticeLaws { | ||
| def apply[A](implicit ev: BoundedLattice[A]): BoundedLatticeLaws[A] = | ||
| new BoundedLatticeLaws[A] { def S: BoundedLattice[A] = ev } | ||
| } | ||
|
|
13 changes: 13 additions & 0 deletions
13
laws/src/main/scala/algebra/laws/BoundedMeetLatticeLaws.scala
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| package algebra.laws | ||
|
|
||
| import algebra.lattice._ | ||
|
|
||
| trait BoundedMeetLatticeLaws[A] extends LatticeLaws[A] with BoundedMeetSemilatticeLaws[A] { | ||
| override implicit def S: Lattice[A] with BoundedMeetSemilattice[A] | ||
| } | ||
|
|
||
| object BoundedMeetLatticeLaws { | ||
| def apply[A](implicit ev: Lattice[A] with BoundedMeetSemilattice[A]): BoundedMeetLatticeLaws[A] = | ||
| new BoundedMeetLatticeLaws[A] { def S: Lattice[A] with BoundedMeetSemilattice[A] = ev } | ||
| } | ||
|
|
13 changes: 13 additions & 0 deletions
13
laws/src/main/scala/algebra/laws/BoundedMeetSemilatticeLaws.scala
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| package algebra.laws | ||
|
|
||
| import cats.kernel.laws.BoundedSemilatticeLaws | ||
| import algebra.lattice._ | ||
|
|
||
| trait BoundedMeetSemilatticeLaws[A] extends MeetSemilatticeLaws[A] with BoundedSemilatticeLaws[A] { | ||
| override implicit def S: BoundedMeetSemilattice[A] | ||
| } | ||
|
|
||
| object BoundedMeetSemilatticeLaws { | ||
| def apply[A](implicit ev: BoundedMeetSemilattice[A]): BoundedMeetSemilatticeLaws[A] = | ||
| new BoundedMeetSemilatticeLaws[A] { def S: BoundedMeetSemilattice[A] = ev } | ||
| } |
This file was deleted.
Oops, something went wrong.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| package algebra | ||
| package laws | ||
|
|
||
| import algebra.ring._ | ||
|
|
||
| trait CommutativeRigLaws[A] extends RigLaws[A] with CommutativeSemiringLaws[A] with MultiplicativeCommutativeMonoidLaws[A] { | ||
| override implicit def S: CommutativeRig[A] | ||
| } | ||
|
|
||
| object CommutativeRigLaws { | ||
| def apply[A](implicit ev: CommutativeRig[A]): CommutativeRigLaws[A] = | ||
| new CommutativeRigLaws[A] { def S: CommutativeRig[A] = ev } | ||
| } |
13 changes: 13 additions & 0 deletions
13
laws/src/main/scala/algebra/laws/CommutativeRingLaws.scala
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| package algebra | ||
| package laws | ||
|
|
||
| import algebra.ring._ | ||
|
|
||
| trait CommutativeRingLaws[A] extends RingLaws[A] with CommutativeRigLaws[A] with CommutativeRngLaws[A] { | ||
| override implicit def S: CommutativeRing[A] | ||
| } | ||
|
|
||
| object CommutativeRingLaws { | ||
| def apply[A](implicit ev: CommutativeRing[A]): CommutativeRingLaws[A] = | ||
| new CommutativeRingLaws[A] { def S: CommutativeRing[A] = ev } | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| package algebra | ||
| package laws | ||
|
|
||
| import algebra.ring._ | ||
|
|
||
| trait CommutativeRngLaws[A] extends CommutativeSemiringLaws[A] with RngLaws[A] { | ||
| override implicit def S: CommutativeRng[A] | ||
| } | ||
|
|
||
| object CommutativeRngLaws { | ||
| def apply[A](implicit ev: CommutativeRng[A]): CommutativeRngLaws[A] = | ||
| new CommutativeRngLaws[A] { def S: CommutativeRng[A] = ev } | ||
| } |
13 changes: 13 additions & 0 deletions
13
laws/src/main/scala/algebra/laws/CommutativeSemiringLaws.scala
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| package algebra | ||
| package laws | ||
|
|
||
| import algebra.ring._ | ||
|
|
||
| trait CommutativeSemiringLaws[A] extends SemiringLaws[A] with MultiplicativeCommutativeSemigroupLaws[A] { | ||
| override implicit def S: CommutativeSemiring[A] | ||
| } | ||
|
|
||
| object CommutativeSemiringLaws { | ||
| def apply[A](implicit ev: CommutativeSemiring[A]): CommutativeSemiringLaws[A] = | ||
| new CommutativeSemiringLaws[A] { def S: CommutativeSemiring[A] = ev } | ||
| } |
20 changes: 20 additions & 0 deletions
20
laws/src/main/scala/algebra/laws/DistributiveLatticeLaws.scala
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,20 @@ | ||
| package algebra | ||
| package laws | ||
|
|
||
| import algebra.lattice._ | ||
| import cats.kernel.laws._ | ||
|
|
||
|
|
||
| trait DistributiveLatticeLaws[A] extends LatticeLaws[A] { | ||
| override implicit def S: DistributiveLattice[A] | ||
|
|
||
| def distributive(x: A, y: A, z: A)(implicit E: Eq[A]): IsEq[Boolean] = | ||
| (E.eqv(S.join(x, S.meet(y, z)), S.meet(S.join(x, y), S.join(x, z))) && | ||
| E.eqv(S.meet(x, S.join(y, z)), S.join(S.meet(x, y), S.meet(x, z)))) <-> true | ||
|
|
||
| } | ||
|
|
||
| object DistributiveLatticeLaws { | ||
| def apply[A](implicit ev: DistributiveLattice[A]): DistributiveLatticeLaws[A] = | ||
| new DistributiveLatticeLaws[A] { def S: DistributiveLattice[A] = ev } | ||
| } | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| package algebra | ||
| package laws | ||
|
|
||
| import algebra.ring._ | ||
|
|
||
| trait FieldLaws[A] extends CommutativeRingLaws[A] with MultiplicativeCommutativeGroupLaws[A] { | ||
| override implicit def S: Field[A] | ||
| } | ||
|
|
||
| object FieldLaws { | ||
| def apply[A: Field]: FieldLaws[A] = | ||
| new FieldLaws[A] { def S: Field[A] = implicitly } | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,19 @@ | ||
| package algebra.laws | ||
|
|
||
| import algebra._ | ||
| import algebra.lattice._ | ||
|
|
||
| import cats.kernel.laws._ | ||
|
|
||
|
|
||
| trait HeytingLaws[A] extends BoundedDistributiveLatticeLaws[A] { | ||
| override implicit def S: Heyting[A] | ||
|
|
||
| def absorption(x: A, y: A)(implicit E: Eq[A]): IsEq[Boolean] = | ||
| (E.eqv(S.join(x, S.meet(x, y)), x) && E.eqv(S.meet(x, S.join(x, y)), x)) <-> true | ||
| } | ||
|
|
||
| object HeytingLaws { | ||
| def apply[A](implicit ev: Heyting[A]): HeytingLaws[A] = | ||
| new HeytingLaws[A] { def S: Heyting[A] = ev } | ||
| } |
13 changes: 13 additions & 0 deletions
13
laws/src/main/scala/algebra/laws/JoinSemilatticeLaws.scala
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| package algebra.laws | ||
|
|
||
| import algebra.lattice.JoinSemilattice | ||
| import cats.kernel.laws.SemilatticeLaws | ||
|
|
||
| trait JoinSemilatticeLaws[A] extends SemilatticeLaws[A] { | ||
|
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. A |
||
| override implicit def S: JoinSemilattice[A] | ||
| } | ||
|
|
||
| object JoinSemilatticeLaws { | ||
| def apply[A](implicit ev: JoinSemilattice[A]): JoinSemilatticeLaws[A] = | ||
| new JoinSemilatticeLaws[A] { def S: JoinSemilattice[A] = ev } | ||
| } | ||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why not split in two laws that return
IsEq[A]?