equational-reasoning

Proof assistant for Haskell using DataKinds & PolyKinds

LTS Haskell 16.23:0.6.0.3
Stackage Nightly 2020-11-23:0.6.0.3
Latest on Hackage:0.6.0.3

See all snapshots equational-reasoning appears in

BSD-3-Clause licensed by Hiromi ISHII
Maintained by konn.jinro_at_gmail.com
This version can be pinned in stack with:equational-reasoning-0.6.0.3@sha256:a59f45b15118add889948c3a3b25ed8cc324e01c088616302a5265db9ac451c8,1772

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