From 05f5fe675bac676b6815d6c49df42c1c546cd1fa Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 13 Sep 2024 13:33:38 +1000 Subject: [PATCH] Apply suggestions from code review --- LeanSearchClient/Syntax.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/LeanSearchClient/Syntax.lean b/LeanSearchClient/Syntax.lean index bcf9d37..b86846b 100644 --- a/LeanSearchClient/Syntax.lean +++ b/LeanSearchClient/Syntax.lean @@ -174,17 +174,17 @@ instance : Inhabited SearchServer := ⟨leanSearchServer⟩ namespace SearchServer -def getCommandSuggestions (ss : SearchServer) (s : String)(num_results : Nat) : +def getCommandSuggestions (ss : SearchServer) (s : String) (num_results : Nat) : MetaM (Array TryThis.Suggestion) := do let suggestions ← ss.query s num_results return suggestions.map SearchResult.toCommandSuggestion -def getTermSuggestions (ss : SearchServer) (s : String)(num_results : Nat) : +def getTermSuggestions (ss : SearchServer) (s : String) (num_results : Nat) : MetaM (Array TryThis.Suggestion) := do let suggestions ← ss.query s num_results return suggestions.map SearchResult.toTermSuggestion -def getTacticSuggestionGroups (ss : SearchServer) (s : String)(num_results : Nat) : +def getTacticSuggestionGroups (ss : SearchServer) (s : String) (num_results : Nat) : MetaM (Array (String × Array TryThis.Suggestion)) := do let suggestions ← ss.query s num_results return suggestions.map fun sr =>