equational-reasoning 0.7.0.1 → 0.7.0.2
raw patch · 1 files changed
+40/−39 lines, 1 filesdep −semigroupsdep ~template-haskelldep ~th-desugarPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependencies removed: semigroups
Dependency ranges changed: template-haskell, th-desugar
API changes (from Hackage documentation)
- Proof.Equational: type family Args c :: [Type];
- Proof.Propositional: instance Proof.Propositional.Inhabited.Inhabited (GHC.Real.Ratio GHC.Integer.Type.Integer)
- Proof.Propositional: instance Proof.Propositional.Inhabited.Inhabited GHC.Integer.Type.Integer
+ Proof.Equational: type Args c :: [Type];
+ Proof.Equational: type OriginalProp (f :: k -> Type) (n :: k) :: Type;
+ Proof.Equational: type Predicate c :: Bool;
+ Proof.Propositional: instance Proof.Propositional.Inhabited.Inhabited (GHC.Real.Ratio GHC.Num.Integer.Integer)
+ Proof.Propositional: instance Proof.Propositional.Inhabited.Inhabited GHC.Num.Integer.Integer
- Proof.Equational: [Refl] :: forall k (a :: k). a :~: a
+ Proof.Equational: [Refl] :: forall {k} (a :: k). a :~: a
- Proof.Equational: sym :: forall k (a :: k) (b :: k). (a :~: b) -> b :~: a
+ Proof.Equational: sym :: forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
- Proof.Equational: trans :: forall k (a :: k) (b :: k) (c :: k). (a :~: b) -> (b :~: c) -> a :~: c
+ Proof.Equational: trans :: forall {k} (a :: k) (b :: k) (c :: k). (a :~: b) -> (b :~: c) -> a :~: c
Files
- equational-reasoning.cabal +40/−39
equational-reasoning.cabal view
@@ -1,43 +1,44 @@--- Initial equational-reasoning.cabal generated by cabal init. For further--- documentation, see http://haskell.org/cabal/users-guide/+name: equational-reasoning+version: 0.7.0.2+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. -name: equational-reasoning-version: 0.7.0.1-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.-license: BSD3-license-file: LICENSE-author: Hiromi ISHII-maintainer: konn.jinro_at_gmail.com-copyright: (c) Hiromi ISHII 2013-2020-category: Math-build-type: Simple-tested-with: GHC == 8.0.2,- GHC == 8.2.1,- GHC == 8.4.1,- GHC == 8.6.3,- GHC == 8.8.2,- GHC == 8.10.3,- GHC == 9.0.1-cabal-version: >=1.10+license: BSD3+license-file: LICENSE+author: Hiromi ISHII+maintainer: konn.jinro_at_gmail.com+copyright: (c) Hiromi ISHII 2013-2020+category: Math+build-type: Simple+tested-with:+ GHC ==9.0.2+ || ==9.2.8+ || ==9.4.8+ || ==9.6.3+ || ==9.8.1++cabal-version: >=1.10+ source-repository head- type: git- location: git://github.com/konn/equational-reasoning-in-haskell.git+ type: git+ location: git://github.com/konn/equational-reasoning-in-haskell.git library- exposed-modules: Proof.Equational, Proof.Propositional- , Proof.Propositional.Inhabited- , Proof.Propositional.Empty- other-modules: Proof.Propositional.TH- ghc-options: -Wall- build-depends: base >= 4 && < 5- , containers >= 0.5 && < 0.7- , template-haskell >= 2.11 && < 2.19- , void >= 0.6 && < 0.8- if impl(ghc >= 8.4)- build-depends: th-desugar >= 1.8 && < 1.14- else- build-depends: semigroups == 0.18.*- build-depends: th-desugar >= 1.6 && < 1.8- default-language: Haskell2010+ exposed-modules:+ Proof.Equational+ Proof.Propositional+ Proof.Propositional.Empty+ Proof.Propositional.Inhabited++ other-modules: Proof.Propositional.TH+ ghc-options: -Wall+ build-depends:+ base >=4 && <5+ , containers >=0.5 && <0.7+ , template-haskell >=2.11 && <2.22+ , void >=0.6 && <0.8+ , th-desugar >=1.8 && <1.17++ default-language: Haskell2010