Closed ocharles closed 5 years ago
In fact, I don't even need a pair, the test doesn't even work with naturals:
> lawsCheck (ordLaws (integral @_ @Natural (linear 1 100)))
✓ <interactive> passed 100 tests.
✗ <interactive> failed after 3 tests.
━━━ Context ━━━
When testing the Transitivity law(†), for the Ord typeclass, the following test failed:
x <= y && y <= z ≡ x <= z, where
x = 1
y = 2
z = 1
The reduced test is:
False ≡ True
The law in question:
(†) Transitivity Law: x <= y && y <= z ≡ x <= z
━━━━━━━━━━━━━━━
This failure can be reproduced by running:
> recheck (Size 2) (Seed 3253908977522463743 17379856752577018227) <property>
✓ <interactive> passed 100 tests.
✓ <interactive> passed 100 tests.
Something is very wrong here.
I think the equality should be an implication. Transitivity is:
x <= y && y <= z
implies x <= z
You're right. I just pushed a50eaa453a79a75ef8346e3ffba5bf4085e6545e, which after adding some tests seems to fix the issue. Would you mind trying that out? I need to make a release with a fix.
Certainly. Just building now, will report back.
Thank you very much!
Works perfectly for my case, thank you!
Awesome!
I find the following quite surprising, and I'm not really sure what to do with the test failure: