From ef3288d6d8a5380fe8a23a7555dec7ecd1d52042 Mon Sep 17 00:00:00 2001 From: Siddhartha Gadgil Date: Wed, 18 Sep 2024 17:13:35 +0530 Subject: [PATCH] removed noise --- LeanSearchClient/LoogleSyntax.lean | 2 -- 1 file changed, 2 deletions(-) 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 "|- "