equational-reasoning

Proof assistant for Haskell using DataKinds & PolyKinds

Version on this page:0.6.0.4
LTS Haskell 22.11:0.7.0.2
Stackage Nightly 2024-02-22:0.7.0.2
Latest on Hackage:0.7.0.2

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.4@sha256:a90cd27f6aa33d238fcac95295ea0bbe573581b3f31c4cc5bb406562184ae9bd,1723

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.