Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / leanprover/lean4 issues and pull requests

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

Pull Request - State: open - Opened by bollu about 19 hours ago - 1 comment
Labels: toolchain-available

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

Pull Request - State: open - Opened by bollu about 20 hours ago - 1 comment
Labels: toolchain-available

#5408 - chore: basic cleanups for bv_decide

Pull Request - State: closed - Opened by hargoniX 1 day ago - 1 comment
Labels: toolchain-available

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

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

#5406 - Structure update notation falls over optional parameters

Issue - State: open - Opened by nomeata 1 day ago - 1 comment
Labels: bug, P-medium

#5405 - chore: reverse direction of List.set_map

Pull Request - State: open - Opened by semorrison 1 day ago - 1 comment
Labels: awaiting-mathlib, breaks-mathlib, toolchain-available

#5404 - feat: more of BitVec.getElem_*

Pull Request - State: open - Opened by tobiasgrosser 1 day ago - 1 comment
Labels: toolchain-available, P-high

#5403 - feat: theorems about List.toArray

Pull Request - State: open - Opened by semorrison 1 day ago - 1 comment
Labels: awaiting-mathlib, breaks-mathlib, toolchain-available

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

Pull Request - State: open - Opened by kmill 1 day ago - 2 comments
Labels: awaiting-review, builds-mathlib, toolchain-available, P-high

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

Pull Request - State: closed - Opened by alexkeizer 1 day ago - 1 comment
Labels: toolchain-available

#5400 - chore: reorganization in Array/Basic

Pull Request - State: closed - Opened by semorrison 1 day ago - 1 comment
Labels: toolchain-available

#5399 - fix: downgrade instance synth order issues to warnings

Pull Request - State: open - Opened by kmill 1 day ago - 4 comments
Labels: awaiting-review, builds-mathlib, toolchain-available

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

Pull Request - State: open - Opened by jcommelin 1 day 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 1 day 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 2 days ago - 1 comment
Labels: builds-mathlib, toolchain-available

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

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

#5394 - feat: lemmas about List.maximum?

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

#5393 - feat: List.fold relators

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

#5392 - feat: List.fold / attach lemmas

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

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

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

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

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

#5389 - fix: make formatter use current token table

Pull Request - State: open - Opened by kmill 3 days ago - 2 comments
Labels: builds-mathlib, toolchain-available

#5387 - Metavariable assignment can fail if created underneath `let`

Issue - State: open - Opened by kmill 3 days ago
Labels: bug, P-low

#5386 - RFC: Named arguments in explicit mode should not be able to make parameters become implicit

Issue - State: closed - Opened by kmill 3 days ago - 1 comment
Labels: RFC, awaiting-review

#5385 - feat: add BitVec.ofBool_[and|or|xor]_ofBool theorems

Pull Request - State: closed - Opened by tobiasgrosser 3 days ago - 3 comments
Labels: toolchain-available

#5384 - unwanted reduction when checking simp_arith proof objects

Issue - State: open - Opened by nomeata 3 days ago
Labels: bug, P-low

#5383 - Hover for _ argument shows irrelevant information

Issue - State: open - Opened by TwoFX 3 days ago
Labels: bug, P-low

#5382 - chore: fixes spurious omega error in #5315

Pull Request - State: closed - Opened by semorrison 3 days ago - 2 comments
Labels: toolchain-available

#5381 - chore: cleaning up redundant simp lemmas

Pull Request - State: closed - Opened by semorrison 3 days ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5380 - feat: missing Fin @[simp] lemmas

Pull Request - State: closed - Opened by semorrison 3 days ago - 8 comments
Labels: builds-mathlib, toolchain-available

#5379 - chore: remove some @[simp]s from Fin lemmas

Pull Request - State: closed - Opened by semorrison 3 days ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5378 - chore: modify signature of lemmas about mergeSort

Pull Request - State: closed - Opened by semorrison 3 days ago - 1 comment
Labels: toolchain-available

#5377 - chore: upstream map_mergeSort

Pull Request - State: closed - Opened by semorrison 3 days ago - 1 comment
Labels: toolchain-available

#5376 - fix: modify projection instance binder info

Pull Request - State: closed - Opened by leodemoura 3 days ago - 16 comments
Labels: builds-mathlib, toolchain-available

#5375 - feat: add `bv_decide` normalization rules for `ofBool (a.getLsbD i)` and `ofBool a[i]`

Pull Request - State: closed - Opened by alexkeizer 4 days ago - 2 comments
Labels: toolchain-available

#5374 - feat: add Nonempty instances for products

Pull Request - State: closed - Opened by david-christiansen 4 days ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5373 - chore: fix name of List.length_mergeSort

Pull Request - State: closed - Opened by semorrison 4 days ago - 1 comment
Labels: toolchain-available

#5372 - doc: add Verso to release checklist process

