batteries

batteries copied to clipboard

These lemmas are separate from the rest and need not be pulled in by the main file.

digama0

- [x] Depends on: #735 - [x] Depends on: #737 - [x] Depends on: #738 This adds RBMap lemmas corresponding to all of the RBSet lemmas.

digama0

feat: fill in proof of Array.erase_data

17

I also added some lemmas in List.Lemmas that were necessary. I'm not sure about the naming of some of the lemmas I added, so I would appreciate feedback!

Seppel3210

feat: `List.forall_get_iff_forall_mem `

3

```Lean4 theorem forall_mem_iff_forall_index [DecidableEq α] {p : α → Prop} {l : List α} : (∀ x ∈ l, p x) ↔ (∀ i : Fin (l.length), p (l.get i))...

Qiu233

feat: apply dupNamespace linter to instances

4

This caught 14 bugs with no false positives over in https://github.com/leanprover-community/mathlib4/pull/10899

Ruben-VandeVelde

feat: `List.insertP` and lemmas

1

`List.insertP` is a generalized, tail-recursive version of the insert step in insertion-sort. Sample use: ```lean def insertionSort [LT α] [DecidableRel (α:=α) (· < ·)] (l : List α) := l.foldl...

fgdorais

Pattern-based unfolding tactic

7

This is a tactic that allows targeted unfolding of expressions in the proof state by specifying patterns and occurrences (an idea that is due to Yaël Dillies). The file `Utils.lean`...

0art0

feat: DiscrTree

27

I've made a new version of Lean's `DiscrTree` called `RefinedDiscrTree` with a lot of new features. It is able to index lambda's, forall's, and their bound variables. It also gives...

JovanGerb

chore: make RBNode.mem_insert more robust

6

This proof has three different hypotheses named `h`, and in a upcoming version of leanprover/lean4#2793 something is going to change in how they shadow each other. This is a fix...

kim-em

chore: upstream @[eqns]

1

kim-em