Popular repositories Loading

1. HoTTClasses HoTTClasses Public

   HoTT proofs using experimental induction-induction (mostly about real numbers) (used to contain the HoTT.Classes proofs)

   Coq 15 5

2. HoTT-algebra HoTT-algebra Public archive

   Coq formalisation of algebra in Homotopy Type Theory

   Coq 7 1

3. rocq-sharing-analyser rocq-sharing-analyser Public

   Memory sharing analyser for Rocq (Coq)

   OCaml 6

4. coq-ltac2-compiler coq-ltac2-compiler Public

   OCaml 5

5. rocq rocq 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 3 2

6. ZF ZF Public

   Playing around with axiomatic set theory in Coq

   Coq 3 1