Proof assistant for Haskell using DataKinds & PolyKinds

Version on this page:
LTS Haskell 15.6:
Stackage Nightly 2020-04-05:
Latest on Hackage:

See all snapshots equational-reasoning appears in

BSD-3-Clause licensed by Hiromi ISHII
Maintained by konn.jinro_at_gmail.com

Module documentation for

This version can be pinned in stack with:[email protected]:8a1422fb4a79f19d3e95e73f721aa764968e12768b5e2d2e2940e2db71d2e452,1737

A simple convenient library to write equational / preorder proof as in Agda. Since, this no longer depends on singletons package, and the Proof.Induction module goes to equational-reasoning-induction package.