prelude: Add Natural comparison functions #674
Conversation
Adds Natural/lt, Natural/lte, Natural/eq, Natural/gte, Natural/gt
Prelude/Natural/gte
Outdated
|
|
||
| let gte | ||
| : Natural → Natural → Bool | ||
| = λ(x : Natural) → λ(y : Natural) → Bool/not (lt x y) |
There was a problem hiding this comment.
It should be a bit more efficient to implement this analogously to along the lines of lte.
There was a problem hiding this comment.
@ocharles Did you see my comment above?
There was a problem hiding this comment.
I did, but I don't have the time to change it now. I'm happy to take a PR to this PR though!
|
@Gabriel439 Can I update the |
|
@ocharles: Yeah, you can update the |
|
Ok, I believe this is good to go. |
|
Also, can you turn the examples into |
| ? ./greaterThanEqual | ||
| , greaterThan = | ||
| ./greaterThan sha256:f702abcdfcd7ad73619b9285d7e41c3a1d017fb6b8d037cf40bd93bf30c09b2c | ||
| ? ./greaterThan |
There was a problem hiding this comment.
Apparently this record was previously formatted with ascending keys – not sure whether that's actually important…
Good idea! |
PR dhall-lang#674 added new functions to the prelude without updating this test, which now fails. This fixes it.
PR #674 added new functions to the prelude without updating this test, which now fails. This fixes it.
Adds Natural/lt, Natural/lte, Natural/eq, Natural/gte, Natural/gt