package coq-coqeal
CoqEAL - The Coq Effective Algebra Library
Install
Dune Dependency
Authors
Maintainers
Sources
2.1.1.tar.gz
sha512=49e8b603d4c8f19d4f34ddc204f21f94a790d31e27cdec6a19ec0840d4db927c8e433c31f60446b2f705181d12b42495660462f5f2e124eb6a29ced1abc0ca50
Description
This Coq library contains a subset of the work that was developed in the context of the ForMath EU FP7 project (2009-2013). It has two parts:
- theory, which contains developments in algebra including normal forms of matrices, and optimized algorithms on MathComp data structures.
- refinements, which is a framework to ease change of data representations during a proof.
Tags
category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms keyword:effective algebra keyword:elementary divisor rings keyword:Smith normal form keyword:mathematical components keyword:Bareiss keyword:Karatsuba multiplication keyword:refinements logpath:CoqEALPublished: 08 Dec 2025
Dependencies (7)
-
coq-mathcomp-real-closed
>= "2.0" -
coq-mathcomp-multinomials
>= "2.0" - coq-mathcomp-algebra
-
coq-mathcomp-ssreflect
>= "2.3" & < "2.6~" -
coq-hierarchy-builder
>= "1.4.0" -
coq-elpi
>= "2.5.0" - coq-bignums
Dev Dependencies (1)
-
coq
(>= "8.20" & < "9.2~") | (= "dev")
Used by (4)
Conflicts
None
On This Page