Popular repositories Loading

1. coq coq Public

   Forked from rocq-prover/rocq

   Coq 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

2. coq-hit coq-hit Public

   Coq and Higher Inductive Types

3. Coq-Equations Coq-Equations Public

   Forked from mattam82/Coq-Equations

   A plugin for Coq to add dependent pattern-matching.

   OCaml

4. coq-bitset coq-bitset Public

   Forked from artart78/coq-bitset

   Coq

5. cic-model-1 cic-model-1 Public

   Forked from barras/cic-model

   Set-theoretical models of various type theories (up to an extensional version of the Calculus of Inductive Constructions), aiming at proving logical consistency and strong normalization

   Coq

6. template-coq template-coq Public

   Forked from MetaRocq/metarocq

   Reflection library for Coq

   OCaml