Popularity
8.2
Stable
Activity
2.1
Declining
45
4
5

Monthly Downloads: 106
Programming language: Haskell
License: BSD 3-clause "New" or "Revised" License
Tags: Math    
Latest version: v0.6.0.3

equational-reasoning alternatives and similar packages

Based on the "Math" category.
Alternatively, view equational-reasoning alternatives based on common mentions on social networks and blogs.

Do you think we are missing an alternative of equational-reasoning or a related project?

Add another 'Math' Package

README

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.