Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Small improvements for Prelude.Natural #719

Merged
merged 6 commits into from Sep 6, 2019

Conversation

@sjakobi
Copy link
Collaborator

commented Sep 1, 2019

  • Add Natural.subtract
  • Small improvements for the Natural comparison functions
    • Add property assertions
    • Only lessThanEqual uses the Natural/subtract primitive, everything
      else is ultimately implemented in terms of lessThanEqual.
    • greaterThanEqual requires only 2 normalization steps instead of 3
sjakobi added 2 commits Sep 1, 2019
Prelude: Small improvements for the Natural comparison functions
* Add property assertions
* Only lessThanEqual uses the Natural/subtract primitive, everything
  else is ultimately implemented in terms of lessThanEqual.
* greaterThanEqual requires only 2 normalization steps instead of 3
@sjakobi

This comment has been minimized.

Copy link
Collaborator Author

commented Sep 1, 2019

How do I produce the SHA256 hash of a recent version version of dhall-haskell for nixops/dhall-haskell.json?

@Gabriel439

This comment has been minimized.

Copy link
Contributor

commented Sep 1, 2019

@sjakobi: Run:

$ nix-prefetch-git --fetch-submodule git@github.com:dhall-lang/dhall-haskell.git

... and if you need a specific revision then add it to the end of the command

Update nixops/dhall-haskell.json
Command used:

    nix-prefetch-git --fetch-submodules https://github.com/dhall-lang/dhall-haskell
λ(b : Natural)
Natural/isZero (Natural/subtract a b)
&& Natural/isZero (Natural/subtract b a)
= λ(a : Natural) λ(b : Natural) lessThanEqual a b && lessThanEqual b a

This comment has been minimized.

Copy link
@singpolyma

singpolyma Sep 1, 2019

Collaborator

Why is this better?

@sjakobi

This comment has been minimized.

Copy link
Collaborator Author

commented Sep 1, 2019

@singpolyma I guess it was just my personal preference to re-use a prelude function here. The normalized code is of course the same (modulo commutativity maybe).

@sjakobi sjakobi added the Voting Open label Sep 2, 2019

@f-f
f-f approved these changes Sep 5, 2019

@sjakobi sjakobi merged commit 898510c into master Sep 6, 2019

1 check passed

hydra Hydra build #31704 of dhall-lang:719:dhall-lang
Details

@sjakobi sjakobi deleted the sjakobi/prelude-natural-improvements branch Sep 6, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
4 participants
You can’t perform that action at this time.