Popularity
8.1
Growing
Activity
4.9
-
42
3
5
Monthly Downloads: 543
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
-
statistics
A library of statistical types, data, and functions -
HerbiePlugin
automatically improve your code's numeric stability -
estimator
State-space estimation algorithms such as Kalman Filters -
computational-algebra
Well-kinded computational algebra library, currently supporting Groebner basis. -
mwc-random
Fast, high quality pseudo random number generation -
vector-space
Vector & affine spaces, linear maps, and derivatives -
bayes-stack
Framework for inferring generative probabilistic models with Gibbs sampling -
monte-carlo
A monad and transformer for Monte Carlo calculations. -
math-functions
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 general-purpose GPU library -
safe-decimal
Safe and very efficient arithmetic operations on fixed decimal point numbers -
shapes-math
faster vector/matrix math using unboxed numbers and Template Haskell -
simple-smt
A simple way to interact with an SMT solver process. -
vector-th-unbox
Deriver for Data.Vector.Unboxed using Template Haskell -
vector-binary-instances
Instances of Data.Binary and Data.Serialize for vector -
diagrams-solve
Pure Haskell solver routines used by diagrams -
manifold-random
Sampling random points on general manifolds. -
linear-accelerate
Instances to use linear vector spaces on accelerate backends -
uncertain
Manipulating numbers with inherent experimental/measurement uncertainty -
vector-instances
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 equational-reasoning or a related project?
README
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.