leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover
Apache License 2.0
232 stars 95 forks source link

feat: some array lemma aliases #891

Closed fgdorais closed 1 month ago

fgdorais commented 1 month ago

Core uses nil instead of empty for some array lemmas and I keep getting caught by that, so I'm proposing to add aliases for the empty variants. I'm also proposing to add mem_singleton since that one comes up often enough that I'd like to avoid going through list every time.

semorrison commented 1 month ago

I will try to fix these in Lean in not too long!