-
coq-dpdgraph Public
Forked from rocq-community/coq-dpdgraphBuild dependency graphs between COQ objects
-
opam-coq-archive Public
Forked from rocq-prover/opamArchive for all Coq related OPAM packages organized in various repositories
-
-
-
pi-agm Public
A formal description in Coq of computations of PI using arithmetic-geometric means
-
stdlib Public
Forked from rocq-prover/stdlibStdlib for the Rocq Prover
Rocq Prover GNU Lesser General Public License v2.1 UpdatedJul 31, 2025 -
Coq-Equations Public
Forked from mattam82/Coq-EquationsA function definition package for Coq
Coq GNU Lesser General Public License v2.1 UpdatedJun 26, 2025 -
platform-docs Public
Forked from rocq-prover/platform-docsA project of short tutorials and how-to guides for Coq features and Coq Platform packages.
Coq Other UpdatedApr 22, 2025 -
coq Public
Forked from rocq-prover/rocqCoq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…
OCaml GNU Lesser General Public License v2.1 UpdatedDec 13, 2024 -
-
coq-elpi Public
Forked from LPCIC/coq-elpiCoq plugin embedding elpi
OCaml GNU Lesser General Public License v2.1 UpdatedNov 14, 2024 -
math-comp.github.io Public
Forked from math-comp/math-comp.github.iohttps://math-comp.github.io/
HTML UpdatedOct 10, 2024 -
reachout_math Public
internship on making more easily accessible formalized mathematics using Coq
-
-
hierarchy-builder Public
Forked from math-comp/hierarchy-builderHigh level commands to declare a hierarchy based on packed classes
Prolog MIT License UpdatedApr 19, 2024 -
math-comp-nix Public
Forked from math-comp/math-comp-nixNix support for mathcomp packages
Nix GNU General Public License v3.0 UpdatedMar 7, 2024 -
awesome-coq Public
Forked from rocq-community/awesome-coqA curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainers=@anton-trunov,@palmskog]
Creative Commons Zero v1.0 Universal UpdatedFeb 12, 2024 -
itp-conference.github.io Public
Forked from itp-conference/itp-conference.github.ioHTML UpdatedDec 12, 2023 -
platform Public
Forked from rocq-prover/platformMulti platform setup for Coq, Coq libraries and tools
Shell Creative Commons Zero v1.0 Universal UpdatedNov 3, 2023 -
breadth_first_search Public
A generic algorithm for breadth first search, in Coq, with proofs
-
coq-lsp Public
Forked from ejgallego/rocq-lspLanguage Server Protocol and VS Code Extension for Coq
OCaml GNU Lesser General Public License v2.1 UpdatedJan 26, 2023 -
Formal-proofs-for-the-convergence-of-visibility-walks-in-triangulations Public
Forked from cneyrand/Formal-proofs-for-the-convergence-of-visibility-walks-in-triangulations -
coq-art Public
Forked from rocq-community/coq-artCoq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
Coq MIT License UpdatedJul 20, 2022 -
real-closed Public
Forked from math-comp/real-closedTheorems for Real Closed Fields
Coq UpdatedJul 5, 2022 -
coqeal Public
Forked from rocq-community/coqealThe Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
Coq Other UpdatedMay 6, 2022 -
fourcolor Public
Forked from rocq-community/fourcolorFormal proof of the Four Color Theorem
Coq UpdatedMar 29, 2022 -
semantics Public
Forked from rocq-community/semanticsA survey of semantics styles in Coq, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation [maintainer=@k4rtik]
Coq MIT License UpdatedMar 4, 2022 -
-
extructures Public
Forked from arthuraa/extructuresFinite sets and maps for Coq with extensional equality
Coq MIT License UpdatedOct 27, 2021 -
analysis Public
Forked from math-comp/analysisMathematical Components compliant Analysis Library
Coq Other UpdatedOct 12, 2021
{{ message }}