Skip to content

Commit

Permalink
removed noise
Browse files Browse the repository at this point in the history
  • Loading branch information
siddhartha-gadgil committed Sep 18, 2024
1 parent 860de61 commit ef3288d
Showing 1 changed file with 0 additions and 2 deletions.
2 changes: 0 additions & 2 deletions LeanSearchClient/LoogleSyntax.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 "|- "
Expand Down

0 comments on commit ef3288d

Please sign in to comment.