ghc-proofs: GHC plugin to prove program equations by simplification
Often when writing Haskel code, one would like to prove things about the code.
A good example is writing an
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.
[Skip to Readme]
|Dependencies||base (>=4.9 && <4.11), ghc (>=8.2 && <8.4) [details]|
|Copyright||2017 Joachim Breitner|
|Category||Compiler Plugin, Formal Methods|
|Source repo||head: git clone git://github.com/nomeata/ghc-proofs.git|
|Uploaded||by JoachimBreitner at Tue Sep 5 13:00:25 UTC 2017|
|Downloads||401 total (27 in the last 30 days)|
|Rating||(no votes yet) [estimated by rule of succession]|
|Status||Docs uploaded by user [build log]
All reported builds failed as of 2017-09-05 [all 2 reports]
Hackage Matrix CI
For package maintainers and hackage trustees