leanprover/lean4 issues and pull requests

#5508 - feat: add BitVec.getElem_[add|add_add_bool|mul|rotateLeft|rotateRight…

Pull Request - State: open - Opened by tobiasgrosser about 1 month ago - 5 comments
Labels: toolchain-available

#5497 - doc: update documentation and tests for `toUIntX` functions

Pull Request - State: closed - Opened by TomasPuverle about 1 month ago - 5 comments
Labels: toolchain-available

#5486 - feat: lake: Reservoir build cache

Pull Request - State: open - Opened by tydeu about 2 months ago - 1 comment
Labels: builds-mathlib, toolchain-available, release-ci

#5475 - Unbound fvar in "don't know how to synthesize implicit argument" error

Issue - State: closed - Opened by TomasPuverle about 2 months ago
Labels: bug, P-low

#5472 - feat: @[simp] lemmas about `List.toArray`

Pull Request - State: open - Opened by kim-em about 2 months ago - 1 comment
Labels: toolchain-available

#5471 - RFC: well-founded recursion: automatic `.attach` insertion

Issue - State: open - Opened by nomeata about 2 months ago - 3 comments
Labels: RFC, WIP, P-high

#5470 - doc: `contradiction` docstring indendation

Pull Request - State: closed - Opened by nomeata about 2 months ago - 1 comment
Labels: toolchain-available

#5469 - feat: add BitVec.[not_not, allOnes_shiftLeft_or_shiftLeft, allOnes_shiftLeft_and_shiftLeft]

Pull Request - State: closed - Opened by luisacicolini about 2 months ago - 1 comment
Labels: toolchain-available

#5468 - test: remove flaky test

Pull Request - State: closed - Opened by Kha about 2 months ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5467 - [Backport releases/v4.12.0] fix: changing whitespace after module header may break subsequent commands

Pull Request - State: closed - Opened by github-actions[bot] about 2 months ago

#5466 - feat: Array.foldX lemmas

Pull Request - State: closed - Opened by kim-em about 2 months ago - 1 comment
Labels: toolchain-available

#5465 - feat: improve Array GetElem lemmas

Pull Request - State: closed - Opened by kim-em about 2 months ago - 1 comment
Labels: toolchain-available

#5464 - feat: adjust simp attributes on monad lemmas

Pull Request - State: closed - Opened by kim-em about 2 months ago - 5 comments
Labels: builds-mathlib, toolchain-available

#5463 - chore: upstream some monad lemmas

Pull Request - State: closed - Opened by kim-em about 2 months ago - 2 comments
Labels: builds-mathlib, toolchain-available

#5462 - chore: update src/lake/lakefie.toml

Pull Request - State: closed - Opened by tydeu about 2 months ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5461 - chore: restore `@[simp]` on `Array.swapAt!_def`

Pull Request - State: closed - Opened by kim-em about 2 months ago - 1 comment
Labels: toolchain-available

#5460 - chore: missing List.set_replicate_self

Pull Request - State: closed - Opened by kim-em about 2 months ago - 1 comment
Labels: toolchain-available

#5459 - chore: missing BitVec lemmas

Pull Request - State: closed - Opened by kim-em about 2 months ago - 1 comment
Labels: toolchain-available

#5458 - chore: cleanup of Array docstrings after refactor

Pull Request - State: closed - Opened by kim-em about 2 months ago - 1 comment
Labels: toolchain-available

#5457 - bug: synthesizing `MonadLog` for a `StateT` is surprisingly slow

Issue - State: open - Opened by alexkeizer about 2 months ago
Labels: bug

#5456 - feat: add `heq_comm`

Pull Request - State: closed - Opened by kmill about 2 months ago - 1 comment
Labels: toolchain-available

#5455 - simp unfolds a local let with zetaDelta disabled

Issue - State: open - Opened by b-mehta about 2 months ago
Labels: bug

#5454 - chore: make some instance arguments implicit

