mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-21 10:18:23 +03:00
rename proof search to type search
This commit is contained in:
parent
34bfb159f2
commit
0b0c9b33a4
@ -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"
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
Loading…
Reference in New Issue
Block a user