leanprover-community/batteries

Issues

• Bug: `simp?` does not take reverse directions into account

  #264 opened a year ago by sgouezel
  2

• Fixed width signed integer datatypes.

  #472 opened a year ago by joehendrix
  3

• `simpNF` should use dsimp for lemmas proved by `rfl`

  #86 opened 2 months ago by digama0
  3

• `runLinter` should determine the target module by asking Lake

  #795 opened 2 months ago by kim-em
  2

• Syntax for creating concrete HashMaps

  #726 opened 2 months ago by austinletson
  3

• `#print prefix` elaborator crashes language server downstream of Mathlib

  #995 opened 2 months ago by mhuisi
  0

• `proof_wanted` is linted for unused arguments

  #938 opened 3 months ago by YaelDillies
  2

• Add docker / gitpod integrations

  #565 opened a year ago by alexjbest
  3

• False positive from the unusedHavesSuffices linter

  #428 opened a year ago by kim-em
  5

• alias does not open namespaces

  #810 opened 7 months ago by YaelDillies
  0

• `#where` doesn't print `open scoped`

  #778 opened 8 months ago by fpvandoorn
  0

• Missing lemma about `Sum.elim`

  #685 opened 9 months ago by madvorak
  6

• Usage examples for HashMap.lean

  #469 opened 9 months ago by digama0
  2

• `List.pmap`, but for proofs only and O(1)

  #711 opened 9 months ago by digama0
  2

• Documentation instructions are out of date.

  #333 opened 9 months ago by joehendrix
  3

• Do not make `#guard_msgs` sensitive to whitespace and line breaks

  #717 opened 9 months ago by Seasawher
  3

• Bugs in `ext` tactic

  #618 opened 10 months ago by fgdorais
  2

• Installation instruction confusion

  #689 opened 10 months ago by mars0i
  5

• simpNF complains if LHS contains higher-order function

  #671 opened 10 months ago by timotree3
  0

• `omega` does not support powers.

  #500 opened 10 months ago by ericrbg
  2

• Array.minX functions are buggy

  #431 opened a year ago by Blei
  4

• `omega` fails when an extra divisibility hypothesis is added

  #562 opened a year ago by dwrensha
  1

• `omega` has issues with `mdata` handling

  #509 opened a year ago by girving
  1

• bug: MVarId.isIndependentOf doesn't check local context.

  #424 opened a year ago by joehendrix
  0

• `omega` only wants constants on one side.

  #499 opened a year ago by ericrbg
  0

• `omega` doesn't understand `n ≠ 0`

  #482 opened a year ago by girving
  2

• Int.ofNat_natAbs_eq_of_nonneg and Int.natAbs_of_nonneg seem duplicates

  #419 opened a year ago by Ruben-VandeVelde
  2

• Document std4#232

  #402 opened a year ago by fgdorais
  0

• Update stable branch to v4.3.0

  #414 opened a year ago by fgdorais
  1

• After import Std, the behavior of HMod.hMod of Int changed without warning.

  #411 opened a year ago by JiechengZhao
  5

• Missing release tag for v4.3.0-rc2

  #391 opened a year ago by fgdorais
  1

• simpNF linter does not handle conditional simp lemmas correctly

  #365 opened a year ago by eric-wieser
  0

• Codify style guide

  #336 opened a year ago by digama0
  0

• Codify naming conventions

  #335 opened a year ago by joehendrix
  0

• Code action for induction ... using ...

  #311 opened a year ago by PatrickMassot
  1

• Build fails: Failed to syntesize instance

  #319 opened a year ago by yetanotherus3r
  1

• Automate testing against Mathlib?

  #309 opened a year ago by joehendrix
  6

• Signature of ``BitVec.shiftLeft, BitVec.ushiftRight, BitVec.sshiftRight, BitVec.zeroExtend`` does not match SMT-LIB

  #302 opened a year ago by PratherConid
  14

• Upstream various lemmas about sublists to Std

  #307 opened a year ago by eric-wieser
  0

• docBlame linter requires docstrings on propositional structure fields

  #217 opened a year ago by eric-wieser
  0

• over-zealous `cases` code action

  #270 opened a year ago by kbuzzard
  0

• rcases doesn't seem to support ?_ placeholders

  #116 opened 2 years ago by Ruben-VandeVelde
  1

• `simpNF` gives false positives when the LHS simplifies by a lower priority lemma

  #207 opened a year ago by kim-em
  0

• List.mem_reverse has more explicit arguments than in mathlib3

  #90 opened a year ago by Ruben-VandeVelde
  1

• incorrect output from `linter.unnecessarySimpa`

  #180 opened a year ago by kbuzzard
  0

• show_term auto bound interaction and by?

  #167 opened 2 years ago by alexjbest
  0

• `simpNF` linter rejecting working simp lemma

  #71 opened 2 years ago by kbuzzard
  3

• Consider removing RBTree.ofList

  #117 opened 2 years ago by Ruben-VandeVelde
  3

• `dupNamespace` linter should ignore aux lemmas

  #103 opened 2 years ago by urkud
  0

• `@[norm_cast move]` is broken

  #79 opened 2 years ago by gebner
  0