From 3e9460c40e09457b2fd079ef55316535536425fc Mon Sep 17 00:00:00 2001 From: Siddhartha Gadgil Date: Tue, 17 Sep 2024 15:46:14 +0530 Subject: [PATCH] removed loogle syntax --- LeanSearchClient.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanSearchClient.lean b/LeanSearchClient.lean index ee7b95d..12be72c 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