Pull Request - State: closed - Opened by kim-em about 2 months ago - 1 comment
Labels: toolchain-available

#5453 - feature request: add lake require from the command line

Issue - State: open - Opened by kim-em about 2 months ago
Labels: feature, Lake

#5452 - feat: refactor of Array

Pull Request - State: closed - Opened by kim-em about 2 months ago - 1 comment
Labels: toolchain-available, release-ci

#5451 - chore: remove trailing and repeated spaces

Pull Request - State: closed - Opened by euprunin about 2 months ago - 2 comments
Labels: toolchain-available

#5450 - feat: add BitVec.toInt_[intMin|neg|neg_of_ne_intMin ]

Pull Request - State: closed - Opened by tobiasgrosser about 2 months ago - 2 comments
Labels: toolchain-available

#5449 - chore: update copyrights

Pull Request - State: closed - Opened by kim-em about 2 months ago - 1 comment
Labels: toolchain-available

#5448 - feat: add lemmas about `List.IsPrefix`

Pull Request - State: open - Opened by Command-Master about 2 months ago - 3 comments
Labels: awaiting-review, toolchain-available

#5447 - chore: update Pi instance names

Pull Request - State: closed - Opened by kim-em about 2 months ago - 1 comment
Labels: toolchain-available

#5446 - chore: cleanup after List.toArray refactor

Pull Request - State: open - Opened by kim-em about 2 months ago - 1 comment
Labels: help wanted, awaiting-review, toolchain-available, release-ci

#5445 - Json.parse does not handle surrogate pairs in string literals

Issue - State: open - Opened by eric-wieser about 2 months ago
Labels: bug

#5444 - chore: Mathlib's lean-pr-testing-NNNN branches should use Batteries' lean-pr-testing-NNNN branches

Pull Request - State: closed - Opened by kim-em about 2 months ago - 1 comment
Labels: toolchain-available

#5443 - Add `\U00000000` notation for large unicode literals

Pull Request - State: open - Opened by eric-wieser about 2 months ago - 4 comments
Labels: toolchain-available

#5442 - chore: release notes for 4.12.0

Pull Request - State: open - Opened by kmill about 2 months ago - 1 comment
Labels: toolchain-available

#5441 - chore: release notes for 4.12.0

Pull Request - State: closed - Opened by kmill about 2 months ago

#5440 - chore: fix spelling mistakes in RELEASES.md

Pull Request - State: closed - Opened by euprunin about 2 months ago - 1 comment
Labels: toolchain-available

#5439 - chore: fix spelling mistakes in tests

Pull Request - State: closed - Opened by euprunin about 2 months ago - 1 comment
Labels: toolchain-available

#5438 - chore: remove repeated words

Pull Request - State: closed - Opened by euprunin about 2 months ago - 1 comment
Labels: toolchain-available

#5437 - chore: remove (syntactically) duplicate imports

Pull Request - State: closed - Opened by euprunin about 2 months ago - 1 comment
Labels: toolchain-available

#5436 - chore: fix spelling mistakes in src/Lean/Meta/

Pull Request - State: closed - Opened by euprunin about 2 months ago - 1 comment
Labels: toolchain-available

#5435 - chore: fix spelling mistakes in src/Lean/Elab/

Pull Request - State: closed - Opened by euprunin about 2 months ago - 2 comments
Labels: toolchain-available

#5434 - chore: fix spelling mistakes in examples (doc/examples/)

Pull Request - State: closed - Opened by euprunin about 2 months ago - 2 comments
Labels: toolchain-available

#5433 - feat: present the bv_decide counter example at the API

Pull Request - State: closed - Opened by hargoniX about 2 months ago - 1 comment
Labels: toolchain-available

#5432 - fix: make `Repr` deriving instance handle explicit type parameters

Pull Request - State: closed - Opened by kmill about 2 months ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5431 - chore: fix spelling mistakes in src/Std/

