Skip to content

Commit

Permalink
Apply suggestions from code review
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em authored Sep 13, 2024
1 parent 9fc966a commit 05f5fe6
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions LeanSearchClient/Syntax.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 =>
Expand Down

0 comments on commit 05f5fe6

Please sign in to comment.