package coq-coqeal
CoqEAL - The Coq Effective Algebra Library
Install
Dune Dependency
Authors
Maintainers
Sources
2.1.0.tar.gz
sha512=5d771d442a403bdf38a8d159df38299e6409f248a6a7b62b9608dae1df440ec796067ce16ecd3b6088d47a07cf5b6f0bc9eceb75aacb8a9ca9c63a80f597d00b
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: 18 Feb 2025
Dependencies (7)
-
coq-mathcomp-real-closed
>= "2.0" -
coq-mathcomp-multinomials
>= "2.0" - coq-mathcomp-algebra
-
coq-mathcomp-ssreflect
>= "2.3" & < "2.5~" -
coq-hierarchy-builder
>= "1.4.0" -
coq-elpi
>= "2.5.0" & < "3.2~" - coq-bignums
Dev Dependencies (1)
-
coq
(>= "8.20" & < "9.1~") | (= "dev")
Used by (3)
- coq-mathcomp-apery
-
coq-prosa
>= "0.5" - coq-validsdp
Conflicts
None
On This Page