From 06f6ae33c67c251d82286bdaec5337521f80a149 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Charlotte=20=F0=9F=A6=9D=20Delenk?= Date: Thu, 1 Sep 2022 09:05:34 +0100 Subject: [PATCH] add Integer --- Double/package.dhall | 1 + Double/toNatural.dhall | 6 ++++ Function/compose.dhall | 17 ++++++++++++ Function/identity.dhall | 10 +++++++ Function/package.dhall | 1 + Integer/abs.dhall | 15 ++++++++++ Integer/add.dhall | 22 +++++++++++++++ Integer/clamp.dhall | 14 ++++++++++ Integer/divide.dhall | 11 ++++++++ Integer/equal.dhall | 21 ++++++++++++++ Integer/fromAny.dhall | 11 ++++++++ Integer/greaterThan.dhall | 24 ++++++++++++++++ Integer/greaterThanEqual.dhall | 24 ++++++++++++++++ Integer/lessThan.dhall | 22 +++++++++++++++ Integer/lessThanEqual.dhall | 35 +++++++++++++++++++++++ Integer/multiply.dhall | 37 ++++++++++++++++++++++++ Integer/negate.dhall | 12 ++++++++ Integer/negative.dhall | 18 ++++++++++++ Integer/nonNegative.dhall | 18 ++++++++++++ Integer/nonPositive.dhall | 16 +++++++++++ Integer/package.dhall | 23 +++++++++++++++ Integer/positive.dhall | 20 +++++++++++++ Integer/show.dhall | 14 ++++++++++ Integer/subtract.dhall | 51 ++++++++++++++++++++++++++++++++++ Integer/toDouble.dhall | 10 +++++++ Integer/toNatural.dhall | 17 ++++++++++++ Natural/equal.dhall | 17 ++++++++++++ Natural/greaterThanEqual.dhall | 23 +++++++++++++++ Natural/lessThanEqual.dhall | 16 +++++++++++ Number/package.dhall | 1 + Number/toNatural.dhall | 8 ++++++ package.dhall | 2 ++ 32 files changed, 537 insertions(+) create mode 100644 Double/toNatural.dhall create mode 100644 Function/compose.dhall create mode 100644 Function/identity.dhall create mode 100644 Function/package.dhall create mode 100644 Integer/abs.dhall create mode 100644 Integer/add.dhall create mode 100644 Integer/clamp.dhall create mode 100644 Integer/divide.dhall create mode 100644 Integer/equal.dhall create mode 100644 Integer/fromAny.dhall create mode 100644 Integer/greaterThan.dhall create mode 100644 Integer/greaterThanEqual.dhall create mode 100644 Integer/lessThan.dhall create mode 100644 Integer/lessThanEqual.dhall create mode 100644 Integer/multiply.dhall create mode 100644 Integer/negate.dhall create mode 100644 Integer/negative.dhall create mode 100644 Integer/nonNegative.dhall create mode 100644 Integer/nonPositive.dhall create mode 100644 Integer/package.dhall create mode 100644 Integer/positive.dhall create mode 100644 Integer/show.dhall create mode 100644 Integer/subtract.dhall create mode 100644 Integer/toDouble.dhall create mode 100644 Integer/toNatural.dhall create mode 100644 Natural/equal.dhall create mode 100644 Natural/greaterThanEqual.dhall create mode 100644 Natural/lessThanEqual.dhall create mode 100644 Number/toNatural.dhall diff --git a/Double/package.dhall b/Double/package.dhall index 4cecec2..04adfbf 100644 --- a/Double/package.dhall +++ b/Double/package.dhall @@ -18,4 +18,5 @@ , show = ./show.dhall , subtract = ./subtract.dhall nix , toInteger = ./toInteger.dhall nix + , toNatural = ./toNatural.dhall nix } diff --git a/Double/toNatural.dhall b/Double/toNatural.dhall new file mode 100644 index 0000000..8e7543e --- /dev/null +++ b/Double/toNatural.dhall @@ -0,0 +1,6 @@ +λ(nix : ../NixPrelude.dhall) → + let Number/fromDouble = ../Number/fromDouble.dhall nix + + let Number/toNatural = ../Number/toNatural.dhall nix + + in λ(a : Double) → Number/toNatural (Number/fromDouble a) diff --git a/Function/compose.dhall b/Function/compose.dhall new file mode 100644 index 0000000..3931702 --- /dev/null +++ b/Function/compose.dhall @@ -0,0 +1,17 @@ +--| Compose two functions into one. +let compose + : ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → (b → c) → a → c + = λ(A : Type) → + λ(B : Type) → + λ(C : Type) → + λ(f : A → B) → + λ(g : B → C) → + λ(x : A) → + g (f x) + +let example0 = + assert + : compose Natural Natural Bool (λ(n : Natural) → n + n) Natural/even 3 + ≡ True + +in compose diff --git a/Function/identity.dhall b/Function/identity.dhall new file mode 100644 index 0000000..40d3a67 --- /dev/null +++ b/Function/identity.dhall @@ -0,0 +1,10 @@ +--| The identity function simply returns its input +let identity + : ∀(a : Type) → ∀(x : a) → a + = λ(a : Type) → λ(x : a) → x + +let example0 = assert : identity Natural 1 ≡ 1 + +let example1 = assert : identity Bool ≡ (λ(x : Bool) → x) + +in identity diff --git a/Function/package.dhall b/Function/package.dhall new file mode 100644 index 0000000..ddd5532 --- /dev/null +++ b/Function/package.dhall @@ -0,0 +1 @@ +{ compose = ./compose.dhall, identity = ./identity.dhall } diff --git a/Integer/abs.dhall b/Integer/abs.dhall new file mode 100644 index 0000000..f32770a --- /dev/null +++ b/Integer/abs.dhall @@ -0,0 +1,15 @@ +--| Returns the absolute value of an `Integer`, i.e. its non-negative value. +let abs + : Integer → Natural + = λ(n : Integer) → + if Natural/isZero (Integer/clamp n) + then Integer/clamp (Integer/negate n) + else Integer/clamp n + +let example0 = assert : abs +7 ≡ 7 + +let example2 = assert : abs +0 ≡ 0 + +let example3 = assert : abs -3 ≡ 3 + +in abs diff --git a/Integer/add.dhall b/Integer/add.dhall new file mode 100644 index 0000000..087f01a --- /dev/null +++ b/Integer/add.dhall @@ -0,0 +1,22 @@ +--| `add m n` computes `m + n`. +let Integer/subtract = ./subtract.dhall + +let add + : Integer → Integer → Integer + = λ(m : Integer) → λ(n : Integer) → Integer/subtract (Integer/negate m) n + +let example0 = assert : add +3 +5 ≡ +8 + +let example1 = assert : add -3 -5 ≡ -8 + +let example2 = assert : add -4 +4 ≡ +0 + +let example3 = assert : add -3 +5 ≡ +2 + +let example4 = assert : add +3 -5 ≡ -2 + +let example5 = assert : add +0 -3 ≡ -3 + +let example6 = assert : add +0 +3 ≡ +3 + +in add diff --git a/Integer/clamp.dhall b/Integer/clamp.dhall new file mode 100644 index 0000000..c55f73d --- /dev/null +++ b/Integer/clamp.dhall @@ -0,0 +1,14 @@ +{-| +Convert an `Integer` to a `Natural` number, with negative numbers becoming zero. +-} +let clamp + : Integer → Natural + = Integer/clamp + +let example0 = assert : clamp +7 ≡ 7 + +let example2 = assert : clamp +0 ≡ 0 + +let example3 = assert : clamp -3 ≡ 0 + +in clamp diff --git a/Integer/divide.dhall b/Integer/divide.dhall new file mode 100644 index 0000000..311f148 --- /dev/null +++ b/Integer/divide.dhall @@ -0,0 +1,11 @@ +λ(nix : ../NixPrelude.dhall) → + let Number/fromInteger = ../Number/fromInteger.dhall nix + + let Number/divide = ../Number/divide.dhall nix + + let Number/toInteger = ../Number/toInteger.dhall nix + + in λ(a : Integer) → + λ(b : Integer) → + Number/toInteger + (Number/divide (Number/fromInteger a) (Number/fromInteger b)) diff --git a/Integer/equal.dhall b/Integer/equal.dhall new file mode 100644 index 0000000..5933f29 --- /dev/null +++ b/Integer/equal.dhall @@ -0,0 +1,21 @@ +--| `equal` checks if two Integers are equal. +let Natural/equal = ../Natural/equal.dhall + +let equal + : Integer → Integer → Bool + = λ(a : Integer) → + λ(b : Integer) → + Natural/equal (Integer/clamp a) (Integer/clamp b) + && Natural/equal + (Integer/clamp (Integer/negate a)) + (Integer/clamp (Integer/negate b)) + +let example0 = assert : equal +5 +5 ≡ True + +let example1 = assert : equal +5 +6 ≡ False + +let example2 = assert : equal +5 -5 ≡ False + +let example3 = assert : equal -5 -5 ≡ True + +in equal diff --git a/Integer/fromAny.dhall b/Integer/fromAny.dhall new file mode 100644 index 0000000..7281e96 --- /dev/null +++ b/Integer/fromAny.dhall @@ -0,0 +1,11 @@ +λ(nix : ../NixPrelude.dhall) → + let Any = ../Any/Type.dhall + + let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix + + let Misc/throw = ../Misc/throw.dhall nix + + in λ(v : Any) → + if nix.builtins.isInt v + then Any/toTypeUnchecked Integer v + else Misc/throw Integer "Failed to coerce object into Double" diff --git a/Integer/greaterThan.dhall b/Integer/greaterThan.dhall new file mode 100644 index 0000000..6eb91a9 --- /dev/null +++ b/Integer/greaterThan.dhall @@ -0,0 +1,24 @@ +--| `greaterThan` checks if one Integer is greater than another. +let Bool/not = ../Bool/not.dhall + +let lessThanEqual = ./lessThanEqual.dhall + +let greaterThan + : Integer → Integer → Bool + = λ(x : Integer) → λ(y : Integer) → Bool/not (lessThanEqual x y) + +let example0 = assert : greaterThan +5 +6 ≡ False + +let example1 = assert : greaterThan +5 +5 ≡ False + +let example2 = assert : greaterThan +5 +4 ≡ True + +let example3 = assert : greaterThan -5 +8 ≡ False + +let example4 = assert : greaterThan -5 -3 ≡ False + +let example5 = assert : greaterThan -3 -5 ≡ True + +let example6 = assert : greaterThan -3 -3 ≡ False + +in greaterThan diff --git a/Integer/greaterThanEqual.dhall b/Integer/greaterThanEqual.dhall new file mode 100644 index 0000000..73be7fd --- /dev/null +++ b/Integer/greaterThanEqual.dhall @@ -0,0 +1,24 @@ +{-| +`greaterThanEqual` checks if one Integer is greater than or equal to another. +-} +let lessThanEqual = ./lessThanEqual.dhall + +let greaterThanEqual + : Integer → Integer → Bool + = λ(x : Integer) → λ(y : Integer) → lessThanEqual y x + +let example0 = assert : greaterThanEqual +5 +6 ≡ False + +let example1 = assert : greaterThanEqual +5 +5 ≡ True + +let example2 = assert : greaterThanEqual +5 +4 ≡ True + +let example3 = assert : greaterThanEqual -5 +8 ≡ False + +let example4 = assert : greaterThanEqual -5 -3 ≡ False + +let example5 = assert : greaterThanEqual -3 -5 ≡ True + +let example6 = assert : greaterThanEqual -3 -3 ≡ True + +in greaterThanEqual diff --git a/Integer/lessThan.dhall b/Integer/lessThan.dhall new file mode 100644 index 0000000..9b5cd93 --- /dev/null +++ b/Integer/lessThan.dhall @@ -0,0 +1,22 @@ +--| `lessThan` checks if one Integer is less than another. +let greaterThan = ./greaterThan.dhall + +let lessThan + : Integer → Integer → Bool + = λ(x : Integer) → λ(y : Integer) → greaterThan y x + +let example0 = assert : lessThan +5 +6 ≡ True + +let example1 = assert : lessThan +5 +5 ≡ False + +let example2 = assert : lessThan +5 +4 ≡ False + +let example3 = assert : lessThan -5 +8 ≡ True + +let example4 = assert : lessThan -5 -3 ≡ True + +let example5 = assert : lessThan -3 -5 ≡ False + +let example6 = assert : lessThan -3 -3 ≡ False + +in lessThan diff --git a/Integer/lessThanEqual.dhall b/Integer/lessThanEqual.dhall new file mode 100644 index 0000000..6105e39 --- /dev/null +++ b/Integer/lessThanEqual.dhall @@ -0,0 +1,35 @@ +--| `lessThanEqual` checks if one Integer is less than or equal to another. +let Natural/greaterThanEqual = ../Natural/greaterThanEqual.dhall + +let Natural/lessThanEqual = ../Natural/lessThanEqual.dhall + +let nonPositive = ./nonPositive.dhall + +let nonNegative = ./nonNegative.dhall + +let lessThanEqual + : Integer → Integer → Bool + = λ(x : Integer) → + λ(y : Integer) → + if nonPositive x + then nonNegative y + || Natural/greaterThanEqual + (Integer/clamp (Integer/negate x)) + (Integer/clamp (Integer/negate y)) + else Natural/lessThanEqual (Integer/clamp x) (Integer/clamp y) + +let example0 = assert : lessThanEqual +5 +6 ≡ True + +let example1 = assert : lessThanEqual +5 +5 ≡ True + +let example2 = assert : lessThanEqual +5 +4 ≡ False + +let example3 = assert : lessThanEqual -5 +8 ≡ True + +let example4 = assert : lessThanEqual -5 -3 ≡ True + +let example5 = assert : lessThanEqual -3 -5 ≡ False + +let example6 = assert : lessThanEqual -3 -3 ≡ True + +in lessThanEqual diff --git a/Integer/multiply.dhall b/Integer/multiply.dhall new file mode 100644 index 0000000..f6a4f78 --- /dev/null +++ b/Integer/multiply.dhall @@ -0,0 +1,37 @@ +--| `multiply m n` computes `m * n`. +let nonPositive = ./nonPositive.dhall + +let multiplyNonNegative = + λ(x : Integer) → + λ(y : Integer) → + Natural/toInteger (Integer/clamp x * Integer/clamp y) + +let multiply + : Integer → Integer → Integer + = λ(m : Integer) → + λ(n : Integer) → + if nonPositive m + then if nonPositive n + then multiplyNonNegative (Integer/negate m) (Integer/negate n) + else Integer/negate (multiplyNonNegative (Integer/negate m) n) + else if nonPositive n + then Integer/negate (multiplyNonNegative m (Integer/negate n)) + else multiplyNonNegative m n + +let example0 = assert : multiply +3 +5 ≡ +15 + +let example1 = assert : multiply -3 +5 ≡ -15 + +let example2 = assert : multiply -3 -5 ≡ +15 + +let example3 = assert : multiply +0 +5 ≡ +0 + +let example4 = assert : multiply +5 +0 ≡ +0 + +let example5 = assert : multiply +0 +0 ≡ +0 + +let example6 = assert : multiply +1 +5 ≡ +5 + +let example7 = assert : multiply +3 -1 ≡ -3 + +in multiply diff --git a/Integer/negate.dhall b/Integer/negate.dhall new file mode 100644 index 0000000..03eff72 --- /dev/null +++ b/Integer/negate.dhall @@ -0,0 +1,12 @@ +--| Invert the sign of an `Integer`, with zero remaining unchanged. +let negate + : Integer → Integer + = Integer/negate + +let example0 = assert : negate -3 ≡ +3 + +let example2 = assert : negate +7 ≡ -7 + +let example3 = assert : negate +0 ≡ +0 + +in negate diff --git a/Integer/negative.dhall b/Integer/negative.dhall new file mode 100644 index 0000000..c05bb65 --- /dev/null +++ b/Integer/negative.dhall @@ -0,0 +1,18 @@ +{-| +Returns `True` for any `Integer` less than `+0`. + +`negative` is more efficient than `./lessThan +0` or `./lessThanEqual -1`. +-} +let positive = ./positive.dhall + +let negative + : Integer → Bool + = λ(n : Integer) → positive (Integer/negate n) + +let example0 = assert : negative +1 ≡ False + +let example1 = assert : negative +0 ≡ False + +let example2 = assert : negative -1 ≡ True + +in negative diff --git a/Integer/nonNegative.dhall b/Integer/nonNegative.dhall new file mode 100644 index 0000000..7f08249 --- /dev/null +++ b/Integer/nonNegative.dhall @@ -0,0 +1,18 @@ +{-| +Returns `True` for `+0` and any positive `Integer`. + +`nonNegative` is more efficient than `./greaterThanEqual +0` or `./greaterThan -1`. +-} +let nonPositive = ./nonPositive.dhall + +let nonNegative + : Integer → Bool + = λ(n : Integer) → nonPositive (Integer/negate n) + +let example0 = assert : nonNegative +1 ≡ True + +let example1 = assert : nonNegative +0 ≡ True + +let example2 = assert : nonNegative -1 ≡ False + +in nonNegative diff --git a/Integer/nonPositive.dhall b/Integer/nonPositive.dhall new file mode 100644 index 0000000..f7d7a49 --- /dev/null +++ b/Integer/nonPositive.dhall @@ -0,0 +1,16 @@ +{-| +Returns `True` for `+0` and any negative `Integer`. + +`nonPositive` is more efficient than `./lessThanEqual +0` or `./lessThan +1`. +-} +let nonPositive + : Integer → Bool + = λ(n : Integer) → Natural/isZero (Integer/clamp n) + +let example0 = assert : nonPositive +1 ≡ False + +let example1 = assert : nonPositive +0 ≡ True + +let example2 = assert : nonPositive -1 ≡ True + +in nonPositive diff --git a/Integer/package.dhall b/Integer/package.dhall new file mode 100644 index 0000000..86bd415 --- /dev/null +++ b/Integer/package.dhall @@ -0,0 +1,23 @@ +λ(nix : ../NixPrelude.dhall) → + { Type = Integer + , abs = ./abs.dhall + , add = ./add.dhall + , clamp = ./clamp.dhall + , divide = ./divide.dhall nix + , equal = ./equal.dhall + , fromAny = ./fromAny.dhall nix + , greaterThan = ./greaterThan.dhall + , greaterThanEqual = ./greaterThanEqual.dhall + , lessThan = ./lessThan.dhall + , lessThanEqual = ./lessThanEqual.dhall + , multiply = ./multiply.dhall + , negate = ./negate.dhall + , negative = ./negative.dhall + , nonNegative = ./nonNegative.dhall + , nonPositive = ./nonPositive.dhall + , positive = ./positive.dhall + , show = ./show.dhall + , subtract = ./subtract.dhall + , toDouble = ./toDouble.dhall + , toNatural = ./toNatural.dhall + } diff --git a/Integer/positive.dhall b/Integer/positive.dhall new file mode 100644 index 0000000..2f279b9 --- /dev/null +++ b/Integer/positive.dhall @@ -0,0 +1,20 @@ +{-| +Returns `True` for any `Integer` greater than `+0`. + +`positive` is more efficient than `./greaterThan +0` or `./greaterThanEqual +1`. +-} +let not = ../Bool/not.dhall + +let nonPositive = ./nonPositive.dhall + +let positive + : Integer → Bool + = λ(n : Integer) → not (nonPositive n) + +let example0 = assert : positive +1 ≡ True + +let example1 = assert : positive +0 ≡ False + +let example2 = assert : positive -1 ≡ False + +in positive diff --git a/Integer/show.dhall b/Integer/show.dhall new file mode 100644 index 0000000..33e6b5a --- /dev/null +++ b/Integer/show.dhall @@ -0,0 +1,14 @@ +{-| +Render an `Integer` as `Text` using the same representation as Dhall source +code (i.e. a decimal number with a leading `-` sign if negative and a leading +`+` sign if non-negative) +-} +let show + : Integer → Text + = Integer/show + +let example0 = assert : show -3 ≡ "-3" + +let example1 = assert : show +0 ≡ "+0" + +in show diff --git a/Integer/subtract.dhall b/Integer/subtract.dhall new file mode 100644 index 0000000..f5768b2 --- /dev/null +++ b/Integer/subtract.dhall @@ -0,0 +1,51 @@ +--| `subtract m n` computes `n - m`. +let nonPositive = ./nonPositive.dhall + +let subtractNonNegative = + λ(xi : Integer) → + λ(yi : Integer) → + let xn = Integer/clamp xi + + let yn = Integer/clamp yi + + let dn = Natural/subtract xn yn + + in if Natural/isZero dn + then Integer/negate (Natural/toInteger (Natural/subtract yn xn)) + else Natural/toInteger dn + +let subtract + : Integer → Integer → Integer + = λ(m : Integer) → + λ(n : Integer) → + if nonPositive m + then if nonPositive n + then subtractNonNegative (Integer/negate n) (Integer/negate m) + else Natural/toInteger + (Integer/clamp (Integer/negate m) + Integer/clamp n) + else if nonPositive n + then Integer/negate + ( Natural/toInteger + (Integer/clamp m + Integer/clamp (Integer/negate n)) + ) + else subtractNonNegative m n + +let example0 = assert : subtract +3 +5 ≡ +2 + +let example1 = assert : subtract +4 +4 ≡ +0 + +let example2 = assert : subtract +5 +3 ≡ -2 + +let example3 = assert : subtract -3 -5 ≡ -2 + +let example4 = assert : subtract -4 -4 ≡ +0 + +let example5 = assert : subtract -5 -3 ≡ +2 + +let example6 = assert : subtract -3 +5 ≡ +8 + +let example7 = assert : subtract +3 -5 ≡ -8 + +let example8 = assert : subtract +0 -3 ≡ -3 + +in subtract diff --git a/Integer/toDouble.dhall b/Integer/toDouble.dhall new file mode 100644 index 0000000..b5d1e61 --- /dev/null +++ b/Integer/toDouble.dhall @@ -0,0 +1,10 @@ +--| Convert an `Integer` to the corresponding `Double` +let toDouble + : Integer → Double + = Integer/toDouble + +let example0 = assert : toDouble -3 ≡ -3.0 + +let example1 = assert : toDouble +2 ≡ 2.0 + +in toDouble diff --git a/Integer/toNatural.dhall b/Integer/toNatural.dhall new file mode 100644 index 0000000..fbbd05b --- /dev/null +++ b/Integer/toNatural.dhall @@ -0,0 +1,17 @@ +{-| +Convert an `Integer` to an `Optional Natural`, with negative numbers becoming `None Natural`. +-} +let nonNegative = ./nonNegative.dhall + +let toNatural + : Integer → Optional Natural + = λ(n : Integer) → + if nonNegative n then Some (Integer/clamp n) else None Natural + +let example0 = assert : toNatural +7 ≡ Some 7 + +let example2 = assert : toNatural +0 ≡ Some 0 + +let example3 = assert : toNatural -3 ≡ None Natural + +in toNatural diff --git a/Natural/equal.dhall b/Natural/equal.dhall new file mode 100644 index 0000000..eb8d1c2 --- /dev/null +++ b/Natural/equal.dhall @@ -0,0 +1,17 @@ +--| `equal` checks if two Naturals are equal. +let lessThanEqual = + ./lessThanEqual.dhall + sha256:1a5caa2b80a42b9f58fff58e47ac0d9a9946d0b2d36c54034b8ddfe3cb0f3c99 + ? ./lessThanEqual.dhall + +let equal + : Natural → Natural → Bool + = λ(a : Natural) → λ(b : Natural) → lessThanEqual a b && lessThanEqual b a + +let example0 = assert : equal 5 5 ≡ True + +let example1 = assert : equal 5 6 ≡ False + +let property0 = λ(n : Natural) → assert : equal n n ≡ True + +in equal diff --git a/Natural/greaterThanEqual.dhall b/Natural/greaterThanEqual.dhall new file mode 100644 index 0000000..57d3433 --- /dev/null +++ b/Natural/greaterThanEqual.dhall @@ -0,0 +1,23 @@ +{-| +`greaterThanEqual` checks if one Natural is greater than or equal to another. +-} +let lessThanEqual = + ./lessThanEqual.dhall + sha256:1a5caa2b80a42b9f58fff58e47ac0d9a9946d0b2d36c54034b8ddfe3cb0f3c99 + ? ./lessThanEqual.dhall + +let greaterThanEqual + : Natural → Natural → Bool + = λ(x : Natural) → λ(y : Natural) → lessThanEqual y x + +let example0 = assert : greaterThanEqual 5 6 ≡ False + +let example1 = assert : greaterThanEqual 5 5 ≡ True + +let example2 = assert : greaterThanEqual 5 4 ≡ True + +let property0 = λ(n : Natural) → assert : greaterThanEqual n 0 ≡ True + +let property1 = λ(n : Natural) → assert : greaterThanEqual n n ≡ True + +in greaterThanEqual diff --git a/Natural/lessThanEqual.dhall b/Natural/lessThanEqual.dhall new file mode 100644 index 0000000..822d271 --- /dev/null +++ b/Natural/lessThanEqual.dhall @@ -0,0 +1,16 @@ +--| `lessThanEqual` checks if one Natural is less than or equal to another. +let lessThanEqual + : Natural → Natural → Bool + = λ(x : Natural) → λ(y : Natural) → Natural/isZero (Natural/subtract y x) + +let example0 = assert : lessThanEqual 5 6 ≡ True + +let example1 = assert : lessThanEqual 5 5 ≡ True + +let example2 = assert : lessThanEqual 5 4 ≡ False + +let property0 = λ(n : Natural) → assert : lessThanEqual 0 n ≡ True + +let property1 = λ(n : Natural) → assert : lessThanEqual n n ≡ True + +in lessThanEqual diff --git a/Number/package.dhall b/Number/package.dhall index 0cfe9f3..d4cfcab 100644 --- a/Number/package.dhall +++ b/Number/package.dhall @@ -22,4 +22,5 @@ , subtract = ./subtract.dhall nix , toDouble = ./toDouble.dhall nix , toInteger = ./toInteger.dhall nix + , toNatural = ./toNatural.dhall nix } diff --git a/Number/toNatural.dhall b/Number/toNatural.dhall new file mode 100644 index 0000000..7847028 --- /dev/null +++ b/Number/toNatural.dhall @@ -0,0 +1,8 @@ +λ(nix : ../NixPrelude.dhall) → + let Number = ./Type.dhall + + let Integer/toNatural = ../Integer/toNatural.dhall + + let Number/toInteger = ./toInteger.dhall nix + + in λ(a : Number) → Integer/toNatural (Number/toInteger a) diff --git a/package.dhall b/package.dhall index 38d8f7b..dead41a 100644 --- a/package.dhall +++ b/package.dhall @@ -2,6 +2,8 @@ { Any = ./Any/package.dhall nix , Bool = ./Bool/package.dhall nix , Double = ./Double/package.dhall nix + , Function = ./Function/package.dhall + , Integer = ./Integer/package.dhall nix , Misc = ./Misc/package.dhall nix , Monoid = ./Monoid.dhall , Number = ./Number/package.dhall nix