batteries icon indicating copy to clipboard operation
batteries copied to clipboard
verified publisher icon leanprover-community

feat: some lemmas about variations List.get and List.getLast, fix duplicate lemma

Open javra opened this issue 2 years ago • 2 comments

javra avatar Sep 28 '23 20:09 javra

While appreciating that the Std PR queue is slow, it's helpful if PRs are labelled when they are ready for review. Contributors can write a comment containing just awaiting-review or awaiting-author or WIP in order to switch between these labels.

kim-em avatar Oct 26 '23 02:10 kim-em

awaiting-review

kim-em avatar Oct 26 '23 02:10 kim-em

These changes are now all in Lean core.

fgdorais avatar Jul 23 '24 10:07 fgdorais