@@ -95,7 +95,12 @@ process (Eval t) = do (tm, ty) <- elabVal toplevel False t
95 iputStrLn (show (delab ist tm') ++ " : " ++
95 iputStrLn (show (delab ist tm') ++ " : " ++
96 show (delab ist ty'))
96 show (delab ist ty'))
97process (Check (PRef _ n))
97process (Check (PRef _ n))
98− = process (Check (PQuote (Var n)))
98+ = do ctxt <- getContext
100+ case lookupTy n ctxt of
101+ Just t -> iputStrLn $ show n ++ " : " ++
103+ _ -> iputStrLn $ "No such variable " ++ show n
99process (Check t) = do (tm, ty) <- elabVal toplevel False t
104process (Check t) = do (tm, ty) <- elabVal toplevel False t
100 ctxt <- getContext
105 ctxt <- getContext
101 ist <- get
106 ist <- get