mini-prover

Term project for TaPL. A mini coq-like proof assistant.

Usage

System Requirement

Linux or macOS, currently not tested on Windows.
The Haskell Tool Stack

Compiling

stack build

Execution

stack exec mini-prover-exe

For verbose output:

stack exec mini-prover-exe -- -v[0-3]

Demos

See ./demo/demo.v.

Unit Test

stack test

Detail

See ./tex/report.