Command with examples

leanprover-community · Sep 13, 2024 · 0105add · 0105add
1 parent e51d414
commit 0105add
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/LeanSearchClient/LoogleSyntax.lean b/LeanSearchClient/LoogleSyntax.lean
@@ -158,4 +158,8 @@ syntax (name := loogle_cmd) "#loogle" str "go" : command
 
 #loogle "List ?a → ?b" go
 
+#loogle "nonsense" go
+
+#loogle "?a → ?b" go
+
 end LeanSearchClient