equational-reasoning 0.0.4.1 → 0.1.0.0

raw patch · 2 files changed

+11/−7 lines, 2 filesdep ~singletonsdep ~tagged

Dependency ranges changed: singletons, tagged

Files

• Proof/Equational.hs +4/−4
• equational-reasoning.cabal +7/−3

@@ -32,10 +32,10 @@ leibnizToRefl :: Leibniz a b -> a :=: b leibnizToRefl eq = apply eq Refl -fromLeibniz :: (Preorder eq, SingRep a) => Leibniz a b -> eq a b+fromLeibniz :: (Preorder eq, SingI a) => Leibniz a b -> eq a b fromLeibniz eq = apply eq (reflexivity sing) -fromRefl :: (Preorder eq, SingRep b) => a :=: b -> eq a b+fromRefl :: (Preorder eq, SingI b) => a :=: b -> eq a b fromRefl Refl = reflexivity'  reflToLeibniz :: a :=: b -> Leibniz a b@@ -76,7 +76,7 @@ data Reason eq x y where   Because :: Sing y -> eq x y -> Reason eq x y -reflexivity' :: (SingRep x, Preorder r) => r x x+reflexivity' :: (SingI x, Preorder r) => r x x reflexivity' = reflexivity sing  by, because :: Sing y -> eq x y -> Reason eq x y@@ -102,7 +102,7 @@ start :: Preorder eq => Sing a -> eq a a start = reflexivity -byDefinition :: (SingRep a, Preorder eq) => eq a a+byDefinition :: (SingI a, Preorder eq) => eq a a byDefinition = reflexivity sing  admitted :: Reason eq x y

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