Improve :t for names with implicit args
commit74183cb1ab0d9941bfad63a476f5293337e73632
authorEdwin Brady <eb@cs.st-andrews.ac.uk>
dateMon 14 Nov 2011, 10:15 (15 years ago)
parent5afe678
src/Idris/REPL.hs+2
@@ -86,6 +86,8 @@ process _ (Eval t) = do (tm, ty) <- elabVal toplevel False t
8686 logLvl 3 $ "Raw: " ++ show (tm', ty')
8787 iputStrLn (show (delab ist tm') ++ " : " ++
8888 show (delab ist ty'))
89+process x (Check (PRef _ n))
90+ = process x (Check (PQuote (Var n)))
8991process _ (Check t) = do (tm, ty) <- elabVal toplevel False t
9092 ctxt <- getContext
9193 ist <- get