equational-reasoning 0.7.0.2 → 0.7.0.3
raw patch · 3 files changed
+73/−24 lines, 3 filesdep ~containersPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: containers
API changes (from Hackage documentation)
- Proof.Propositional.Empty: instance Proof.Propositional.Empty.Empty Data.Void.Void
+ Proof.Propositional.Empty: instance Proof.Propositional.Empty.Empty GHC.Base.Void
- Proof.Equational: [:-] :: x -> HVec xs -> HVec (x : xs)
+ Proof.Equational: [:-] :: x -> HVec xs -> HVec (x ': xs)
- Proof.Equational: data (a :: k) :~: (b :: k)
+ Proof.Equational: data () => (a :: k) :~: (b :: k)
- Proof.Equational: data Proxy (t :: k)
+ Proof.Equational: data () => Proxy (t :: k)
Files
- Changelog.md +20/−0
- README.md +30/−0
- equational-reasoning.cabal +23/−24
+ Changelog.md view
@@ -0,0 +1,20 @@+Changelog+==========++## 0.7.0.2++- Supports GHC 9.8+- Drops support for GHC <9++## 0.6.0.3++- Support for GHC >= 8.10++## 0.6.0.2++- Adds support for th-desugar-1.11++## 0.6.0.1++- Supports GHC 8.8.+- Adds support for th-desugar-1.10 (Thanks: Justin Le @mstksg)
+ README.md view
@@ -0,0 +1,30 @@+Agda-style Equational Reasoning in Haskell by Data Kinds+=========================================================+[](https://travis-ci.org/konn/equational-reasoning-in-haskell) [](https://hackage.haskell.org/package/equational-reasoning)++What is this?+--------------+This library provides means to prove equations in Haskell.+You can prove equations in Agda's EqReasoning like style.++See blow for an example:++```haskell+plusZeroL :: SNat m -> Zero :+: m :=: m+plusZeroL SZero = Refl+plusZeroL (SSucc m) =+ start (SZero %+ (SSucc m))+ === SSucc (SZero %+ m) `because` plusSuccR SZero m+ === SSucc m `because` succCongEq (plusZeroL m)++```++It also provides some utility functions to use an induction.++For more detail, please read source codes!+++TODOs+------++* Automatic generation for induction schema for any inductive types.
equational-reasoning.cabal view
@@ -1,28 +1,27 @@-name: equational-reasoning-version: 0.7.0.2-synopsis: Proof assistant for Haskell using DataKinds & PolyKinds+cabal-version: 3.4+name: equational-reasoning+version: 0.7.0.3+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+license: BSD-3-Clause+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+ ghc ==9.0.2 || ==9.2.8 || ==9.4.8 || ==9.6.5 || ==9.8.2 -cabal-version: >=1.10+extra-doc-files:+ Changelog.md+ README.md source-repository head- type: git+ type: git location: git://github.com/konn/equational-reasoning-in-haskell.git library@@ -32,13 +31,13 @@ Proof.Propositional.Empty Proof.Propositional.Inhabited - other-modules: Proof.Propositional.TH- ghc-options: -Wall+ 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+ base >=4 && <5,+ containers >=0.5 && <0.7,+ template-haskell >=2.11 && <2.23,+ th-desugar >=1.8 && <1.18,+ void >=0.6 && <0.8, default-language: Haskell2010