This aims to be a very simple theorem prover (nay, verifier) based on functional expression rewriting to educate myself and others about the basics of theorem provers.
It also has types to ensure the expressions are not nonsensical.
Examples are on the examples directory.
for instructions on installation and how to prove your theorems in nnoq, see tutorial.