StructTact
Proof assistant library
A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants.
Coq utility and tactic library.
21 stars
31 watching
8 forks
Language: Coq
last commit: 12 months ago coqcoq-librarytactics
Related projects:
| Repository | Description | Stars |
|---|---|---|
 coq/platform | A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching | 188 |
 uds-psl/mpctt | A research project on using the Coq proof assistant to develop and prove mathematical models of computation in computational type theory | 80 |
 ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
| uwplse/pumpkin-pi | Automatically discovers and proves relationships between types in Coq to simplify proof development and code reuse. | 49 |
 andrew-johnson-4/lsts | A programming language and proof assistant built around type theory and lambda calculus. | 114 |
 mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 41 |
 ptival/haystac | A collection of Ltac tactics to help find specific mathematical proofs in Coq | 5 |
 whonore/coqtail | Enables interactive proof development in Vim similar to other proof assistants. | 274 |
| uwplse/cheerios | A formally verified serialization library for Coq | 23 |
 coq-community/coq-art | Coq proof assistant book with exercises and examples | 110 |
| uds-psl/autosubst2 | A tool for generating Coq code from syntactic theories with variable binders | 17 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 291 |
 deepspec/interactiontrees | A library for representing recursive and impure programs in the Coq proof assistant language. | 203 |
 matafou/libhyps | A Coq library providing tactics to manipulate hypotheses in formal proofs. | 20 |