batteries

batteries copied to clipboard

feat: make the unreachable tactic linter complain if tactics are called with no goals remaining

3

alexjbest

feat: add function for refl and apply

2

mcdoll

feat: well founded stream class

2

Based on discussions on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/Porting.20just.20functionality/near/354657447). Still needs more love to make it polished.

digama0

chore: adaptations for leanprover/lean4#3756

1

astrainfinita

feat: unbundle array size constraint from hash map bucket array

3

This PR makes sure that the positivity checker is happy with the following construction: ```lean inductive ContainsItselfInHashMapValues where | base | recursive (l : HashMap.Imp Bool ContainsItselfInHashMapValues) ``` Users actually...

TwoFX

```lean import Std.Tactic.Where open scoped Nat #where -- In root namespace with initial scope ``` Duplicate of https://github.com/leanprover-community/mathlib4/issues/12606 because I didn't realize `#where` is defined here.

fpvandoorn

feat: `Array.qsort_sorted`

4

This was a surprisingly challenging proof. It really highlights some of the pain involved in verifying programs which perform many array modifications without something isomorphic to separation logic, because one...

digama0

- [x] Depends on: #735 - [x] Depends on: #737 - [x] Depends on: #738 - [x] Depends on: #739 - [x] Depends on: #740 Continuation of the RBMap series....

digama0

Complement to #762. Adds List version of all the definitions in `Data.Array.Merge`. Also adds `List.mergeSort` (upstreamed from mathlib), as a replacement for `Array.qsort` on lists (because `qsort` cannot easily be...

digama0

feat: add lemma code-action

17

The 'lemma' command elaborates as 'theorem' but gives warning + codeaction to use 'theorem' instead. I am picking up @jcommelin's PR #413, but I did not know how to modify...

adomani