name: ghc-proofs version: 0.1 synopsis: GHC plugin to prove program equations by simplification description: Often when writing Haskel code, one would like to prove things about the code. . A good example is writing an 'Applicative' or 'Monad' instance: there are equation that should hold, and checking them manually is tedious. . Wouldn’t it be nice if the compiler could check them for us? With this plugin, he can! (At least in certain simple cases – for everything else, you have to use a more dedicated solution.) . See the documentation in "GHC.Proof" or the project webpage for more examples and more information. category: Compiler Plugin, Formal Methods homepage: https://github.com/nomeata/ghc-proofs license: MIT license-file: LICENSE author: Joachim Breitner maintainer: mail@joachim-breitner.de copyright: 2017 Joachim Breitner build-type: Simple extra-source-files: ChangeLog.md, README.md cabal-version: >=1.10 Tested-With: GHC == 8.2.1, GHC == 8.3 source-repository head type: git location: git://github.com/nomeata/ghc-proofs.git library exposed-modules: GHC.Proof GHC.Proof.Plugin build-depends: base >=4.9 && <4.11 build-depends: ghc >= 8.2 && <8.4 default-language: Haskell2010 test-suite successors type: exitcode-stdio-1.0 hs-source-dirs: examples main-is: Successors.hs build-depends: ghc-proofs build-depends: base >=4.9 && <4.11 default-language: Haskell2010 ghc-options: -main-is Successors test-suite hlint type: exitcode-stdio-1.0 hs-source-dirs: examples main-is: HLint.hs build-depends: ghc-proofs build-depends: base >=4.9 && <4.11 build-depends: transformers default-language: Haskell2010 ghc-options: -main-is HLint