Agda-style equational reasoning in Haskell
Haskell
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
Proof
.gitignore
.travis.yml
LICENSE
README.md
Setup.hs
equational-reasoning.cabal
stack-800.yaml
stack-802.yaml
stack-804.yaml
stack.yaml

README.md

Agda-style Equational Reasoning in Haskell by Data Kinds

Build Status Hackage

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.