batteries

batteries copied to clipboard

The attribute elaborator checks whether `move` is a string literal, which it is not.

gebner

I always wanted to do this in core. Doing it in std4 first could be a good case study.

Kha

`mathlib` `RBTree` and `RBMap` won't be ported to `mathlib4` but some of the theorems there should eventually be covered in `Std`. In particular: https://github.com/leanprover-community/mathlib/blob/master/src/data/rbtree/basic.lean https://github.com/leanprover-community/mathlib/blob/master/src/data/rbtree/find.lean https://github.com/leanprover-community/mathlib/blob/master/src/data/rbtree/min_max.lean https://github.com/leanprover-community/mathlib/blob/master/src/data/rbmap/default.lean

arienmalec

We should port the content of [Lean.Data.PersistentHashMap](https://github.com/leanprover/lean4/blob/master/src/Lean/Data/PersistentHashMap.lean) to std4 with similar functionality, and additional lemmas.

mpenciak

We should port the content of [Lean.Data.HashSet](https://github.com/leanprover/lean4/blob/master/src/Lean/Data/HashSet.lean) to std4 with similar functionality, and additional lemmas.

mpenciak

Doing this on thousands of files would be very slow: ```lean def copyFile (src : FilePath) (dst : FilePath) : IO Unit := do IO.FS.writeFile dst (← IO.FS.readFile src) ```...

lovettchris

feat: getElem_tail lemmas

1

I felt like these were missing, I tried adhering to the existing standards, but happy to patch things up if I missed something:)

pimotte

feat: detect default target on runLinter

6

Now `runLinter` will try to detect all root modules of the default build targets of type `lean_exe` or `lean_lib` in Lake's environment using the same `resolveDefaultPackageTarget` function as `lake build`....

austinletson

kim-em

refactor: make `List.length_eq_countP_add_countP` avoid Prop

4

Changes this lemma to use boolean not rather than propositional not.

BoltonBailey