loogle miss

Stream: mathlib4

[Jireh Loreaux]

Why doesn't @loogle (∀ y, inner ?x y = inner ?z y), ?x = ?z

find docs#ext_inner_right here?

[loogle]

:shrug: nothing found

[Floris van Doorn]

@loogle (∀ y, inner ?x y = inner ?z y) -> ?x = ?z

[loogle]

:search: ext_inner_right

[Floris van Doorn]

That doesn't answer your question. I don't your the answer.

[Floris van Doorn]

I expect that Loogle doesn't like this quantifier as head of an expression. This also works:
@loogle inner _ ?y = inner _ ?y

[loogle]

:search: ext_inner_right, ext_inner_map, and 4 more

[Floris van Doorn]

(@Joachim Breitner )

[Joachim Breitner]

(∀ y, inner ?x y = inner ?z y) is equivalent to (y : ?x) → inner ?x y = inner ?z y. I would have assumed that this would be equivalent to searching for inner ?x ?y = inner ?z ?y and then finding a hypothesis matching ?x, but it seems that this somewhere doesn't work.

So I don’t your the answer either.

[Joachim Breitner]

But using the same metavariables on independent filters (the comma-separated things) doesn’t do what you want it to do anyways. Likely loogle should warn about this. If you want the metavariable to scope that way, you have to put them into one expression, like Floris did.

[Eric Wieser]

does P -> R match expressions of the form P -> Q -> R?

[Eric Wieser]

Because if not, then that's often a reason for wanting to use independent filters

[Joachim Breitner]

Eric Wieser said:

does P -> R match expressions of the form P -> Q -> R?

It should

[Joachim Breitner]

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
:search: (?a -> ?b) -> List ?a -> List ?b
:search: List ?a -> (?a -> ?b) -> List ?b

[Joachim Breitner]

@loogle (?a -> ?b) -> List ?b

[loogle]

:search: List.modifyHead, List.map, and 20 more