equational-reasoning 0.2.0.4 → 0.2.0.5

raw patch · 2 files changed

+23/−4 lines, 2 filesdep ~voidPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: void

API changes (from Hackage documentation)

Files

• Proof/Equational.hs +21/−2
• equational-reasoning.cabal +2/−2

@@ -89,11 +89,17 @@   symmetry     :: eq a b  -> eq b a  instance Preorder (:=:) where+  {-# SPECIALISE instance Preorder (:=:) #-}   transitivity Refl Refl = Refl+  {-# INLINE[1] transitivity #-}+   reflexivity  _         = Refl+  {-# INLINE[1] reflexivity #-}  instance Equality (:=:) where+  {-# SPECIALISE instance Equality (:~:) #-}   symmetry     Refl      = Refl+  {-# INLINE[1] symmetry #-}  instance Preorder (->) where   reflexivity _ = id@@ -128,11 +134,16 @@ (=<=) :: Preorder r => r x y -> Reason r y z -> r x z eq =<= (_ `Because` eq') = transitivity eq eq' +{-# SPECIALISE INLINE[1] (=<=) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}+ (=>=) :: Preorder r => r y z -> Reason r x y -> r x z eq =>= (_ `Because` eq') = transitivity eq' eq +{-# SPECIALISE INLINE[1] (=>=) :: y :~: z -> Reason (:~:) x y -> x :~: z #-}+ (===) :: Equality eq => eq x y -> Reason eq y z -> eq x z (===) = (=<=)+{-# SPECIALISE INLINE[1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}  (=~=) :: Preorder r => r x y -> Sing y -> r x y eq =~= _ = eq@@ -159,12 +170,20 @@ -- you can reduce the overhead introduced by run-time proof. coerce :: (a :=: b) -> f a -> f b coerce Refl a = unsafeCoerce a-{-# INLINE coerce #-}+{-# INLINE[1] coerce #-}  -- | Coercion for identity types. coerce' :: a :=: b -> a -> b coerce' Refl a = unsafeCoerce a-{-# INLINE coerce' #-}+{-# INLINE[1] coerce' #-}++{-# RULES+"coerce/unsafeCoerce" forall xs.+  coerce xs = unsafeCoerce+"coerce'/unsafeCoerce" forall xs.+  coerce' xs = unsafeCoerce+  #-}+  #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 class Proposition (f :: k -> *) where

@@ -2,7 +2,7 @@ --  documentation, see http://haskell.org/cabal/users-guide/  name:                equational-reasoning-version:             0.2.0.4+version:             0.2.0.5 synopsis:            Proof assistant for Haskell using DataKinds & PolyKinds description:         A simple convenient library to write equational / preorder proof as in Agda. license:             BSD3@@ -22,7 +22,7 @@ library   exposed-modules:     Proof.Equational, Proof.Propositional, Proof.Induction   build-depends:       base             >= 4      && < 5-               ,       void             == 0.6.*+               ,       void             >= 0.6    && < 0.8                ,       template-haskell >= 2.8    && < 2.11   if impl(ghc < 7.8)     build-depends:     singletons       == 0.8.*