Unicode symbols in Loogle

Stream: general

[Jeremy Kahn]

One thing I've noticed using loogle is that I often want to search for expressions using special characters, as in _ \in _ or _ \le _ or _\inv. Is there any mechanism for including such characters in loogle? Failing that, is there an easy way to look up the actual (ASCII) function for a special character?

[Kevin Buzzard]

I just write stuff in VS Code and then copy-paste.

[Joachim Breitner]

Or live.lean-lang.org if you don't have a browser.
I doubt it's easy to add that functionality to the Loogle webpage. One argument in favor of vscode-integrated Loogle search, so you might try that extension!

[Yaël Dillies]

You might want to try https://github.com/arthurpaulino/chrome-lean-unicode

[Jeremy Kahn]

Yes, @Kevin Buzzard 's suggestion is pure genius! I don't know why I didn't think of that. Maybe it's a matter of learning to look for workarounds. :laughing:

[Joachim Breitner]

Oh, nice. @Arthur Paulino , do you think you could make a variant of that that websites could embed and enable for specific text input fields?

[Ruben Van de Velde]

Also you can spell out Inv.inv, for example

[Jeremy Kahn]

Is there a nice way to look up the official name for a function from its unicode infix or suffix?

[Jeremy Kahn]

@Yaël Dillies @Arthur Paulino I installed the extension, and now I can get ∈ and α in the Zulip chat. I added "https://loogle.lean-lang.org" to the list of covered websites, and the icon appears as green, but it doesn't seem to work in the loogle entry field.

[Joachim Breitner]

Would it be useful if the lean elaborator simply understood \in just like corresponding symbol, so that ASCII input works? Would require the parser or elaborator to know the list of abbreviations, and is a bit of a layering violation, but would be useful in a few places (e.g. on the command line). (Not sure, just thinking out loudly)

[Joachim Breitner]

Maybe the extension only works in text areas, not input fields?

[Mario Carneiro]

the leader key isn't always \

[Mario Carneiro]

plus, that would cause problems for string escapes like \n (which I always have to convince the extension to not replace with ¬)

[Mario Carneiro]

Jeremy Kahn said:

Is there a nice way to look up the official name for a function from its unicode infix or suffix?

If you just type #check x \in y or similar in the editor you can ctrl-click on the symbol to go to the definition

[Mario Carneiro]

ditto if you see it in existing code in either docgen or mathlib

[Shreyas Srinivas]

I tried adding that feature in the extension. But it is painful to get it right

[Shreyas Srinivas]

On the positive side, I do the copy paste thing easily because I am already in vscode

[Shreyas Srinivas]

If someone's willing to contribute this feature, PRs to the loogle extension repo are welcome

[Arthur Paulino]

Sorry, I don't have the time to debug :sad:

[Jeremy Kahn]

@Joachim Breitner I do think it would be helpful for loogle to understand escape sequences in the input field. But not really necessary given the cut-and-paste option and other workarounds (including the loogle bot in Zulip).

[Joachim Breitner]

I fully agree! I think the best course of action is if someone can generalize https://github.com/arthurpaulino/chrome-lean-unicode to a library that a website can embed, then loogle can use it.