Pinned Loading

1. rocq-prover/rocq rocq-prover/rocq Public

   The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…

   OCaml 5k 679

2. MetaRocq/metarocq MetaRocq/metarocq Public

   Metaprogramming, verified meta-theory and implementation of Rocq in Rocq

   Coq 437 88

3. HoTT/Coq-HoTT HoTT/Coq-HoTT Public

   A Coq library for Homotopy Type Theory

   Coq 1.3k 197

4. Coq-Equations Coq-Equations Public

   A function definition package for Coq

   Coq 228 49

5. rocq-prover/opam rocq-prover/opam Public

   Archive for all Rocq and Coq-related opam packages organized in various repositories

   OCaml 138 169

6. unicoq/unicoq unicoq/unicoq Public

   An enhanced unification algorithm for Coq

   OCaml 55 17