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