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

#5376 - fix: modify projection instance binder info

Pull Request - State: closed - Opened by leodemoura about 2 months 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 about 2 months ago - 2 comments
Labels: toolchain-available

#5374 - feat: add Nonempty instances for products

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

#5373 - chore: fix name of List.length_mergeSort

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

#5372 - doc: add Verso to release checklist process

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

#5370 - feat: HashSet.partition (unverified)

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

#5369 - feat: HashSet.ofArray (unverified)

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

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

Pull Request - State: open - Opened by Aaron1011 about 2 months ago - 1 comment
Labels: toolchain-available, P-low

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

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

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

Issue - State: open - Opened by nomeata about 2 months ago - 8 comments
Labels: bug, P-low

#5365 - feat: bv_decide diagnosis

Pull Request - State: closed - Opened by hargoniX about 2 months 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 about 2 months ago - 1 comment
Labels: builds-mathlib, toolchain-available

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

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

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

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

#5361 - feat: some BitVec GetElem lemmas

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

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

Pull Request - State: closed - Opened by Parcly-Taxel about 2 months 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 about 2 months ago - 5 comments
Labels: toolchain-available

#5347 - incorrect functional induction principle

Issue - State: closed - Opened by BrunoDutertre about 2 months ago - 4 comments
Labels: bug

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

Pull Request - State: open - Opened by lyphyser about 2 months ago - 15 comments
Labels: awaiting-author, breaks-mathlib, toolchain-available

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

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

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

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

#5340 - fix: shutdown deadlock and crash desync

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

#5339 - Deprecate and remove `Array` literal patterns

Issue - State: open - Opened by Kha 2 months ago - 4 comments

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

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

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

Issue - State: open - Opened by mhuisi 2 months 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 2 months ago - 3 comments
Labels: builds-mathlib, toolchain-available

#5334 - Parser docstring vs syntax hover target audience confusion

Issue - State: open - Opened by nomeata 2 months 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 2 months ago - 1 comment

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

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

#5330 - lake: could not materialize package

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

#5327 - `bv_decide`: support for shifting by a natural number

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

#5326 - `bv_decide` counterexample validation

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

#5323 - refactor: redefine unsigned fixed width integers in terms of BitVec

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

#5321 - Excessive memory consumption for processing simple file.

Issue - State: closed - Opened by gruhn 2 months ago - 3 comments
Labels: bug

#5315 - Error: unexpected bound variable #0

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

#5312 - fix: changing whitespace after module header may break subsequent commands

Pull Request - State: closed - Opened by Kha 2 months ago - 1 comment
Labels: toolchain-available, backport releases/v4.12.0

#5283 - fix: refine how named arguments suppress explicit arguments

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

#5281 - feat: add udiv/umod bitblasting for bv_decide

Pull Request - State: open - Opened by bollu 2 months ago - 3 comments
Labels: awaiting-author, toolchain-available, P-high

#5265 - chore: remove unused deriving handler argument syntax

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

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

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

#5140 - feat: `debug.proofAsSorry`

Pull Request - State: open - Opened by Kha 3 months ago - 2 comments

#5135 - feat: use libuv for tempfiles

Pull Request - State: closed - Opened by hargoniX 3 months ago - 3 comments
Labels: toolchain-available, release-ci

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

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

#5024 - fix: make `rcases` tactic collect new goals

Pull Request - State: open - Opened by kmill 3 months ago - 2 comments
Labels: breaks-mathlib, toolchain-available, release-ci

#4904 - feat: add date and time functionality

Pull Request - State: open - Opened by algebraic-dev 3 months ago - 6 comments
Labels: awaiting-review, breaks-mathlib, toolchain-available, P-high

#4902 - feat: async kernel checking for theorems

Pull Request - State: open - Opened by Kha 3 months ago - 14 comments
Labels: breaks-mathlib, toolchain-available

#4895 - chore: deprecate Nix-based build, remove interactive components

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

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

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

#4739 - feat: make `instance` attribute check that type is a class

Pull Request - State: closed - Opened by kmill 4 months ago - 2 comments
Labels: breaks-mathlib, toolchain-available, release-ci

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

Pull Request - State: closed - Opened by kmill 4 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 4 months ago
Labels: bug, P-medium

#4708 - chore: reorganise lemmas on list getters

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

#4685 - fix: typo in `run_new_frontend` signature

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

#4626 - feat: consistent elaboration of tactic `have ... by`

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

#4595 - feat: `Simp.Config.implicitDefEqProofs`

Pull Request - State: open - Opened by leodemoura 5 months ago - 1 comment
Labels: breaks-mathlib, toolchain-available, release-ci

#4592 - fix: a recursor application is stuck if the major contains metavariables

Pull Request - State: open - Opened by JovanGerb 5 months ago - 1 comment
Labels: builds-mathlib, toolchain-available

#4557 - feat: @[simp] Nat.add_assoc'

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

#4466 - chore: USE_LAKE: integrate into CMake

Pull Request - State: open - Opened by Kha 5 months ago - 1 comment
Labels: toolchain-available, release-ci

#4460 - feat: async linting

Pull Request - State: open - Opened by Kha 5 months ago - 7 comments
Labels: toolchain-available

#4393 - Moving String theorems from Basic to Lemmas

