API Documentation

Stream: new members

[Jeremy Salwen]

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]

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

[Eric Wieser]

Maybe library_search?

[Jeremy Salwen]

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]

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]

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

[Jeremy Salwen]

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

[Moritz Doll]

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]

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

[Mario Carneiro]

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]

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

[Jeremy Salwen]

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

[Jeremy Salwen]

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?