search

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

chore: remove `proof_wanted` in HashMap.Lemmas #874

Closed TwoFX closed 2 months ago

TwoFX commented 2 months ago

It would probably not be a good use of anyone's time to work on that sorry right now, and there was some confusion on Zulip today, so I suggest removing the proof_wanted.

TwoFX commented 2 months ago

awaiting-review

digama0 commented 2 months ago

how about commenting it out and put a note saying why it's not wanted?

TwoFX commented 2 months ago

@digama0 Done.

semorrison commented 2 months ago

Reading this without the request from Mario I would of course ask "what is the point of keeping the comment"?

But it's better than leaving it as is!