REPLICA: REPL Instrumentation for Coq Analysis
-
Updated
Jan 2, 2020 - Python
REPLICA: REPL Instrumentation for Coq Analysis
Coq plugin for printing term abstract syntax trees and their digests
A tutorial on how to write OCaml tactics for the Coq proof assistant
An API for interfacing with Coq through Tactician by external agents
Coq plugin for plain dependency extraction
Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
Certified implementation in Coq of Stålmarck's algorithm for proving tautologies [maintainer=@palmskog]
Fixpoint to eliminator translation in Coq
A rosetta stone for metaprogramming in Coq, with different examples of tactics, plugins, etc implemented in different metaprogramming languages [maintainer=@yforster]
Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]
Library of useful utility functions for Coq plugins
A Coq plugin to add reduction side effects to some Coq reduction strategies [maintainers=@liyishuai,@JasonGross]
An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
Template project for Coq plugins using the Dune build system, showcasing some advanced features [maintainer=@ejgallego]
A standalone implementation of Ltac2 as a Coq plugin. Now part of the main Coq repository.
A Seamless, Interactive Tactic Learner and Prover for Coq
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
Add a description, image, and links to the coq-plugin topic page so that developers can more easily learn about it.
To associate your repository with the coq-plugin topic, visit your repo's landing page and select "manage topics."