gares Goto Github PK

aac-tactics

Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]

addon-elpi

Elpi addon plugin for jsCoq

addon-hierarchy-builder

addon-mathcomp

Mathematical Components addon for jsCoq

addons

A workspace for jsCoq addons

alectryon

A collection of tools for writing technical documents that mix Coq code and prose.

atd

Static types for JSON APIs

autoinduct

Taking a fun tactic implemented in class, and making it public for further refinement

autoview

bignums

Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library

category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work

ceps

Coq Enhancement Proposals

cfml

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 development of machine-checked proofs.

coq-defunctor

CEP62

coq-dpdgraph

Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]

coq-elpi

Coq plugin embedding elpi

coq-equations

A plugin for Coq to add dependent pattern-matching.

coq-lang

VSCode extensions providing syntax highlighting for Coq

coq-opam-snap

A snap for Coq built using opam

coq-performance-tests

A library of Coq source files testing for performance regressions on Coq [maintainer=@JasonGross]

coq-serapi

Coq Protocol Playground with Se(xp)rialization of Internal Structures.

coq-simple-io

IO for Gallina

coq-tools

Some scripts to help construct small reproducing examples of bugs, implement [Proof using], etc.

coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

coqoon-opam

OPAM integration for Coqoon

coqws17

Coq Winter School 2017

coqws18

Coq winter school 2018

coqwshulk

cws16

coq winter school 2016