The mprover package

[Tags: bsd3, program]

MProver is a proof checker for equational reasoning in a Haskell-like language. This is an extremely preliminary release, so don't expect it to be terribly useful just yet!

[Skip to ReadMe]


Change logNone available
Dependenciesbase (<6), containers (>=, haskell98, mtl (>=, parsec (>=3.1.1), pretty (>=, transformers (>=, unbound (>=0.3.1) [details]
AuthorAdam Procter and Aaron Stump
MaintainerAdam Procter <>
CategoryTheorem Provers
UploadedThu Dec 15 11:14:55 UTC 2011 by AdamProcter
Downloads227 total (14 in last 30 days)
0 []
StatusDocs not available [build log]
All reported builds failed as of 2015-09-30 [all 4 reports]


Maintainers' corner

For package maintainers and hackage trustees

Readme for mprover-


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[1].

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):

  $ mp

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 <>

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.