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

25 Open 32 Closed
25 Open 32 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
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 Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

#where doesn't print open scoped
#778 opened May 2, 2024 by fpvandoorn
Syntax for creating concrete HashMaps
#726 opened Apr 10, 2024 by austinletson
Add docker / gitpod integrations
#565 opened Jan 26, 2024 by alexjbest
2
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 semorrison
4
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 semorrison
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 semorrison
5
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
Achieve parity between Array and List lemmas
#24 opened Nov 1, 2022 by mpenciak
4
Port PersistentHashMaps from Lean core
#23 opened Nov 1, 2022 by mpenciak
Port HashSets from Lean core
#22 opened Nov 1, 2022 by mpenciak
copyFile
#2 opened Sep 1, 2022 by lovettchris
ProTip! Exclude everything labeled bug with -label:bug.