From 860de618d20edc6ed060ee412511e5f08a000de2 Mon Sep 17 00:00:00 2001
From: Siddhartha Gadgil <siddhartha.gadgil@gmail.com>
Date: Wed, 18 Sep 2024 15:44:20 +0530
Subject: [PATCH] loogle syntax with nonreserved

---
 LeanSearchClient.lean                    |  2 +-
 LeanSearchClient/LoogleSyntax.lean       | 10 +++++++++-
 LeanSearchClientTest/LoogleExamples.lean |  2 --
 3 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/LeanSearchClient.lean b/LeanSearchClient.lean
index 12be72c..ee7b95d 100644
--- a/LeanSearchClient.lean
+++ b/LeanSearchClient.lean
@@ -2,4 +2,4 @@
 -- Import modules here that should be built as part of the library.
 import LeanSearchClient.Basic
 import LeanSearchClient.Syntax
--- import LeanSearchClient.LoogleSyntax
+import LeanSearchClient.LoogleSyntax
diff --git a/LeanSearchClient/LoogleSyntax.lean b/LeanSearchClient/LoogleSyntax.lean
index 2d6edc3..7bced20 100644
--- a/LeanSearchClient/LoogleSyntax.lean
+++ b/LeanSearchClient/LoogleSyntax.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Siddhartha Gadgil
 -/
 import Lean.Elab.Tactic.Meta
+import Lean.Parser.Basic
 import Lean.Meta.Tactic.TryThis
 import LeanSearchClient.Basic
 import LeanSearchClient.Syntax
@@ -126,8 +127,15 @@ 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 "|- "
+
 /-- The turnstyle uesd bin `#find`, unicode or ascii allowed -/
-syntax turnstyle := patternIgnore("⊢ " <|> "|- ")
+syntax turnstyle := patternIgnore(unicode_turnstile <|> ascii_turnstile)
+
 /-- a single `#find` filter. The `term` can also be an ident or a strlit,
 these are distinguished in `parseFindFilters` -/
 syntax loogle_filter := (turnstyle term) <|> term
diff --git a/LeanSearchClientTest/LoogleExamples.lean b/LeanSearchClientTest/LoogleExamples.lean
index ae06c66..c281de4 100644
--- a/LeanSearchClientTest/LoogleExamples.lean
+++ b/LeanSearchClientTest/LoogleExamples.lean
@@ -16,5 +16,3 @@ set_option loogle.queries 1
 example : 3 ≤ 5 := by
   #loogle Nat.succ_le_succ
   sorry
-
-#loogle List ?a → ?b