Add SplitLaws, SplitTests, and SplitSyntax #232
Conversation
|
I think I've derived the So every |
|
Seems good to me 👍 |
| def eqv(x: (A, B), y: (A, B)): Boolean = | ||
| A.eqv(x._1, y._1) && B.eqv(x._2, y._2) | ||
| } | ||
|
|
There was a problem hiding this comment.
Should this be defined in the std module instead of in laws?
There was a problem hiding this comment.
Oh I see the issue is that laws currently doesn't depend on std does it?
There was a problem hiding this comment.
That instance is required in tests but defined in laws because the Eq[A => B] instance was already there. I think it should ultimately come from algebra.std. Guess I need to open a PR there.
I'd like to not hold up this PR by waiting until this instance appears in algebra.
There was a problem hiding this comment.
I agree that it's smart to define the instances we need here, and then remove them when algebra adds them.
|
👍 |
Add SplitLaws, SplitTests, and SplitSyntax
This PR adds
SplitLaws,SplitTests, andSplitSyntax. I'm submitting this PR although I'm not totally confident that thesplitInterchangelaw I've defined is sound. I just tried to relatesplitwithandThenin a minimal fashion. I've not seen this law anywhere else and I still want to check if it can be derived from the arrow laws.Anyone know where
Splitis originally coming from and which laws it should obey?