inline loogle?

Stream: Is there code for X?

[JJ]

I would like to be able to write out a type with some named type holes, Loogle-style, and get a list of available functions matching the type pattern. Is there any sort of thing for this?

I know there is #find from Mathlib, but this isn't in the standard library (and it doesn't actually work for me when I'm using Mathlib, either -- this is operator error though I think. haven't gotten it to not time out.) I basically want #find for the stdlib.

[Kim Morrison]

exact?

[JJ]

I do not think so? If it is exact?, I am having trouble using it.

[JJ]

I don't want this for tactics or mathematics or anything, I want it so I can find functions on types when I'm using Lean for normal programming things.

[Joachim Breitner]

In theory it's possible to run loogle locally like this:
https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/How.20to.20use.20the.20.23find.20tactic.20from.20Loogle.20in.20a.20custom.20project.3F/near/533041839

The necessary plumbing isn't user friendly yet

[Anand Rao Tadipatri]

You could try adding LeanSearchClient to your repository, which features a #loogle command.

[JJ]

For posterity, I found somebody's notes about this topic: https://lakesare.brick.do/how-to-search-for-theorems-in-lean-4-WXebAQkXVmx1

[JJ]

You could try adding LeanSearchClient to your repository, which features a #loogle command.

I am very happy with this. Thank you! It is a bit slow and doesn't tell me information about the results themselves but is otherwise excellent to use.

[JJ]

I'm even happier with the Lean 4: Loogle VS Code action. I think ideally what I would want would be #loogle from LeanSearchClient but local / speedy, but all of these options also work great.

[JJ]

I hit limitations around this again. I've now learned how to use exact?, though! It's very useful to type example : <signature> := by exact?.

(note to self: do look into running Loogle locally in the future)