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

#5721 - feat: add `BitVec.(msb, getMsbD, getLsbD)_(neg, abs)`

Pull Request - State: open - Opened by luisacicolini 29 days ago - 1 comment
Labels: toolchain-available

#5720 - feat: push/pop tactic API

Pull Request - State: open - Opened by kmill 29 days ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5719 - feat: improved `calc` error messages

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

#5718 - feat: add BitVec.sdiv_[zero|one|self] theorems

Pull Request - State: open - Opened by tobiasgrosser 29 days ago - 2 comments
Labels: toolchain-available

#5717 - feat: simp local confluence testing

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

#5716 - fix: List.drop_drop addition order

Pull Request - State: open - Opened by kim-em 29 days ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5715 - feat: change `lake new math` to use `autoImplicit false`

Pull Request - State: open - Opened by eric-wieser 29 days ago - 3 comments
Labels: toolchain-available

#5714 - feat: bv_decide inequality regression tests

Pull Request - State: open - Opened by alexkeizer 30 days ago - 6 comments
Labels: toolchain-available

#5713 - `show_term` and `by?` change order of elaboration

Issue - State: open - Opened by kmill 30 days ago
Labels: bug

#5712 - feat: add BitVec.[udiv|umod]_[zero|one|self] theorems

Pull Request - State: closed - Opened by tobiasgrosser 30 days ago - 1 comment
Labels: toolchain-available

#5711 - feat: options `pp.mvars.anonymous` and `pp.mvars.levels`

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

#5710 - fix: the `⋯` elaboration warning did not mention `pp.maxSteps`

Pull Request - State: closed - Opened by kmill 30 days ago - 1 comment
Labels: toolchain-available

#5709 - chore: allow LSP client to omit capabilities parameters

Pull Request - State: open - Opened by haruleekim 30 days ago - 1 comment
Labels: toolchain-available

#5708 - fix: ac_nf0: don't tempt the kernel to reduce atoms

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

#5707 - feat: denote deprecations in completion items

Pull Request - State: closed - Opened by mhuisi 30 days ago - 1 comment
Labels: toolchain-available

#5706 - chore: mark prefix_append_right_inj as simp lemma

Pull Request - State: closed - Opened by jcommelin 30 days ago - 1 comment
Labels: toolchain-available

#5705 - chore: better default value for Array.swapAt!

Pull Request - State: closed - Opened by kim-em 30 days ago - 1 comment
Labels: toolchain-available, merge-ci

#5704 - chore: remove @[simp] from Option.isSome_eq_isSome

Pull Request - State: closed - Opened by kim-em 30 days ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5703 - chore: upstream List.sum, planning to later deprecate Nat.sum

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

#5702 - Application type mismatch in simp involving dsimp theorem

Issue - State: open - Opened by JLimperg about 1 month ago
Labels: bug

#5701 - chore: rename `List.join` to `List.flatten`

Pull Request - State: closed - Opened by kim-em about 1 month ago - 1 comment
Labels: toolchain-available, changes-stage0, merge-ci

#5700 - Unable to figure the term when destructing an inductive proposition

Issue - State: closed - Opened by fduxiao about 1 month ago - 2 comments

#5699 - kernel hangs on ac_nf expression

Issue - State: open - Opened by tobiasgrosser about 1 month ago - 4 comments
Labels: bug

#5698 - chore: performance bug in bv_decide

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

#5697 - chore: upstream List.foldxM_map

Pull Request - State: open - Opened by kim-em about 1 month ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5696 - feat: upstream List.mapIdx, and add lemmas

Pull Request - State: closed - Opened by kim-em about 1 month ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5694 - chore: remove instBEqNat, which is redundant with instBEqOfDecidableEq but not defeq

Pull Request - State: open - Opened by kim-em about 1 month ago - 4 comments
Labels: builds-mathlib, toolchain-available

#5693 - chore: import orphaned Lean.Replay

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

#5692 - feat: let dot notation see through `CoeFun` instances

Pull Request - State: closed - Opened by kmill about 1 month ago - 3 comments
Labels: builds-mathlib, toolchain-available

#5691 - feat: add `BitVec.(getMSbD, msb)_(add, sub, neg)` and `BitVec.getLsbD_(sub, neg)`

