Skip to content

Issues: leanprover-community/batteries

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

23 Open 38 Closed
23 Open 38 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

alias does not open namespaces
#810 opened May 25, 2024 by YaelDillies
runLinter should determine the target module by asking Lake
#795 opened May 13, 2024 by kim-em
1
2
#where doesn't print open scoped
#778 opened May 2, 2024 by fpvandoorn
Add docker / gitpod integrations
#565 opened Jan 26, 2024 by alexjbest
3
Fixed width signed integer datatypes.
#472 opened Dec 20, 2023 by joehendrix
2
False positive from the unusedHavesSuffices linter
#428 opened Dec 8, 2023 by kim-em
5
simpNF linter does not handle conditional simp lemmas correctly
#365 opened Nov 15, 2023 by eric-wieser
Codify style guide
#336 opened Oct 30, 2023 by digama0
Codify naming conventions
#335 opened Oct 30, 2023 by joehendrix
Code action for induction ... using ...
#311 opened Oct 21, 2023 by PatrickMassot
1
Automate testing against Mathlib?
#309 opened Oct 20, 2023 by joehendrix
6
Upstream various lemmas about sublists to Std
#307 opened Oct 19, 2023 by eric-wieser
Bug: simp? does not take reverse directions into account
#264 opened Sep 15, 2023 by sgouezel
1
simpNF gives false positives when the LHS simplifies by a lower priority lemma
#207 opened Aug 6, 2023 by kim-em
incorrect output from linter.unnecessarySimpa
#180 opened Jul 7, 2023 by kbuzzard
rcases doesn't seem to support ?_ placeholders
#116 opened Apr 16, 2023 by Ruben-VandeVelde
1
simpNF should use dsimp for lemmas proved by rfl
#86 opened Jan 13, 2023 by digama0
1
@[norm_cast move] is broken
#79 opened Jan 8, 2023 by gebner
simpNF linter rejecting working simp lemma
#71 opened Dec 21, 2022 by kbuzzard
3
rcases can't use rfl on 0 = a in some circumstances.
#62 opened Dec 8, 2022 by kim-em
6
RBMap etc. should take typeclasses, not explicit comparators
#51 opened Dec 3, 2022 by Kha
Cover mathlib theorems for RBMap
#27 opened Nov 17, 2022 by arienmalec
copyFile
#2 opened Sep 1, 2022 by lovettchris
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.