Popular repositories Loading

1. compileo compileo Public

2. rocq rocq Public

   Forked from rocq-prover/rocq

   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

3. coq-lsp coq-lsp Public

   Forked from ejgallego/rocq-lsp

   Visual Studio Code Extension and Language Server Protocol for Coq

   OCaml

4. rocq-lean-import rocq-lean-import Public

   Forked from rocq-community/rocq-lean-import

   OCaml

5. metarocq metarocq Public

   Forked from MetaRocq/metarocq

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

   Coq

6. paramcoq paramcoq Public

   Forked from rocq-community/paramcoq

   Old Coq plugin for parametricity [maintainer=@ppedrot]

   Coq