equational-reasoning 0.6.0.3 → 0.6.0.4
raw patch · 1 files changed
+1/−2 lines, 1 filesdep −th-extrasPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependencies removed: th-extras
API changes (from Hackage documentation)
- Proof.Equational: data Proxy (t :: k) :: forall k. () => k -> Type
+ Proof.Equational: data (a :: k) :~: (b :: k)
+ Proof.Equational: data Proxy (t :: k)
- Proof.Equational: Proxy :: Proxy
+ Proof.Equational: Proxy :: Proxy (t :: k)
- Proof.Equational: [Refl] :: forall k (a :: k) (b :: k). () => a :~: a
+ Proof.Equational: [Refl] :: forall k (a :: k). a :~: a
- Proof.Equational: fromBool :: (FromBool c, Predicate c ~ 'True) => HVec (Args c) -> c
+ Proof.Equational: fromBool :: (FromBool c, Predicate c ~ 'True) => HVec (Args c) -> c
- Proof.Equational: fromBool' :: forall proxy c. (KnownTypeList (Args c), FromBool c, Predicate c ~ 'True) => proxy c -> Args c :~> c
+ Proof.Equational: fromBool' :: forall proxy c. (KnownTypeList (Args c), FromBool c, Predicate c ~ 'True) => proxy c -> Args c :~> c
- Proof.Equational: sym :: () => (a :~: b) -> b :~: a
+ Proof.Equational: sym :: forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
- Proof.Equational: trans :: () => (a :~: b) -> (b :~: c) -> a :~: c
+ Proof.Equational: trans :: forall k (a :: k) (b :: k) (c :: k). (a :~: b) -> (b :~: c) -> a :~: c
- Proof.Propositional: [Witness] :: IsTrue 'True
+ Proof.Propositional: [Witness] :: IsTrue 'True
- Proof.Propositional: withWitness :: IsTrue b -> (b ~ 'True => r) -> r
+ Proof.Propositional: withWitness :: IsTrue b -> (b ~ 'True => r) -> r
Files
equational-reasoning.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: equational-reasoning-version: 0.6.0.3+version: 0.6.0.4 synopsis: Proof assistant for Haskell using DataKinds & PolyKinds description: A simple convenient library to write equational / preorder proof as in Agda. Since 0.6.0.0, this no longer depends on @singletons@ package, and the @Proof.Induction@ module goes to @equational-reasoning-induction@ package.@@ -28,7 +28,6 @@ build-depends: base >= 4 && < 5 , containers >= 0.5 && < 0.7 , template-haskell >= 2.11 && < 2.17- , th-extras == 0.0.* , void >= 0.6 && < 0.8 if impl(ghc >= 8.4) build-depends: th-desugar >= 1.8 && < 1.12