Pull Request - State: closed - Opened by euprunin about 2 months ago - 1 comment
Labels: toolchain-available

#5430 - chore: fix spelling mistakes in non-Lean files

Pull Request - State: closed - Opened by euprunin about 2 months ago - 1 comment
Labels: toolchain-available

#5429 - perf: optimize unfolding constant lookup

Pull Request - State: open - Opened by Kha about 2 months ago - 5 comments
Labels: builds-mathlib, toolchain-available

#5428 - fix: worker: make sure to always report some recent range as progress when waiting

Pull Request - State: closed - Opened by Kha about 2 months ago - 2 comments
Labels: toolchain-available

#5427 - chore: fix spelling mistakes in src/Init/

Pull Request - State: closed - Opened by euprunin about 2 months ago - 1 comment
Labels: toolchain-available

#5426 - chore: fix spelling mistakes in src/Lean/

Pull Request - State: closed - Opened by euprunin about 2 months ago - 1 comment
Labels: toolchain-available

#5425 - chore: fix spelling mistakes in error messages/exceptions

Pull Request - State: closed - Opened by euprunin about 2 months ago - 1 comment
Labels: toolchain-available

#5424 - Signature formatter creates very long lines when many parameters share a type

Issue - State: open - Opened by david-christiansen about 2 months ago - 4 comments
Labels: bug

#5423 - feat: enhance the rewriting rules of bv_decide

Pull Request - State: closed - Opened by hargoniX about 2 months ago - 1 comment
Labels: toolchain-available

#5422 - feat: refactor DecidableEq (Array α)

Pull Request - State: closed - Opened by kim-em about 2 months ago - 1 comment
Labels: toolchain-available

#5421 - feat: implement `To/FromJSON Empty`

Pull Request - State: closed - Opened by TomasPuverle about 2 months ago - 3 comments
Labels: toolchain-available

#5420 - chore: make `Array` functions either semireducible or use structural recursion

Pull Request - State: closed - Opened by kim-em about 2 months ago - 1 comment
Labels: toolchain-available

#5419 - fix: must not reduce `ite` in the discriminant of match-expression when reducibility setting is `.reducible`

Pull Request - State: closed - Opened by leodemoura about 2 months ago - 3 comments
Labels: builds-mathlib, toolchain-available

#5418 - feat: decidable quantifers for BitVec

Pull Request - State: closed - Opened by kim-em about 2 months ago - 4 comments
Labels: toolchain-available

#5417 - `structure A; abbrev B := A; structure C extends B` fails

Issue - State: open - Opened by euprunin about 2 months ago - 3 comments
Labels: bug

#5416 - feat: add LawCommIdentity + IdempotentOp for BitVec.[and|or|xor]

Pull Request - State: closed - Opened by tobiasgrosser about 2 months ago - 3 comments
Labels: awaiting-review, toolchain-available

#5415 - feat: implement `Repr Empty`

Pull Request - State: closed - Opened by TomasPuverle about 2 months ago - 13 comments
Labels: builds-mathlib, toolchain-available

#5414 - Elaboration failure from interaction between `GetElem?` and default instances

Issue - State: open - Opened by kmill about 2 months ago
Labels: bug

#5413 - feat: add `_self`, `_zero`, and `_allOnes` for BitVec.[and|or|xor]

Pull Request - State: closed - Opened by tobiasgrosser about 2 months ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5412 - feat: expose Kernel.check for debugging purposes

Pull Request - State: open - Opened by nomeata about 2 months ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5411 - feat: BitVec.toNat_{add,sub,mul_of_lt} for BitVector non-overflow reasoning

Pull Request - State: closed - Opened by bollu about 2 months ago - 4 comments
Labels: toolchain-available

#5410 - feat: BitVec analogues of Nat.{mul_two, two_mul, mul_succ, succ_mul}

Pull Request - State: closed - Opened by bollu about 2 months ago - 1 comment
Labels: toolchain-available

