Popularity
8.1
Growing
Activity
4.9

42
3
5
Monthly Downloads: 543
Programming language: Haskell
License: BSD 3clause "New" or "Revised" License
Tags:
Math
Latest version: v0.6.0.3
equationalreasoning alternatives and similar packages
Based on the "Math" category

statistics
A library of statistical types, data, and functions 
HerbiePlugin
automatically improve your code's numeric stability 
estimator
Statespace estimation algorithms such as Kalman Filters 
computationalalgebra
Wellkinded computational algebra library, currently supporting Groebner basis. 
mwcrandom
Fast, high quality pseudo random number generation 
vectorspace
Vector & affine spaces, linear maps, and derivatives 
bayesstack
Framework for inferring generative probabilistic models with Gibbs sampling 
montecarlo
A monad and transformer for Monte Carlo calculations. 
mathfunctions
Special functions and Chebyshev polynomials 
hgeometry
Geometric Algorithms, Data structures, and Data types. 
sbvPlugin
Formally prove properties of Haskell programs using SBV/SMT 
arrayfire
Haskell bindings to the ArrayFire generalpurpose GPU library 
safedecimal
Safe and very efficient arithmetic operations on fixed decimal point numbers 
shapesmath
faster vector/matrix math using unboxed numbers and Template Haskell 
simplesmt
A simple way to interact with an SMT solver process. 
vectorthunbox
Deriver for Data.Vector.Unboxed using Template Haskell 
vectorbinaryinstances
Instances of Data.Binary and Data.Serialize for vector 
diagramssolve
Pure Haskell solver routines used by diagrams 
manifoldrandom
Sampling random points on general manifolds. 
linearaccelerate
Instances to use linear vector spaces on accelerate backends 
uncertain
Manipulating numbers with inherent experimental/measurement uncertainty 
vectorinstances
Orphan Instances for 'Data.Vector'
* Code Quality Rankings and insights are calculated and provided by Lumnify.
They vary from L1 to L5 with "L5" being the highest. Visit our partner's website for more details.
Do you think we are missing an alternative of equationalreasoning or a related project?
README
Agdastyle 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.