git.iko.soy/Idris-dev
on master help sign in
Use `fullExpr` instead of `typeExpr` in search
bd4789c(λ _ λ)
src/Idris/REPL/Parser.hs+1−1
compare with master
unifiedsplit
@@ -521,7 +521,7 @@ packageBasedCmd valParser cmd name =
521
521
522cmd_search :: String -> P.IdrisParser (Either String Command)
522cmd_search :: String -> P.IdrisParser (Either String Command)
523cmd_search = packageBasedCmd
523cmd_search = packageBasedCmd
524− (P.typeExpr (defaultSyntax { implicitAllowed = True })) Search
524+ (P.fullExpr (defaultSyntax { implicitAllowed = True })) Search
525
525
526cmd_proofsearch :: String -> P.IdrisParser (Either String Command)
526cmd_proofsearch :: String -> P.IdrisParser (Either String Command)
527cmd_proofsearch name = do
527cmd_proofsearch name = do