Pull Request - State: closed - Opened by david-christiansen 4 days ago - 1 comment
Labels: toolchain-available

#5370 - feat: HashSet.partition (unverified)

Pull Request - State: closed - Opened by semorrison 4 days ago - 1 comment
Labels: toolchain-available

#5369 - feat: HashSet.ofArray (unverified)

Pull Request - State: closed - Opened by semorrison 4 days ago - 1 comment
Labels: breaks-mathlib, toolchain-available

#5368 - fix: consistently show non-mvar term in hovertext

Pull Request - State: open - Opened by Aaron1011 5 days ago - 1 comment
Labels: toolchain-available, P-low

#5367 - Hovering over underscore (`_`) shows type, but not term

Issue - State: open - Opened by Aaron1011 5 days ago - 1 comment
Labels: bug, P-medium

#5366 - “implicit lambda” works with `exact`, but not `apply`

Issue - State: open - Opened by nomeata 5 days ago - 8 comments
Labels: bug, P-low

#5365 - feat: bv_decide diagnosis

Pull Request - State: closed - Opened by hargoniX 5 days ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5364 - feat: FunInd: more equalities in context, more careful cleanup

Pull Request - State: closed - Opened by nomeata 5 days ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5363 - RFC: 'Measure time to cancellation' option

Issue - State: open - Opened by mhuisi 5 days ago - 2 comments
Labels: RFC, P-high

#5362 - refactor: remove the last use of Lean.(HashSet|HashMap)

Pull Request - State: closed - Opened by hargoniX 5 days ago - 8 comments
Labels: builds-mathlib, toolchain-available

#5361 - feat: some BitVec GetElem lemmas

Pull Request - State: closed - Opened by semorrison 5 days ago - 1 comment
Labels: toolchain-available

#5359 - chore: ensure that the `rfl` tactic tries `Iff.rfl`

Pull Request - State: closed - Opened by Parcly-Taxel 5 days ago - 18 comments
Labels: builds-mathlib, toolchain-available

#5358 - chore: introduce BitVec.setWidth to unify zeroExtend and truncate

Pull Request - State: closed - Opened by tobiasgrosser 5 days ago - 5 comments
Labels: toolchain-available

#5347 - incorrect functional induction principle

Issue - State: closed - Opened by BrunoDutertre 7 days ago - 4 comments
Labels: bug

#5346 - feat: qsort with proven bounds and correctness proof

Pull Request - State: open - Opened by lyphyser 7 days ago - 10 comments
Labels: breaks-mathlib, toolchain-available

#5345 - Can't use `attribute [semireducible]` on well-founded definitions.

Issue - State: open - Opened by semorrison 7 days ago - 2 comments
Labels: bug, P-low

#5342 - RFC: lake: add command to fetch dependency sources

Issue - State: open - Opened by JLimperg 8 days ago - 1 comment
Labels: RFC, P-medium

#5340 - fix: shutdown deadlock and crash desync

Pull Request - State: open - Opened by mhuisi 8 days ago - 2 comments
Labels: builds-mathlib, toolchain-available

#5339 - Deprecate and remove `Array` literal patterns

Issue - State: open - Opened by Kha 8 days ago - 4 comments

#5338 - perf: do not lint unused variables defined in tactics by default

Pull Request - State: open - Opened by Kha 8 days ago - 1 comment
Labels: breaks-mathlib, toolchain-available

#5336 - Elaborator doesn't produce `InfoTree` for incomplete `match` and incomplete terms in `apply`

Issue - State: open - Opened by mhuisi 8 days ago - 1 comment
Labels: bug, P-medium

#5335 - fix: unused variable false positive when combining alias and non-lexical use

Pull Request - State: closed - Opened by Kha 8 days ago - 3 comments
Labels: builds-mathlib, toolchain-available

#5334 - Parser docstring vs syntax hover target audience confusion

Issue - State: open - Opened by nomeata 8 days ago
Labels: bug, new-user-papercuts, P-medium

#5333 - modifying TC synth order can give 2% speedup of mathlib

Issue - State: closed - Opened by jcommelin 8 days ago - 1 comment

#5332 - chore: notation ^^ for Bool.xor

Pull Request - State: closed - Opened by semorrison 8 days ago - 7 comments
Labels: builds-mathlib, toolchain-available

#5330 - lake: could not materialize package

Issue - State: open - Opened by jcommelin 8 days ago - 2 comments
Labels: bug, Lake, P-medium

#5326 - `bv_decide` counterexample validation

Issue - State: closed - Opened by leodemoura 8 days ago
Labels: bug, feature, P-medium

#5321 - Excessive memory consumption for processing simple file.

Issue - State: closed - Opened by gruhn 9 days ago - 3 comments
Labels: bug

#5315 - Error: unexpected bound variable #0

Issue - State: closed - Opened by BrunoDutertre 10 days ago - 1 comment
Labels: bug, P-high

#5265 - chore: remove unused deriving handler argument syntax

