equational-reasoning

Proof assistant for Haskell using DataKinds & PolyKinds

Version on this page:	0.7.0.1@rev:2
LTS Haskell 20.16:	0.7.0.1@rev:3
Stackage Nightly 2023-03-26:	0.7.0.1@rev:3
Latest on Hackage:	0.7.0.1@rev: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.7.0.1@sha256:1bbd5f30e134106e935727441b7a472ad60e6512fbd37d25ae77d2df34e4243e,1943

Module documentation for 0.7.0.1

Proof
- Proof.Equational
- Proof.Propositional
  - Proof.Propositional.Empty
  - Proof.Propositional.Inhabited

Depends on 5 packages(full list with versions):

base, containers, template-haskell, th-desugar, void

Used by 4 packages in nightly-2023-02-03(full list with versions):

ghc-typelits-presburger, singletons-presburger, sized, type-natural

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.