Zulip Chat Archive

Stream: new members

Topic: constructive library_search?


Jason Orendorff (Jun 16 2020 at 19:31):

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 (Jun 16 2020 at 19:47):

tauto might be enough

Reid Barton (Jun 16 2020 at 19:48):

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

Johan Commelin (Jun 16 2020 at 19:48):

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

Johan Commelin (Jun 16 2020 at 19:49):

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

Jalex Stark (Jun 16 2020 at 19:50):

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

Jason Orendorff (Jun 16 2020 at 21:14):

i shall redouble my efforts to not care :)


Last updated: Dec 20 2023 at 11:08 UTC