Monadic effects and equational reasonig in Coq
-
Updated
May 24, 2024 - Coq
Monadic effects and equational reasonig in Coq
A Coq formalization of information theory and linear error-correcting codes
Multinomials for the Mathematical Components library.
A proof of Abel-Ruffini theorem.
Stable sort algorithms and their stability proofs in Coq
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
Formal power series in mathomp
Ring, field, lra, nra, and psatz tactics for Mathematical Components
Micromega tactics for Mathematical Components
Finite sets, finite maps, multisets and generic sets
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
The formal proof of the Odd Order Theorem
Add a description, image, and links to the ssreflect topic page so that developers can more easily learn about it.
To associate your repository with the ssreflect topic, visit your repo's landing page and select "manage topics."