Proof General

proofgeneral.github.iosite

Generic interface for proof assistants based on the extensible, customizable text editor Emacs.

from

Coq

added

2026-10-10

likes

0

similar

1. ▲
   Company-Coq github.com

   tool category #coq link ↗

   IDE extensions for Proof General's Coq mode.

   
2. ▲
   Trakt github.com

   tool category #coq link ↗

   Generic goal preprocessing tool for proof automation tactics.

   
3. ▲
   proof-using-helper.py github.com

   site category #coq link ↗

   Modifies source files to include proof annotations for faster parallel proving.

4. ▲
   Lean Proof Assistant lean-lang.org

   site category #theoretical-computer-science link ↗

   Lean Proof Assistant.

   
5. ▲
   FreeSpec github.com

   tool category #coq link ↗

   Framework for modularly verifying programs with effects and effect handlers.

6. ▲
   CoqHammer github.com

   tool category #coq link ↗

   General-purpose automated reasoning hammer tool that combines learning from previous proofs with the translation of problems to automated provers and the reconstruction of found proofs.

   

Coq › Projects > User Interfaces: “Generic interface for proof assistants based on the extensible, customizable text editor Emacs.”