equational-reasoning
Proof assistant for Haskell using DataKinds & PolyKinds
| LTS Haskell 23.1: | 0.7.0.3@rev:1 |
| Stackage Nightly 2024-12-26: | 0.7.0.3@rev:1 |
| Latest on Hackage: | 0.7.0.3@rev:1 |
Maintained by konn.jinro_at_gmail.com
This version can be pinned in stack with:
equational-reasoning-0.7.0.3@sha256:fe66bd6c1a1083ceebedac5f355b41de4a2472072079f17f244a47de87a903ee,1215Module documentation for 0.7.0.3
Depends on 5 packages(full list with versions):
Used by 4 packages in nightly-2024-09-12(full list with versions):
Agda-style Equational Reasoning in Haskell by Data Kinds
What is this?
This library provides means to prove equations in Haskell. You can prove equations in Agda’s EqReasoning like style.
See blow for an example:
plusZeroL :: SNat m -> Zero :+: m :=: m
plusZeroL SZero = Refl
plusZeroL (SSucc m) =
start (SZero %+ (SSucc m))
=== SSucc (SZero %+ m) `because` plusSuccR SZero m
=== SSucc m `because` succCongEq (plusZeroL m)
It also provides some utility functions to use an induction.
For more detail, please read source codes!
TODOs
- Automatic generation for induction schema for any inductive types.