doubly-generic
Arity-generic datatype-generic, or doubly-generic, programming in Coq. (by jeanpehk)
Coq-Equations
A function definition package for Coq (by mattam82)
| doubly-generic | Coq-Equations | |
|---|---|---|
| 1 | 1 | |
| 4 | 209 | |
| - | - | |
| 0.0 | 6.8 | |
| almost 3 years ago | 10 days ago | |
| Coq | Coq | |
| MIT License | GNU Lesser General Public License v3.0 only |
The number of mentions indicates the total number of mentions that we've tracked plus the number of user suggested alternatives.
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.
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.
doubly-generic
Posts with mentions or reviews of doubly-generic.
We have used some of these posts to build our list of alternatives
and similar projects.
Coq-Equations
Posts with mentions or reviews of Coq-Equations.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2021-05-02.
-
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?
When comparing doubly-generic and Coq-Equations you can also consider the following projects:
mathlib - Lean 3's obsolete mathematical components library: please use mathlib4
coq-library-undecidability - A library of mechanised undecidability proofs in the Coq proof assistant.
toychain - A minimalistic blockchain consensus implemented and verified in Coq
ttlite - A SuperCompiler for Martin-Löf's Type Theory
principia - The Principia Rewrite
rupicola - Gallina to Bedrock2 compilation toolkit