loogle: Logical or (sum) of patterns

Stream: general

[Jakub Nowak]

Is there a way to do "OR" on patterns on loogle? I often find myself running multiple queries to basically make an OR. The main reason is that mathlib often has multiple definitions for more or less the same thing, so I search trying all of them.

[Aaron Liu]

related, is there a way to do "SETMINUS" on patterns in loogle?

[Jakub Nowak]

Maybe someone should just make Lean to Elasticsearch exporter so we could query definitions in SQL? :thinking:

[Snir Broshi]

I think the point of it is mostly the parser + pattern matcher rather than the DB.
But maybe we can write a small python wrapper, then import loogle and import pandas then do whatever set operations on the results (or a DuckDB plugin if you wanna be fancy)