Pull Request - State: open - Opened by luisacicolini about 1 month ago - 1 comment
Labels: toolchain-available

#5690 - Recursive theorems with `cases` vs `match`

Issue - State: open - Opened by hargoniX about 1 month ago - 2 comments
Labels: bug

#5689 - fix: when pretty printing constant names, do not use aliases from "non-API `export`s"

Pull Request - State: open - Opened by kmill about 1 month ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5688 - fix: have `Lake` not create core aliases into `Lake` namespace

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

#5687 - chore: deprecation for Array.data

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

#5686 - feat: DiscrTree: index the domain of `∀`

Pull Request - State: open - Opened by nomeata about 1 month ago - 1 comment
Labels: builds-mathlib, toolchain-available, changes-stage0

#5685 - fix: help message flags, removes -f flag and adds -g flag

Pull Request - State: closed - Opened by James-Oswald about 1 month ago - 1 comment
Labels: toolchain-available

#5684 - feat: update toolchain on `lake update`

Pull Request - State: open - Opened by tydeu about 1 month ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5683 - Slow elaboration of `List Nat` literals

Issue - State: open - Opened by kmill about 1 month ago - 3 comments
Labels: bug

#5682 - "-f" flag not recognized as alternative to "--features"

Issue - State: closed - Opened by James-Oswald about 1 month ago - 1 comment
Labels: bug

#5681 - refactor: remove mkRecursorInfoForKernelRec

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

#5680 - feat: expand relationship with BitVec and toFin

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

#5679 - fix: RecursorVal.getInduct to return name of major argument’s type

Pull Request - State: open - Opened by nomeata about 1 month ago - 6 comments
Labels: builds-mathlib, toolchain-available

#5678 - fix: make IO-bound tasks dedicated

Pull Request - State: closed - Opened by mhuisi about 1 month ago - 1 comment
Labels: toolchain-available

#5677 - fix: some goal state issues

Pull Request - State: open - Opened by mhuisi about 1 month ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5676 - feat: make bv_decide error when the LRAT proof is invalid

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

#5675 - fix: context tracking in bv_decide counter example

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

#5673 - chore: disable ac_nf by default

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

#5671 - fix: make `@[elab_as_elim]` require at least one discriminant

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

#5670 - feat: ~~~(-x) bv_decide

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

#5669 - refactor: construc `.eq_def` before `.eq_n`

Pull Request - State: open - Opened by nomeata about 1 month ago - 1 comment
Labels: breaks-mathlib, toolchain-available

#5668 - `<|>` notation is not pretty-printed

Issue - State: open - Opened by TwoFX about 1 month ago
Labels: bug

#5667 - "failed to generate equational theorem" when matching on not only recursive call

Issue - State: open - Opened by nomeata about 1 month ago - 5 comments
Labels: bug

#5666 - feat: whitespace tactic completion & tactic completion docs

Pull Request - State: closed - Opened by mhuisi about 1 month ago - 1 comment
Labels: toolchain-available

#5665 - feat: `decide!` tactic for using kernel reduction

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

#5663 - feat: support `let rec` in `#eval`

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

#5662 - chore: add example where omega never terminates / runs out of heartbeats

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

#5661 - Structure eta doesn't work for nested inductives

Issue - State: open - Opened by nomeata about 1 month ago - 12 comments
Labels: bug

#5660 - Meta.check does not check projections

Issue - State: open - Opened by nomeata about 1 month ago
Labels: bug

#5659 - `rintro` error message is in the wrong place

Issue - State: open - Opened by TwoFX about 1 month ago - 1 comment
Labels: bug

#5658 - fix: store local context for 'don't know how to synthesize implicit argument' errors

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

#5657 - feat: Strict Ackermannization tactic (bv_ac_eager) for QF_UFBV

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

#5656 - test: add two benchmarks that are slow to parse or elaborate

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

#5648 - fix: have `simpa ... using ...` do `exact`-like checks

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

#5646 - feat: lemmas about BitVector arithmetic inequalities

Pull Request - State: closed - Opened by bollu about 1 month ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5642 - refactor: lake: restrict cache fetch to leanprover*