Pull Request - State: open - Opened by david-christiansen 16 days ago - 3 comments
Labels: breaks-mathlib, toolchain-available

#5236 - Deprecate and remove `inductive` ... `:=`

Issue - State: open - Opened by david-christiansen 19 days ago - 5 comments
Labels: bug, P-medium

#5093 - Internal error due to lazy definition realization and backtracking

Issue - State: open - Opened by nomeata about 1 month ago - 1 comment
Labels: bug, P-medium

#4904 - feat: add date and time functionality

Pull Request - State: open - Opened by algebraic-dev about 2 months ago - 6 comments
Labels: awaiting-author, toolchain-available, P-high

#4768 - fix: do not ban `..` with a `.` on the next line

Pull Request - State: closed - Opened by eric-wieser 2 months ago - 6 comments
Labels: awaiting-review, toolchain-available, P-medium

#4729 - feat: have IR checker suggest `noncomputable`

Pull Request - State: closed - Opened by kmill 2 months ago - 2 comments
Labels: toolchain-available, P-medium

#4714 - `linter.unusedVariables` false positive when using `match` and `assumption`

Issue - State: closed - Opened by TwoFX 2 months ago
Labels: bug, P-medium

#4708 - chore: reorganise lemmas on list getters

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

#4305 - doc: explain the borrow syntax

Pull Request - State: closed - Opened by eric-wieser 4 months ago - 2 comments
Labels: awaiting-review, toolchain-available, P-medium

#4149 - fix: FunInd: Introduce HEq where necessary and no equality on Props

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

#4146 - FunInd chokes on pattern match with dependent targets

Issue - State: closed - Opened by nomeata 4 months ago
Labels: bug, P-medium

#4090 - RFC: let `unfold` tactic zeta reduce local definitions

Issue - State: closed - Opened by kmill 5 months ago - 3 comments
Labels: RFC, RFC accepted, P-medium

#3718 - refactor: back `rfl` tactic only via `apply_rfl`

Pull Request - State: open - Opened by nomeata 6 months ago - 5 comments
Labels: builds-mathlib, toolchain-available, changes-stage0

#3714 - feat: apply_rfl tactic: handle Eq, HEq, better error messages

Pull Request - State: closed - Opened by nomeata 6 months ago - 4 comments
Labels: builds-mathlib, toolchain-available, P-medium

#3293 - isDefEq fails in presence of unassignable metavariable

Issue - State: open - Opened by kmill 7 months ago - 3 comments
Labels: bug, P-low

#3219 - "failed to generate equational theorem" with nested matches

Issue - State: open - Opened by soulsource 8 months ago - 2 comments
Labels: bug, P-medium

#3213 - Eta-expansion of `Prop`-structures

Issue - State: open - Opened by arthur-adjedj 8 months ago
Labels: bug, P-low

#3211 - RFC: Support http proxy

Issue - State: open - Opened by Landau1994 8 months ago - 1 comment
Labels: RFC, P-low

#3192 - LLVM vs C backend performance

Issue - State: closed - Opened by hargoniX 8 months ago - 2 comments
Labels: bug

#3182 - fix: make lean4 build on FreeBSD

Pull Request - State: open - Opened by yurivict 8 months ago - 2 comments
Labels: awaiting-author, toolchain-available

#3181 - Please make installing LICENSE and LICENSES files optional based on a cmake option

Issue - State: closed - Opened by yurivict 8 months ago - 6 comments
Labels: bug

#3177 - lean4 installs files into a non-standard location src/lean

Issue - State: open - Opened by yurivict 8 months ago - 20 comments
Labels: bug, P-low

#3162 - RFC: Signed Fixed-width Integer Support

Issue - State: open - Opened by pnwamk 8 months ago - 8 comments
Labels: RFC, P-high

#3160 - feat: manage nested inductive types in `deriving`

Pull Request - State: open - Opened by arthur-adjedj 8 months ago - 28 comments
Labels: awaiting-review, breaks-mathlib, toolchain-available, P-medium

#3150 - Bug leading to stack overflow

Issue - State: open - Opened by alreadydone 9 months ago - 5 comments
Labels: bug, P-medium

#3146 - Unification bug

Issue - State: open - Opened by jthulhu 9 months ago
Labels: bug, P-medium

#2204 - Issue finding `Inhabited` instances in partial definition

Issue - State: open - Opened by fgdorais over 1 year ago - 3 comments

#2083 - [cmake] Build Files Generator not pinned to Unix Makefiles

Issue - State: closed - Opened by iacore over 1 year ago - 3 comments

#1867 - passing instances to named arguments turns explicit args into implicit

Issue - State: open - Opened by digama0 almost 2 years ago - 4 comments

#1774 - compiler produces `(kernel) function expected`

Issue - State: open - Opened by fpfu almost 2 years ago - 1 comment
Labels: depends on new code generator