on master help sign in
Improve :t for names with implicit args
74183cbEdwin Brady
src/Idris/REPL.hs+2
@@ -86,6 +86,8 @@ process _ (Eval t) = do (tm, ty) <- elabVal toplevel False t
86 logLvl 3 $ "Raw: " ++ show (tm', ty')
86 logLvl 3 $ "Raw: " ++ show (tm', ty')
87 iputStrLn (show (delab ist tm') ++ " : " ++
87 iputStrLn (show (delab ist tm') ++ " : " ++
88 show (delab ist ty'))
88 show (delab ist ty'))
89+process x (Check (PRef _ n))
90+ = process x (Check (PQuote (Var n)))
89process _ (Check t) = do (tm, ty) <- elabVal toplevel False t
91process _ (Check t) = do (tm, ty) <- elabVal toplevel False t
90 ctxt <- getContext
92 ctxt <- getContext
91 ist <- get
93 ist <- get