Using Loogle

Stream: mathlib4

[Darij Grinberg]

So I'm trying to understand how to use loogle. I want to find a basic logical rule:

https://loogle.lean-lang.org/?q=%28A+%E2%88%A8+B%29+-%3E+%C2%AC+B+-%3E+A

It suggests "* (Std.Time.Modifier.A ∨ B) → ¬B → A" and a bunch of similarly strange hits. What can I do with them?

[Darij Grinberg]

(Getting the impression that these aren't actual hits)

[Mauricio Collares]

https://loogle.lean-lang.org/?q=%28%3Fa+%E2%88%A8+%3Fb%29+-%3E+%C2%AC+%3Fb+-%3E+%3Fa

[Robin Arnez]

You need placeholders (e.g ?A and ?B). It interprets A and B and identifiers

[Darij Grinberg]

ah!

[Darij Grinberg]

so placeholders use ?

[Darij Grinberg]

works perfectly

[Kenny Lau]

works in lean too

[Kevin Buzzard]

(i.e.

import Mathlib

#loogle (?a ∨ ?b) -> ¬ ?b -> ?a -- results appear in infoview

at least if you're connected to the internet)

[Kenny Lau]

I meant that ?a is valid lean syntax not in the context of loogle

[Kenny Lau]

when you do refine ?_ you can also instead do refine ?a

[Kenny Lau]

?a is syntax for named metavariable