constructive library_search?

Stream: new members

[Jason Orendorff]

I have a silly problem. library_search sometimes finds stuff like classical.not_imp.mpr, when I'd rather have the constructive proof.

I shouldn't care about this, but is there an easy way to avoid classical?

[Jalex Stark]

tauto might be enough

[Reid Barton]

Since almost nothing is constructively provable, you might as well just learn all the lemmas :upside_down:

[Johan Commelin]

That doesn't teach you the library lemma names...

[Johan Commelin]

Maybe suggest will give a constructive proof at suggestion 17...

[Jalex Stark]

also you could start by writing your own proof of whatever constructive lemma you were looking for

[Jason Orendorff]

i shall redouble my efforts to not care :)