coq
https://github.com/coq/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.
not yet supported9 Subscribers
Add a CodeTriage badge to coq
Help out
- Issues
- Unifying the syntax of Definition, Theorem, Fixpoint and CoFixpoint (CEP #42)
- Help with docker-coq/docker-mathcomp rebuilds: looking for a volunteer
- Experimenting beta-reducing terms displayed in some unification error messages
- Add `devShell` to `flake.nix` to allow nix-direnv to work
- Extend Derive with an arbitrary long sequence of dependencies
- Proper RR typechecker
- Ensure that andb_true_intro and andb_prop are transparent so that Scheme Equality computes
- Skip existential variable instances in Set Keep Admitted
- Timeout can go wrong in coqide
- Minimization of qualities is under-specific with Prop and Type
- Docs
- not yet supported