Zulip Chat Archive

Stream: new members

Topic: API Documentation


Jeremy Salwen (Dec 08 2022 at 01:01):

Hello all, I am new to lean, just going through the basics of lean4. Is there a facility for searching for functions by type signature (like the Coq "Search" command)? Also, is there official API documentation so I could look up things like how to parse a string to an integer?

Notification Bot (Dec 08 2022 at 01:02):

A message was moved here from #new members > Permission for github by Jeremy Salwen.

Eric Wieser (Dec 08 2022 at 01:10):

Maybe library_search?

Jeremy Salwen (Dec 08 2022 at 01:16):

Correct me if I'm wrong, but that looks like a tactic, not just a user facing search. Like I would want to find a list of functions matching a partial type signature, and then looking them up one by one to check whether they do what I want.

Matt Diamond (Dec 08 2022 at 01:19):

I know what you mean, like Hoogle with Haskell... not sure Lean4 has anything like that (though I don't have that much experience with Lean4)

Matt Diamond (Dec 08 2022 at 01:20):

have you browsed the API docs at https://leanprover-community.github.io/mathlib4_docs/?

Jeremy Salwen (Dec 08 2022 at 01:25):

I have not! Thank you for sharing the link (and thanks Eric for the link to the docs too!)

Moritz Doll (Dec 08 2022 at 01:35):

Hoogle for Lean 4 (Loogle?) has been discussed a few times and I think it only a question of time until someone comes around and does that.

Mario Carneiro (Dec 08 2022 at 01:37):

There is the #find command, which is intended to mimic the coq Search command

Mario Carneiro (Dec 08 2022 at 01:37):

but also, don't let the tactic-like status of library_search fool you. It is actually used for searching, you just make a lemma statement on the spot and try to prove it by library_search

Mario Carneiro (Dec 08 2022 at 01:38):

I think there is also a #library_search command that makes this easier

Jeremy Salwen (Dec 08 2022 at 01:46):

Thank you, #find was what I am looking for!

Jeremy Salwen (Dec 08 2022 at 02:21):

I may be confused, but #find doesn't seem to be working the same way as #eval or #check. Is there some other way I am supposed to invoke it?


Last updated: Dec 20 2023 at 11:08 UTC