LibHyps
Hypothesis manager
A Coq library providing tactics to manipulate hypotheses in formal proofs.
A Coq library providing tactics to deal with hypothesis
20 stars
3 watching
3 forks
Language: Coq
last commit: almost 2 years agoLinked from 2 awesome lists
coqformal-proofshypothesisproof-assistanttacticaltactics
coq-community/awesome-coq
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
 princeton-vl/coqgym | A learning environment for theorem proving with the Coq proof assistant | 388 |
 ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 amintimany/categories | An implementation of category theory in the Coq proof assistant. | 94 |
 ml4tp/gamepad | A platform that exposes Coq proofs to machine learning algorithms | 72 |
 snu-sf/paco | A Coq library for proving properties about stateful systems through parameterized coinduction | 43 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 292 |
 mgrabovsky/fm-notes | A collection of notes and resources on formal methods, type theory, and theorem proving using Coq. | 21 |
 mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 42 |
 unimath/unimath | Formalizes mathematics using the univalent point of view | 964 |
 vafeiadis/hahn | A collection of lemmas and tactics about lists and binary relations for a proof assistant | 30 |
 math-comp/mczify | A Coq library that enables the use of Micromega arithmetic solvers for goals stated with Mathematical Components definitions | 24 |
 ptival/haystac | A collection of Ltac tactics to help find specific mathematical proofs in Coq | 5 |
 uwplse/structtact | A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants. | 21 |
 jtassarotti/coq-proba | A Coq-based probability theory library providing results and definitions for discrete probability, measure theory, and probabilistic choice monads. | 50 |