diff --git a/LeanSearchClient/LoogleSyntax.lean b/LeanSearchClient/LoogleSyntax.lean index 7bced20..f11134b 100644 --- a/LeanSearchClient/LoogleSyntax.lean +++ b/LeanSearchClient/LoogleSyntax.lean @@ -127,8 +127,6 @@ If you pass more than one such search filter, separated by commas Loogle will re 🔍 Real.sin, \"two\", tsum, _ * _, _ ^ _, |- _ < _ → _ woould find all lemmas which mention the constants Real.sin and tsum, have \"two\" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter." -#check Lean.Parser.nonReservedSymbol - open Lean.Parser private def unicode_turnstile := nonReservedSymbol "⊢ " private def ascii_turnstile := nonReservedSymbol "|- "