rupicola
Coq-Equations
Our great sponsors
rupicola | Coq-Equations | |
---|---|---|
3 | 1 | |
48 | 209 | |
- | - | |
7.7 | 6.8 | |
8 days ago | 7 days ago | |
Coq | Coq | |
MIT License | GNU Lesser General Public License v3.0 only |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
rupicola
Coq-Equations
-
Learn coq or agda before diving into idris2?
I'd say Agda is more similar to Idris than Coq. Coq has a different syntax and isn't as good for programming with dependent types as Agda and Idris (Agda and Idris both put a huge emphasis on dependent pattern matching, something that Coq only recently gained support for through the Equations package).
What are some alternatives?
UniMath - This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
mathlib - Lean 3's obsolete mathematical components library: please use mathlib4
proofs - My personal repository of formally verified mathematics.
coq-library-undecidability - A library of mechanised undecidability proofs in the Coq proof assistant.
math-comp - Mathematical Components
toychain - A minimalistic blockchain consensus implemented and verified in Coq
verdi-raft - An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
ttlite - A SuperCompiler for Martin-Löf's Type Theory
magmide - A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
principia - The Principia Rewrite
CompCert - The CompCert formally-verified C compiler