equational-reasoning

Proof assistant for Haskell using DataKinds & PolyKinds

LTS Haskell 17.4:0.6.0.4
Stackage Nightly 2021-02-25:0.7.0.0
Latest on Hackage:0.7.0.0

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.7.0.0@sha256:b15b8d427326b972c61b91d8faee5554b230ca4f451833e1d48c965dd85015a4,1894

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.