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. coq-lean-import coq-lean-import Public

   OCaml 8 3

3. HoTT-algebra HoTT-algebra Public archive

   Coq formalisation of algebra in Homotopy Type Theory

   Coq 7 1

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

   OCaml 5

5. rocq-sharing-analyser rocq-sharing-analyser Public

   Memory sharing analyser for Rocq (Coq)

   OCaml 5

6. coq coq Public

   Forked from coq/coq

   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