From 0b0c9b33a454277c15f0d40054b53a353c9abc23 Mon Sep 17 00:00:00 2001
From: Mathew Polzin <matt.polzin@gmail.com>
Date: Sun, 3 Jan 2021 11:43:58 -0800
Subject: [PATCH] rename proof search to type search

---
 src/Idris/Parser.idr | 2 +-
 src/Idris/REPL.idr   | 6 +++---
 src/Idris/Syntax.idr | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index 1662b0760..f189e9c39 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -1796,7 +1796,7 @@ parserCommandsForHelp : CommandTable
 parserCommandsForHelp =
   [ exprArgCmd (ParseREPLCmd ["t", "type"]) Check "Check the type of an expression"
   , nameArgCmd (ParseREPLCmd ["printdef"]) PrintDef "Show the definition of a function"
-  , exprArgCmd (ParseREPLCmd ["s", "search"]) ProofSearch "Search for values by type"
+  , exprArgCmd (ParseREPLCmd ["s", "search"]) TypeSearch "Search for values by type"
   , nameArgCmd (ParseIdentCmd "di") DebugInfo "Show debugging information for a name"
   , moduleArgCmd (ParseKeywordCmd "module") ImportMod "Import an extra module"
   , noArgCmd (ParseREPLCmd ["q", "quit", "exit"]) Quit "Exit the Idris system"
diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr
index 112d30031..fa24974e6 100644
--- a/src/Idris/REPL.idr
+++ b/src/Idris/REPL.idr
@@ -613,7 +613,7 @@ docsOrType : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              FC -> Name -> Core (List String)
 docsOrType fc n
-    = do syn <- get Syn
+    = do syn  <- get Syn
          defs <- get Ctxt
          all@(_ :: _) <- lookupCtxtName n (gamma defs)
              | _ => throw (UndefinedName fc n)
@@ -749,7 +749,7 @@ process (Exec ctm)
     = execExp ctm
 process Help
     = pure RequestedHelp
-process (ProofSearch searchTerm@(PPi fc rc piInfo _ argTy retTy))
+process (TypeSearch searchTerm@(PPi fc rc piInfo _ argTy retTy))
     = do defs <- branch
          let ctxt = gamma defs
          log "repl.ps" 2 $ "original pi term: " ++ (show searchTerm)
@@ -770,7 +770,7 @@ process (ProofSearch searchTerm@(PPi fc rc piInfo _ argTy retTy))
          doc <- traverse (docsOrType replFC) $ (.fullname) <$> filteredDefs
          pure $ Printed $ vsep $ pretty <$> (intersperse "\n" $ join doc)
 
-process (ProofSearch _)
+process (TypeSearch _)
     = pure $ REPLError $ reflow "Could not parse input as a type signature."
 process (Missing n)
     = do defs <- get Ctxt
diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr
index 147703348..03e59ec34 100644
--- a/src/Idris/Syntax.idr
+++ b/src/Idris/Syntax.idr
@@ -431,7 +431,7 @@ data REPLCmd : Type where
      Compile : PTerm -> String -> REPLCmd
      Exec : PTerm -> REPLCmd
      Help : REPLCmd
-     ProofSearch : PTerm -> REPLCmd
+     TypeSearch : PTerm -> REPLCmd
      DebugInfo : Name -> REPLCmd
      SetOpt : REPLOpt -> REPLCmd
      GetOpts : REPLCmd