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]
|Versions [RSS]||0.1, 0.1.1|
|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 2017-09-05T13:00:25Z|
|Reverse Dependencies||1 direct, 0 indirect [details]|
|Downloads||1540 total (1 in the last 30 days)|
|Rating||(no votes yet) [estimated by Bayesian average]|
|Status||Docs uploaded by user [build log]
All reported builds failed as of 2017-09-05 [all 2 reports]