Popularity
8.2
Stable
Activity
0.0
-
49
6
5
Monthly Downloads: 13
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.
-
-
subhask
Type safe interface for working in subcategories of Hask -
vector
An efficient implementation of Int-indexed arrays (both mutable and immutable), with a powerful loop optimisation framework . -
statistics
A fast, high quality library for computing with statistics in Haskell. -
linear
Low-dimensional linear algebra primitives for Haskell. -
what4
Symbolic formula representation and solver interaction library -
HerbiePlugin
GHC plugin that improves Haskell code's numerical stability -
hgeometry
HGeometry is a library for computing with geometric objects in Haskell. It defines basic geometric types and primitives, and it implements some geometric data structures and algorithms. The main two focusses are: (1) Strong type safety, and (2) implementations of geometric algorithms and data structures that have good asymptotic running time guarantees. -
dimensional
Dimensional library variant built on Data Kinds, Closed Type Families, TypeNats (GHC 7.8+). -
computational-algebra
General-Purpose Computer Algebra System as an EDSL in Haskell -
-
hermit
Haskell Equational Reasoning Model-to-Implementation Tunnel -
matrix
A Haskell native implementation of matrices and their operations. -
mwc-random
A very fast Haskell library for generating high quality pseudo-random numbers. -
lambda-calculator
An introduction to the Lambda Calculus -
-
-
numhask
A haskell numeric prelude, providing a clean structure for numbers and operations that combine them. -
vector-space
Vector & affine spaces, linear maps, and derivatives -
poly
Fast polynomial arithmetic in Haskell (dense and sparse, univariate and multivariate, usual and Laurent) -
-
cf
"Exact" real arithmetic for Haskell using continued fractions (Not formally proven correct) -
optimization
Some numerical optimization methods implemented in Haskell -
bayes-stack
Framework for Gibbs sampling of probabilistic models -
rampart
:european_castle: Determine how intervals relate to each other. -
monte-carlo
A Monte Carlo monad and transformer for Haskell. -
bed-and-breakfast
Matrix operations in 100% pure Haskell -
simple-smt
A simple way to interact with an SMT solver process. -
safe-decimal
Safe and very efficient arithmetic operations on fixed decimal point numbers -
sbvPlugin
Formally prove properties of Haskell programs using SBV/SMT. -
polynomial
Haskell library for manipulating and evaluating polynomials -
monoid-subclasses
Subclasses of Monoid with a solid theoretical foundation and practical purposes -
eigen
Haskel binding for Eigen library. Eigen is a C++ template library for linear algebra: matrices, vectors, numerical solvers, and related algorithms. -
manifold-random
Coordinate-free hypersurfaces as Haskell types -
modular-arithmetic
A useful type for working with integers modulo some constant. -
shapes-math
physics engine and other tools for 2D shapes
Updating dependencies is time-consuming.
Solutions like Dependabot or Renovate update but don't merge dependencies. You need to do it manually while it could be fully automated! Add a Merge Queue to your workflow and stop caring about PR management & merging. Try Mergify for free.
Promo
blog.mergify.com
* Code Quality Rankings and insights are calculated and provided by Lumnify.
They vary from L1 to L5 with "L5" being the highest.
Do you think we are missing an alternative of equational-reasoning or a related project?
|
Static code analysis for 29 languages.
sponsored
www.sonarqube.org
|
Popular Comparisons
-
equational-reasoningvscontinued-fractions
-
equational-reasoningvslambda-calculator
-
equational-reasoningvsoptimization
-
equational-reasoningvsnimber
-
hmatrixvshmatrix-repa
|
Collect and Analyze Billions of Data Points in Real Time
sponsored
www.influxdata.com
|
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.