-
coq.github.io Public
Forked from coq/coq.github.ioSource files of the coq.inria.fr website
HTML Other UpdatedNov 11, 2024 -
metaprogramming-rosetta-stone Public
Forked from coq-community/metaprogramming-rosetta-stoneA rosetta stone for metaprogramming in Coq, with different examples of tactics, plugins, etc implemented in different metaprogramming languages [maintainer=@yforster]
Coq MIT License UpdatedJun 30, 2023 -
llvm-project Public
Forked from llvm/llvm-projectThe LLVM Project is a collection of modular and reusable compiler and toolchain technologies. Note: the repository does not accept github pull requests at this moment. Please submit your patches at…
Other UpdatedJan 1, 2023 -
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 UpdatedOct 1, 2022 -
rouge Public
Forked from rouge-ruby/rougeA pure-ruby code highlighter that is compatible with pygments http://rouge.jneen.net/
Ruby Other UpdatedSep 9, 2022 -
nixos-weekly Public
Forked from NixOS/nixos-weeklyNixOS Weekly Newsletter
HTML Creative Commons Attribution Share Alike 4.0 International UpdatedMar 26, 2021 -
opam-coq-archive Public
Forked from coq/opamArchive for all Coq related OPAM packages organized in various repositories
-
-
coq-smt-check Public
Invoke SMT solvers from Coq to check obligations
-
-
-
coq-apply-any Public archive
An extension to eauto that allows you to apply an arbitrary lemma from a hint database
-
-
mirror-core Public
A framework for extensible, reflective decision procedures.
-
coq-seal Public
Implementation of sealing in Coq with macros for generation
-
template-coq Public
Forked from MetaCoq/metacoqReflection library for Coq
-
coq-extensible-records Public
Implementation of extensible records in Coq
-
-
-
clang Public
Forked from llvm-mirror/clangMirror of official clang git repository located at http://llvm.org/git/clang. Updated every five minutes.
C++ Other UpdatedMar 13, 2019 -
coq-plugin-utils Public
Useful utility functions for writing Coq plugins
-
InteractionTrees Public
Forked from DeepSpec/InteractionTreesFormalization of the Interaction Tree Datatype in Coq
Coq MIT License UpdatedJan 17, 2019 -
-
coq-interaction-trees Public
Co-inductive interaction trees provide a way to represent (potentially) non-terminating programs with I/O behavior.
-
-
category-theory Public
Forked from jwiegley/category-theoryA formalization of category theory in Coq for personal study and practical work
Coq UpdatedMar 18, 2018 -
fraxl Public
Forked from ElvishJerricco/fraxlHaskell BSD 3-Clause "New" or "Revised" License UpdatedFeb 12, 2018 -
Haskell-Foldl-Library Public
Forked from Gabriella439/foldlComposable, streaming, and efficient left folds
Haskell BSD 3-Clause "New" or "Revised" License UpdatedJan 18, 2018 -
CTRex.hs Public
Forked from strake/CTRex.hsOpen records for Haskell
Haskell Other UpdatedAug 24, 2017 -
CTRex-aeson.hs Public
Forked from strake/CTRex-aeson.hsAeson instances for CTRex records
Haskell BSD 3-Clause "New" or "Revised" License UpdatedAug 24, 2017