Zulip Chat Archive
Stream: new members
Topic: noob question: vscode and LEAN_PATH
Vincent Siles (Oct 07 2019 at 11:23):
Hi ! I'm trying lean for the first time and I'm a bit lost in the std. So I'd like to use #find which requires a import tactic.find if I am correct.
I'm using vscode and I set up the lean path in vscode settings. I can confirm this works. But the import raises file 'tactic/find' not found in the LEAN_PATH. I'm not sure where to set this path, and to which destination.
Anne Baanen (Oct 07 2019 at 11:27):
The find tactic is part of mathlib, did you also set up that?
Johan Commelin (Oct 07 2019 at 11:29):
For the record: you might also be interested in library_search. It is complementary to #find.
Vincent Siles (Oct 07 2019 at 11:29):
No, I did not. I was just trying to search for some definitions/lemmas in general (like the SearchAbout or SearchPattern in Coq).
Johan Commelin (Oct 07 2019 at 11:29):
Aah, you'll need mathlib for both of them
Johan Commelin (Oct 07 2019 at 11:30):
It's a bit unfortunate... but you need mathlib for almost anything beyond the bare minimum
Vincent Siles (Oct 07 2019 at 11:30):
ok I'll look into how to install mathlib then. Thank you
Johan Commelin (Oct 07 2019 at 11:30):
And nowadays it's not so hard to set up, with pre-compiled binaries etc
Johan Commelin (Oct 07 2019 at 11:31):
There are good instructions on Github
Vincent Siles (Oct 07 2019 at 11:44):
#find and library_search seem to only search for lemmas. Can I use them to search for definitions too or is there another way ?
Johan Commelin (Oct 07 2019 at 11:48):
I think library_search will also find defs
Rob Lewis (Oct 07 2019 at 11:50):
There's no good reason to restrict #find to theorems, is there? It's a trivial change to let it match defs too.
Vincent Siles (Oct 07 2019 at 11:52):
#find bool -> _ -> _ doesn't show the and or or function. Maybe I'm not using it correctly
Rob Lewis (Oct 07 2019 at 11:54):
No, you're right, it doesn't do that right now. It only looks for theorems. But I don't know why it's implemented with that restriction.
Rob Lewis (Oct 07 2019 at 12:12):
https://github.com/leanprover-community/mathlib/pull/1512
Scott Morrison (Oct 08 2019 at 00:49):
library_search will find defs, but often it's not useful, but it finds "the boring ones" rather than the ones you want. A student here @Lucas Allen has some work he'll PR soon that shows a list of applicable lemmas/defs. I think he's busy with non-Lean stuff right now.
Vincent Siles (Oct 08 2019 at 06:57):
good to know, thank you
Last updated: Dec 20 2023 at 11:08 UTC