Pull Request - State: open - Opened by jtristan 5 months ago

#4305 - doc: explain the borrow syntax

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

#4291 - lake progress meter displays as garbage symbols on some windows systems

Issue - State: open - Opened by kim-em 6 months ago - 6 comments
Labels: bug, Lake, new-user-papercuts

#4276 - perf: use `hasExprMvar` in type class search

Pull Request - State: open - Opened by JovanGerb 6 months ago - 2 comments
Labels: breaks-mathlib, toolchain-available

#4272 - perf: cache intermediate type class results and non-results

Pull Request - State: open - Opened by JovanGerb 6 months ago - 1 comment
Labels: breaks-mathlib, toolchain-available

#4271 - feat: fat static libraries with all transitive dependencies

Pull Request - State: open - Opened by bollu 6 months ago - 4 comments
Labels: awaiting-author, toolchain-available

#4253 - chore: minimization of variable-induced slowdown

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

#4223 - chore: decrease priority for `MonadError`

Pull Request - State: open - Opened by JovanGerb 6 months ago - 3 comments
Labels: builds-mathlib, toolchain-available

#4198 - chore: add minimization for 'dsimp at' issue

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

#4182 - RFC: mutual structures

Issue - State: open - Opened by ice1000 6 months ago - 6 comments
Labels: RFC, P-low

#4171 - feat: test for simp problem

Pull Request - State: open - Opened by kim-em 6 months ago - 3 comments
Labels: toolchain-available

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

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

#4146 - FunInd chokes on pattern match with dependent targets

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

#4118 - chore: CI: optimize code under Linux Debug

Pull Request - State: open - Opened by Kha 6 months ago - 2 comments
Labels: toolchain-available

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

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

#3998 - feat: `lake install`

Pull Request - State: open - Opened by tydeu 7 months ago - 3 comments

#3976 - feat: Implement Functor for Array

Pull Request - State: open - Opened by alok 7 months ago - 6 comments
Labels: awaiting-author, toolchain-available

#3973 - feat: use `rfl` proofs of `Iff` in `dsimp`

Pull Request - State: open - Opened by thorimur 7 months ago - 2 comments
Labels: WIP, breaks-mathlib, toolchain-available

#3933 - feat: rm partial / bounds checks in Array.qsort

Pull Request - State: open - Opened by digama0 7 months ago - 11 comments
Labels: WIP, toolchain-available

#3910 - feat: display auto-implicits as inlay hints

Pull Request - State: open - Opened by Kha 7 months ago - 3 comments
Labels: breaks-mathlib, toolchain-available

#3877 - feat: binary recursive implementation of List.mapA

Pull Request - State: open - Opened by digama0 7 months ago - 5 comments
Labels: awaiting-author, builds-mathlib, toolchain-available

#3756 - chore: upstream `Nat.binaryRec`

Pull Request - State: open - Opened by FR-vdash-bot 8 months ago - 11 comments
Labels: awaiting-author, breaks-mathlib, toolchain-available, release-ci

#3727 - feat: BitVec.flatten and basic API

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

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

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

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

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

#3699 - feat: make `registerLabelAttr` consistent with `registerTagAttribute`

Pull Request - State: open - Opened by thorimur 8 months ago - 3 comments
Labels: builds-mathlib, toolchain-available

#3696 - feat: do not propagate pretty printer errors through messages

Pull Request - State: open - Opened by tydeu 8 months ago - 4 comments
Labels: breaks-mathlib, toolchain-available

#3687 - feat: [WIP] Persistent env extension custom types

Pull Request - State: open - Opened by digama0 8 months ago

#3684 - fix: remove special handling of numerals in `DiscrTree`

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

#3641 - feat: `modifyM`/`modifyGetM` for `IO.Ref`

Pull Request - State: open - Opened by tydeu 8 months ago - 4 comments
Labels: builds-mathlib, toolchain-available

#3637 - fix: handle delayed-assigned mvars in `isDefEq` safely

Pull Request - State: open - Opened by thorimur 8 months ago - 3 comments
Labels: breaks-mathlib, toolchain-available

#3568 - feat: `--continue-on-error` to produce .olean file even if elaboration fails

Pull Request - State: open - Opened by digama0 9 months ago - 5 comments
Labels: breaks-mathlib, toolchain-available

#3519 - simp_all? omits unfolded let hypotheses

Issue - State: open - Opened by JLimperg 9 months ago - 3 comments
Labels: bug

#3494 - feat: syntax and delaborator for delayed assignment metavariables

Pull Request - State: open - Opened by kmill 9 months ago - 4 comments
Labels: toolchain-available

#3473 - fix: `isDefEq` handling of delayed-assigned mvars when `withAssignableSyntheticOpaque` is `true`

Pull Request - State: open - Opened by thorimur 9 months ago - 2 comments
Labels: WIP, builds-mathlib, toolchain-available

#3452 - feat: add BitVec.ult/ule_ofNat

Pull Request - State: open - Opened by bollu 9 months ago - 6 comments
Labels: awaiting-review, toolchain-available, P-medium

#3302 - RFC: A single rfl tactic implementation

Issue - State: closed - Opened by nomeata 9 months ago - 9 comments

#3293 - isDefEq fails in presence of unassignable metavariable

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