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
#5409 - Case insensitivity can lead to lake builds which succeed when done "incrementally" but fail done together
Issue -
State: open - Opened by Julian about 22 hours ago
Labels: bug
#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
#5388 - matching on an `if _ then _ else _` gets reduced to `Decidable.rec` by `simp only`, which it then can't further simplify
Issue -
State: open - Opened by alexkeizer 3 days ago
Labels: bug, P-medium
#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
#5324 - Non-Linear Growth In Elaboration Time With A Number Of Local Vars Declared With Let
Issue -
State: open - Opened by gdncc 9 days ago
Labels: bug, P-low
#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
#5086 - RFC: Make "synthesized TC instance not defeq to expression inferred by typing" error easier to debug
Issue -
State: open - Opened by YaelDillies about 1 month ago
Labels: RFC, 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