How to search for function with all-Unicode name?

Stream: new members

[mars0i]

I recently learned about ▸ from Kyle Miller's helpful answer in another thread. I can easily find pull up the documentation for this function in my editor--which is great--but I I can't figure out how to search for it in the API documentation, Loogle, or Moogle. Is there some trick to searching for Unicode-only names in the documentation? Sometimes it's helpful to see what module a function comes from in order to find out how general it is, to find out what other names it might have, or to see what related definitions there are in the same module.

[Daniel Weber]

▸ is a bit of a special case, I'm also not sure where it's defined, but usually when there's notation you can control-click on it to see where it's defined

[Daniel Weber]

It's defined in https://github.com/leanprover/lean4/blob/d3f7ed434b1e9f6f2496f5208d1abd3bf3163013/src/Lean/Elab/BuiltinNotation.lean#L390 --- you can see it's builtin notation, so it's a special case (to find it I searched for ▸ in the lean4 repo)

[mars0i]

Thanks @Daniel Weber. The fact that it's a special case is encouraging. I gather that @[builtin_term_elab subst] is what indicates that it's a builtin. I can check the source when a symbol doesn't show up in a search.

[Luigi Massacci]

I think it’s indeed a problem of the special casing

[Luigi Massacci]

@loogle "▸"

[loogle]

:shrug: nothing found

[Luigi Massacci]

@loogle "∀ᶠ"

[loogle]

:search: Filter.«term∀ᶠ_In_,_», Filter.«term∀ᶠ_In_,_».delab

[Luigi Massacci]

and I can’t imagine what else could be the difference

[Luigi Massacci]

(more generally though, if you know how to type it in lean, know that loogle accepts that as well, i.e. \t, \forallf, etc)

[Luigi Massacci]

But maybe @Joachim Breitner can chip in, I think loogle is his creation

[Joachim Breitner]

This is an elaborator, not definition, so loogle won’t help you here.

Ah, but you are searching for the name containing "▸". Unfortunately, that’s called
@loogle "elabSubst"
and doesn’t have the unicode symbol in the name.

[loogle]

:search: Lean.Elab.Term.elabSubst

[mars0i]

Maybe for now a good method is "Try Loogle or the API doc search, and if it's not there, try grepping the source, and then come back to Loogle or the API search when you find a name that might be what you want. It's not ideal, but it's OK, and it's better than nothing, and there are languages where the situation is worse.

[Kyle Miller]

When I see notation, my usual method is (1) try go-to-declaration on the notation, otherwise (2) try grepping for "▸ or " ▸, since that usually gives the syntax definition.

[mars0i]

Re (1), sometimes I want more context than the in-editor documentation provides. I want to see what module it comes from, what related definitions there are, etc.

I think Lean's documentation system is very good. I won't name other languages that don't provide decent documentation.

[Kyle Miller]

Go-to-declaration and go-to-definition usually goes to the module(s) it comes from. For some reason this subst notation goes to Eq instead though (which makes some sense as subst is fancy notation to create an Eq.rec term, but I don't think that's helpful in this case).

[mars0i]

I didn't know about go-to-declaration and go-to-definition. I see now that lean.nvim lets me use them in an Infoview window, but not in a source window. Not sure whether VSCode is analogous. (I gather that there are VSCode features not yet present in lean.nvim.)

[Julian Berman]

Go to declaration definitely works in neovim as well. Check that you've bound vim.lsp.buf.definition(), which unless you're on 0.11 is not yet bound by default.

[mars0i]

Thanks @Julian Berman. That worked. Great.