on master help sign in
:t prints all names, rather than checking for unique name
a678b80Edwin Brady
src/Idris/REPL.hs+3−3
@@ -151,9 +151,9 @@ process fn (Check (PRef _ n))
151 ist <- get
151 ist <- get
152 imp <- impShow
152 imp <- impShow
153 case lookupTy Nothing n ctxt of
153 case lookupTy Nothing n ctxt of
154− [t] -> iputStrLn $ show n ++ " : " ++
154+ ts@(_:_) -> mapM_ (\t -> iputStrLn $ show n ++ " : " ++
155− showImp imp (delab ist t)
155+ showImp imp (delab ist t)) ts
156− _ -> iputStrLn $ "No such variable " ++ show n
156+ [] -> iputStrLn $ "No such variable " ++ show n
157process fn (Check t) = do (tm, ty) <- elabVal toplevel False t
157process fn (Check t) = do (tm, ty) <- elabVal toplevel False t
158 ctxt <- getContext
158 ctxt <- getContext
159 ist <- get
159 ist <- get