#5409 - Case insensitivity can lead to lake builds which succeed when done "incrementally" but fail done together

Issue - State: open - Opened by Julian about 2 months ago
Labels: bug

#5408 - chore: basic cleanups for bv_decide

Pull Request - State: closed - Opened by hargoniX about 2 months ago - 1 comment
Labels: toolchain-available

#5407 - `exact?` suggests term that does not work

Issue - State: open - Opened by TwoFX about 2 months ago - 1 comment
Labels: bug, P-medium

#5406 - Structure update notation falls over optional parameters

Issue - State: closed - Opened by nomeata about 2 months ago - 1 comment
Labels: bug, P-medium

#5405 - chore: reverse direction of List.set_map

Pull Request - State: closed - Opened by kim-em about 2 months ago - 3 comments
Labels: builds-mathlib, toolchain-available

#5404 - feat: more of BitVec.getElem_*

Pull Request - State: closed - Opened by tobiasgrosser about 2 months ago - 3 comments
Labels: awaiting-review, toolchain-available, P-high

#5403 - feat: theorems about List.toArray

Pull Request - State: closed - Opened by kim-em about 2 months ago - 2 comments
Labels: builds-mathlib, toolchain-available

#5402 - feat: localize universe metavariable errors at `let` bindings and `fun` binders

Pull Request - State: closed - Opened by kmill about 2 months ago - 4 comments
Labels: awaiting-review, builds-mathlib, toolchain-available, P-high

#5401 - feat: instance for `Inhabited (TacticM α)`

Pull Request - State: closed - Opened by alexkeizer about 2 months ago - 1 comment
Labels: toolchain-available

#5400 - chore: reorganization in Array/Basic

Pull Request - State: closed - Opened by semorrison about 2 months ago - 1 comment
Labels: toolchain-available

#5399 - fix: upgrade instance synth order issues to hard errors

Pull Request - State: closed - Opened by kmill about 2 months ago - 6 comments
Labels: awaiting-review, builds-mathlib, toolchain-available

#5398 - doc: fix typo in docstring of `computeSynthOrder`

Pull Request - State: open - Opened by jcommelin about 2 months ago - 2 comments
Labels: toolchain-available

#5397 - RFC: Named arguments should not make explicit arguments implicit except for structure parameters

Issue - State: open - Opened by kmill about 2 months ago - 1 comment
Labels: RFC, awaiting-review, P-medium

#5396 - doc: mark «tacticHave'_:=_» as an alternative form of have'

Pull Request - State: closed - Opened by david-christiansen about 2 months ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5395 - `apply?` generates references to daggered assumptions

Issue - State: open - Opened by david-christiansen about 2 months ago
Labels: bug, P-medium

#5394 - feat: lemmas about List.maximum?

Pull Request - State: closed - Opened by semorrison about 2 months ago - 1 comment
Labels: toolchain-available

#5393 - feat: List.fold relators

Pull Request - State: closed - Opened by semorrison about 2 months ago - 1 comment
Labels: toolchain-available

#5392 - feat: List.fold / attach lemmas

Pull Request - State: closed - Opened by semorrison about 2 months ago - 1 comment
Labels: toolchain-available

#5391 - feat: review of List.erase / List.find lemmas

Pull Request - State: closed - Opened by semorrison about 2 months ago - 1 comment
Labels: toolchain-available

#5390 - chore: remove @[simp] from Bool.bne_assoc

Pull Request - State: closed - Opened by semorrison about 2 months ago
Labels: awaiting-mathlib

#5389 - fix: make formatter use current token table

Pull Request - State: closed - Opened by kmill about 2 months ago - 2 comments
Labels: builds-mathlib, toolchain-available

#5388 - matching on an `if _ then _ else _` gets reduced to `Decidable.rec` by `simp only`, which it then can't further simplify

Issue - State: closed - Opened by alexkeizer about 2 months ago - 1 comment
Labels: bug, P-medium

GitHub / leanprover/lean4 issues and pull requests