Pull Request - State: closed - Opened by tydeu about 1 month ago - 2 comments
Labels: builds-mathlib, toolchain-available, will-merge-soon, backport releases/v4.13.0

#5641 - fix: lake: make package `extraDep` intransitive

Pull Request - State: closed - Opened by tydeu about 1 month ago - 2 comments
Labels: builds-mathlib, toolchain-available, will-merge-soon, backport releases/v4.13.0

#5629 - RFC: decide! tactic variant

Issue - State: closed - Opened by nomeata about 1 month ago - 6 comments
Labels: RFC

#5623 - chore: move BitVec.udiv/umod/sdiv/smod after add/sub/mul/lt

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

#5622 - chore: add LNSym omega benchmarks with large problems that take multiple seconds to solve

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

#5604 - feat: complete `BitVec.[getMsbD|getLsbD|msb]` for shifts

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

#5566 - fix: use `MessageData.tagged` to mark maxHeartbeat exceptions

Pull Request - State: closed - Opened by eric-wieser about 1 month ago - 2 comments
Labels: builds-mathlib, toolchain-available

#5565 - Exception.isMaxHeartbeat no longer works

Issue - State: closed - Opened by eric-wieser about 1 month ago
Labels: bug

#5546 - doc: update README w/ Reservoir package options

Pull Request - State: open - Opened by tydeu about 1 month ago
Labels: backport releases/v4.12.0

#5545 - RFC: Make `Range` behavior "more correct"

Issue - State: open - Opened by TomasPuverle about 1 month ago
Labels: RFC

#5544 - bv_check builds a proof with an incorrect application of Lean.ofReduceBool

Issue - State: open - Opened by bollu about 1 month ago
Labels: bug

#5542 - chore: deprecate `:=` variants of `inductive` and `structure`

Pull Request - State: closed - Opened by kmill about 1 month ago - 3 comments
Labels: breaks-mathlib, toolchain-available

#5541 - fix: rm new shared libs before build for Windows

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

#5540 - Slow elaboration of simple equation with overloaded operator

Issue - State: open - Opened by nomeata about 1 month ago
Labels: bug

#5539 - chore: fix explicitness of Option.mem_toList

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

#5538 - doc: backticks around Lean code in docstrings

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

#5537 - chore: adjust DecidableRel instance for leOfOrd

Pull Request - State: open - Opened by kim-em about 1 month ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5536 - chore: fix Array.modify lemmas

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

#5535 - chore: rename Array.flatten to join, and upstream lemmas

Pull Request - State: open - Opened by kim-em about 1 month ago - 2 comments

#5534 - chore: cleanup of Array GetElem lemmas

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

#5533 - chore: deprecate variants other than `inductive ... where`

Pull Request - State: open - Opened by kmill about 1 month ago - 6 comments
Labels: breaks-mathlib, toolchain-available

#5532 - feat: Option.attach

Pull Request - State: closed - Opened by kim-em about 1 month ago - 1 comment
Labels: breaks-mathlib, toolchain-available

#5531 - fix: default values for structure fields can be noncomputable

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

#5530 - fix: automatic instance names about types with hygienic names should be hygienic

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

#5529 - chore: move `@[simp]` from `exists_prop'` to `exists_prop`

Pull Request - State: open - Opened by kmill about 1 month ago - 1 comment
Labels: breaks-mathlib, toolchain-available

#5528 - feat: allow explicit mode with field notation

Pull Request - State: closed - Opened by kmill about 1 month ago - 3 comments
Labels: builds-mathlib, toolchain-available

#5527 - chore: reduce use of deprecated lemmas in Array

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

#5526 - chore: fix name of Array.length_toList

Pull Request - State: closed - Opened by kim-em about 1 month ago - 1 comment
Labels: builds-mathlib, toolchain-available

#5524 - feat: add ac_nf and test [ac_nf|ac_rfl] for BitVec

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

#5522 - chore: more monadic simp lemmas

Pull Request - State: closed - Opened by kim-em about 1 month ago - 1 comment
Labels: WIP, builds-mathlib, toolchain-available

#5513 - fix: use breakable instead of unbreakable whitespace when formatting tokens

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