35 Pull requests merged by 9 people

• chore: move to v4.13.0-rc3

  #981 merged Oct 5, 2024

• fix: use user's Lean search path in linter

  #980 merged Oct 4, 2024

• chore: move to v4.13.0-rc1

  #979 merged Oct 3, 2024

• chore: adaptations for nightly-2024-10-03

  #978 merged Oct 3, 2024

• chore: adaptations for nightly-2024-10-01

  #976 merged Oct 3, 2024

• fix: argument order and make abbrev

  #975 merged Oct 3, 2024

• chore: only test Mathlib on PRs to main

  #977 merged Oct 3, 2024

• chore: cleanup some unused arguments

  #974 merged Oct 3, 2024

• chore: adaptations for nightly-2024-09-27

  #971 merged Oct 2, 2024

• chore: update toolchain to v4.12.0

  #973 merged Oct 1, 2024

• fix: disable flaky test

  #970 merged Sep 28, 2024

• feat: decidable quantifiers for Vector

  #953 merged Sep 28, 2024

• feat: getElem_tail lemmas

  #905 merged Sep 28, 2024

• chore: use implicit arguments in iff lemmas

  #957 merged Sep 28, 2024

• chore: simplify lakefile

  #950 merged Sep 28, 2024

• fix: remove List.erase_of_forall_bne and replace with List.erase_eq_self_iff_forall_bne

  #967 merged Sep 28, 2024

• chore: add lake-manifest.json when updating batteries-pr-testing branches

  #965 merged Sep 27, 2024

• chore: fix test_mathlib.yml (5)

  #964 merged Sep 27, 2024

• chore: fix test_mathlib.yml (4)

  #963 merged Sep 27, 2024

• chore: fix test_mathlib.yml (3)

  #962 merged Sep 27, 2024

• chore: fix test_mathlib.yml again

  #961 merged Sep 27, 2024

• chore: fix test_mathlib.yml

  #959 merged Sep 27, 2024

• feat: automatically test Mathlib against Batteries PRs

  #958 merged Sep 27, 2024

• feat: fill in proof of Array.data_erase

  #690 merged Sep 26, 2024

• feat: compare List.ofFn and Array.ofFn

  #956 merged Sep 26, 2024

• refactor: avoid relying on rfl's behavior on ground terms

  #832 merged Sep 25, 2024

• fix: add trailing line-break in nolints.json

  #955 merged Sep 25, 2024

• chore: cleanup a breaking non-terminal simp on HashMap

  #954 merged Sep 24, 2024

• chore: fix more Std -> Batteries

  #887 merged Sep 24, 2024

• feat: lemmas about Vector

  #952 merged Sep 23, 2024

• chore: deprecate HashSet.insert'

  #949 merged Sep 18, 2024

• chore: adaptations for nightly-2024-09-12

  #947 merged Sep 16, 2024

• chore: adaptations for nightly-2024-09-10

  #946 merged Sep 12, 2024

• chore: adaptations for nightly-2024-09-05

  #944 merged Sep 10, 2024

• chore: remove >6 month deprecations

  #945 merged Sep 10, 2024

8 Pull requests opened by 5 people

• feat: add `#check_note` command

  #948 opened Sep 14, 2024

• chore: adapt to lean #5346

  #951 opened Sep 21, 2024

• feat: add `#print opaques` command

  #966 opened Sep 27, 2024

• fix: use `by rfl` instead of `rfl` to bypass new compiler bug

  #968 opened Sep 27, 2024

• feat: add `#help` commands

  #969 opened Sep 28, 2024

• feat: `l <+~ [] ↔ l = []`

  #972 opened Sep 30, 2024

• chore: add missing simp for array size lemmas

  #982 opened Oct 5, 2024

• chore: move panicWith out of UnionFind

  #983 opened Oct 5, 2024

15 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

• feat: the trailingWhitespace linter

  #920 commented on Oct 9, 2024 • 2 new comments

• feat: Sum.left, Sum.right

  #105 commented on Sep 22, 2024 • 0 new comments

• chore: make RBNode.mem_insert more robust

  #342 commented on Sep 22, 2024 • 0 new comments

• feat: add `String.splitOn_of_valid`

  #743 commented on Sep 10, 2024 • 0 new comments

• feat: unbundle array size constraint from hash map bucket array

  #748 commented on Sep 30, 2024 • 0 new comments

• refactor: move theorems about lists from mathlib

  #756 commented on Oct 8, 2024 • 0 new comments

• chore: adaptations for leanprover/lean4#3756

  #765 commented on Sep 30, 2024 • 0 new comments

• chore: upstream `Nat.binaryRec`

  #799 commented on Oct 1, 2024 • 0 new comments

• feat: Add `String.isPrefixOf` theorems

  #809 commented on Oct 5, 2024 • 0 new comments

• feat: dependent array type

  #813 commented on Oct 1, 2024 • 0 new comments

• feat: `Fin.foldlM` and `Fin.foldrM`

  #814 commented on Oct 3, 2024 • 0 new comments

• feat: folds for dependent arrays

  #815 commented on Oct 1, 2024 • 0 new comments

• refactor: implement `BinaryHeap` using `Vector`

  #850 commented on Oct 1, 2024 • 0 new comments

• feat: order lemmas for `UIntX` types

  #854 commented on Sep 27, 2024 • 0 new comments

• feat: add bisection algorithm

  #890 commented on Sep 29, 2024 • 0 new comments