Skip to content

Issues: coq-community/math-classes

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

10 Open 23 Closed
10 Open 23 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Port Coq code to use done tactic instead of easy and benchmark help wanted
#128 opened Jul 9, 2024 by palmskog
4
Please suggest example file for Coq Platform "smoke test kit"
#106 opened Sep 24, 2021 by MSoegtropIMC
1
RingOrder for types with decidable equality
#99 opened May 31, 2021 by mdgeorge4153
2
Use universe polymorphism to eliminate ua_subalgebraT.v help wanted
#66 opened Nov 17, 2018 by spitters
Autogenerate dependency graphs, documentation with travis
#62 opened Aug 24, 2018 by spitters
@Zimmi48
1
Fix inner product space laws
#49 opened Mar 29, 2018 by langston-barrett
notation overwrite warnings
#47 opened Nov 25, 2017 by vzaliva
Is there a Decision procedure for ≤ on Rationals?
#31 opened Feb 10, 2017 by langston-barrett
2
Why does rationals_le use the concrete type nat?
#30 opened Feb 10, 2017 by langston-barrett
1
canonical_names.v overwrites a lot of standard notation
#28 opened Feb 4, 2017 by langston-barrett
2
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.