Fix :t for metavariables
Fixes issue #280
commit9b3f2024fe0417a21f964277448bec56c09b869f
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSun 14 Apr 2013, 12:35 (14 years ago)
parent6857a2c
src/Idris/Delaborate.hs+1
@@ -21,6 +21,7 @@ delabTy i n
2121 = case lookupTy n (tt_ctxt i) of
2222 (ty:_) -> case lookupCtxt n (idris_implicits i) of
2323 (imps:_) -> delabTy' i imps ty False
24+ _ -> delabTy' i [] ty False
2425
2526delab' :: IState -> Term -> Bool -> PTerm
2627delab' i t f = delabTy' i [] t f