rupicola
CoqEquations
rupicola  CoqEquations  

3  1  
51  219  
    
7.6  8.1  
11 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
CoqEquations

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.
coqlibraryundecidability  A library of mechanised undecidability proofs in the Coq proof assistant.
mathcomp  Mathematical Components
toychain  A minimalistic blockchain consensus implemented and verified in Coq
verdiraft  An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
ttlite  A SuperCompiler for MartinLöf's Type Theory
magmide  A dependentlytyped proof language intended to make provably correct bare metal code possible for working software engineers.
principia  The Principia Rewrite
CompCert  The CompCert formallyverified C compiler