ghc-proofs

GHC plugin to prove program equations by simplification

https://github.com/nomeata/ghc-proofs

Latest on Hackage:0.1.1

This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow stackage.org to host generated Haddocks.

MIT licensed by Joachim Breitner
Maintained by [email protected]

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.