Simple equational reasoning for a Haskell-ish language
|Latest on Hackage:||0.0.0.0|
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.
This is a highly preliminary release of MProver, a simple (I hope!) proof
checker for equational reasoning in (a subset of) Haskell. It is released
in the spirit, though not under the exact terms, of the CRAPL.
To build and install, use the standard incantation, viz.:
$ runhaskell Setup.hs configure
$ runhaskell Setup.hs build
$ runhaskell Setup.hs install
To launch the REPL (note that loading modules for use in the REPL is not
supported yet, so you may find this a bit useless):
To run the proof checker against an example MProver script:
$ mp examples/Test.hs
If you have any questions or comments, please write:
Adam Procter <firstname.lastname@example.org>
In particular, I'd be glad to send you a draft copy of a conference paper,
currently under review, that outlines MProver's design.
Enjoy at your own risk!
Some particular bugs/limitations/to-do items of note:
* The guardedness check is not implemented yet.
* Program terms are not type checked (!)
* Type classes are not implemented yet.
* Case-proofs must be exhaustive; this is not actually checked for yet.