★ wanayoo — archive 1999 https://github.com/math-comp/math-comp/issuesNouvelle recherche | Portail wanayoo
Skip to content

/ math-comp

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.

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

84 Open 145 Closed
84 Open 145 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels.
Projects
Filter by project
Milestones
Filter by milestone
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀
Wrong error message when trying to unfold with a pattern
#684 opened Dec 10, 2020 by ybertot
1
`pairwise` predicate kind: enhancement
#676 opened Nov 25, 2020 by pi8027 1.13.0
1
@pi8027
Remove the deprecation aliases for `eq_sorted` and attribute them to new lemmas kind: clean-up
#648 opened Nov 13, 2020 by pi8027 1.13.0
Meta-issue: dropping support for Coq 8.10 drops: coq 8.10
#645 opened Nov 12, 2020 by CohenCyril 1.13.0
Quite a bit of lemmas are missing between + - .+1 .-1
#643 opened Nov 12, 2020 by CohenCyril
The relationship between `n_comp` and `partition`
#642 opened Nov 12, 2020 by chdoc
Missing lemma `cycle_all2rel` kind: enhancement
#639 opened Nov 10, 2020 by pi8027
1
@pi8027
Dealing with list membership in the absence of equality. needs: discussion
#638 opened Nov 10, 2020 by chdoc
Put `by move=> _; elim: s` with the first line using a `; last first ...`
#635 opened Nov 8, 2020 by CohenCyril
Switch to Coq's deprecation mechanism drops: coq 8.10
#634 opened Nov 6, 2020 by gares 1.13.0
Cleanup : Adding bigop lemmas for ring : expr_sum and prodr_natmul kind: clean-up
#623 opened Oct 30, 2020 by thery 1.13.0
Missing sorting lemmas specialized for `orderType`
#622 opened Oct 29, 2020 by pi8027
1
@pi8027
Sequences ordered by the suffix-relation
#621 opened Oct 29, 2020 by pi8027
2
Missing lemmas of membership equality
#620 opened Oct 29, 2020 by pi8027
2
Missing subset lemmas
#619 opened Oct 29, 2020 by pi8027
1
Using "positional suffixes" for `mulnDl`, `mulnDr` and the like needs: discussion
#617 opened Oct 25, 2020 by CohenCyril
More order instances for standard types.
#615 opened Oct 16, 2020 by arthuraa
1
Modular lattice of linear subspaces kind: enhancement
#613 opened Oct 11, 2020 by pi8027 1.13.0
1
@pi8027
3
`leq_addr` vs `ltn_addr` (and `addl` variants)
#609 opened Oct 9, 2020 by chdoc
7
Old comments mentioning unsupported versions of Coq kind: clean-up
#606 opened Oct 8, 2020 by pi8027
rename `mem_imset_eq` and `mem_imset2_eq` and remove deprecation aliases kind: clean-up
#602 opened Oct 1, 2020 by chdoc 1.13.0
remove `big_uncond` kind: clean-up
#590 opened Sep 9, 2020 by CohenCyril 1.14.0
rename: `big_uncond` -> `big_rmcond` & remove `big_uncond_in` kind: clean-up
#589 opened Sep 9, 2020 by CohenCyril 1.13.0
Does one use `matrix` or `mx`? kind: refactoring needs: discussion
#581 opened Sep 8, 2020 by CohenCyril 1.13.0
1
@CohenCyril
2
Spacing convention before `//` kind: documentation kind: style
#580 opened Sep 7, 2020 by CohenCyril
1
ProTip! Adding no:label will show everything without a label.
You can’t perform that action at this time.