metacoq
https://github.com/metacoq/metacoq
Coq
Metaprogramming in Coq
Triage Issues!
When you volunteer to triage issues, you'll receive an email each day with a link to an open issue that needs help in this project. You'll also receive instructions on how to triage issues.
Triage Docs!
Receive a documented method or class from your favorite GitHub repos in your inbox every day. If you're really pro, receive undocumented methods or classes and supercharge your commit history.
Coq not yet supported0 Subscribers
Add a CodeTriage badge to metacoq
Help out
- Issues
- Move some general utility lemmas from `TypingWf` to `All_Forall`
- Optimize `tmBind`
- Make `All` universe polymorphic
- Add a kludgy implementation of `tmTry`
- Adapt to coq/coq#16967 (increased kerpair checking)
- [Feature] Please add `tmTry`
- Please enable auto rebase from the web interface
- [Feature Request] Please allow scripting `#[export] Typeclasses Opaque foo.` in the template monad
- Error: Anomaly "Evar ?X40 was not declared." when running template programs with holes which involve `tmDefinition`
- Request: `tmOpenModule` and `tmCloseModule`
- Docs
- Coq not yet supported