-
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 GNU Lesser General Public License v2.1 UpdatedMar 12, 2025 -
template-coq Public
Forked from MetaCoq/metacoqReflection library for Coq
OCaml MIT License UpdatedFeb 20, 2025 -
-
opam-coq-archive Public
Forked from coq/opamArchive for all Coq related OPAM packages organized in various repositories
JavaScript GNU Lesser General Public License v2.1 UpdatedJan 27, 2025 -
rocq-prover.org Public
Forked from coq/rocq-prover.orgThe Rocq Prover Website
HTML Other UpdatedJan 6, 2025 -
-
niloulsarvian.github.io Public
Forked from niloulsarvian/niloulsarvian.github.iothis is my personal website
HTML UpdatedNov 15, 2024 -
-
-
-
-
-
-
-
malfunction Public
Forked from stedolan/malfunctionMalfunctional Programming
OCaml Other UpdatedNov 10, 2023 -
-
-
-
autoinduct Public
Forked from tlringer/autoinductTaking a fun tactic implemented in class, and making it public for further refinement
Coq UpdatedJun 27, 2023 -
coq-library-undecidability Public
Forked from uds-psl/coq-library-undecidabilityA library of formalised undecidable problems in Coq
Coq Other UpdatedJun 23, 2023 -
logrel-coq Public
Forked from CoqHott/logrel-coqLogical Relation for MLTT in Coq
Coq UpdatedMar 28, 2023 -
-
-
-
coq-ceres Public
Forked from Lysxia/coq-ceresCoq library for serialization to S-expressions
Coq MIT License UpdatedJan 11, 2023 -
coq-tricks Public
Forked from rocq-community/coq-tricksTricks you wish the Coq manual told you
Coq UpdatedDec 21, 2022 -
-
-
-