constraints 0.11.2 → 0.12

raw patch · 4 files changed

+32/−3 lines, 4 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.markdown +25/−0
• constraints.cabal +1/−1
• src/Data/Constraint.hs +1/−0
• src/Data/Constraint/Nat.hs +5/−2

@@ -1,3 +1,28 @@+0.12 [2020.02.03]+-----------------+* Relax the type signature for `divideTimes`:++  ```diff+  -dividesTimes :: (Divides a b, Divides a c) :- Divides a (b * c)+  +dividesTimes ::  Divides a b               :- Divides a (b * c)+  ```++* Simplify the type signature of `dividesDef`:++  ```diff+  -dividesDef :: forall a b. Divides a b :- ((a * Div b a) ~ b)+  +dividesDef :: forall a b. Divides a b :- (Mod b a ~ 0)+  ```++  The original type of `diviesDef` can be (partially) recovered by defining+  it in terms of the new `dividesDef`:++  ```hs+  dividesDef' :: forall a b. (1 <= a, Divides a b) :- ((a * Div b a) ~ b)+  dividesDef' = Sub $ case (dividesDef @a @b, euclideanNat @a @b) of+    (Sub Dict, Sub Dict) -> Dict+  ```+ 0.11.2 [2019.09.06] ------------------- * Depend on the `type-equality` compatibility library so that `(:~~:)` may be

@@ -1,6 +1,6 @@ name:          constraints category:      Constraints-version:       0.11.2+version:       0.12 license:       BSD2 cabal-version: >= 1.10 license-file:  LICENSE

@@ -208,6 +208,7 @@ infixr 9 :- infixr 9 ⊢ +-- | Type entailment, as written with a single character. type (⊢) = (:-)  -- | This is the type of entailment.

@@ -323,7 +323,7 @@ dividesPlus :: (Divides a b, Divides a c) :- Divides a (b + c) dividesPlus = Sub axiom -dividesTimes :: (Divides a b, Divides a c) :- Divides a (b * c)+dividesTimes :: Divides a b :- Divides a (b * c) dividesTimes = Sub axiom  dividesMin :: (Divides a b, Divides a c) :- Divides a (Min b c)@@ -332,7 +332,10 @@ dividesMax :: (Divides a b, Divides a c) :- Divides a (Max b c) dividesMax = Sub axiom -dividesDef :: forall a b. Divides a b :- ((a * Div b a) ~ b)+-- This `dividesDef` is simpler and more convenient than Divides a b :- ((a * Div b a) ~ b)+-- because the latter can be easily derived via 'euclideanNat', but not vice versa.++dividesDef :: forall a b. Divides a b :- (Mod b a ~ 0) dividesDef = Sub axiom  dividesPow :: (1 <= n, Divides a b) :- Divides a (b^n)