Coq-Equations
rupicola
Coq-Equations | rupicola | |
---|---|---|
1 | 3 | |
209 | 48 | |
- | - | |
6.8 | 7.7 | |
8 days ago | 9 days ago | |
Coq | Coq | |
GNU Lesser General Public License v3.0 only | MIT License |
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.
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).
rupicola
What are some alternatives?
mathlib - Lean 3's obsolete mathematical components library: please use mathlib4
UniMath - This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
coq-library-undecidability - A library of mechanised undecidability proofs in the Coq proof assistant.
proofs - My personal repository of formally verified mathematics.
toychain - A minimalistic blockchain consensus implemented and verified in Coq
math-comp - Mathematical Components
ttlite - A SuperCompiler for Martin-Löf's Type Theory
verdi-raft - An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
principia - The Principia Rewrite
magmide - A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
CompCert - The CompCert formally-verified C compiler