on master help sign in
Fix :t for metavariables
9b3f202Edwin Brady
src/Idris/Delaborate.hs+1
@@ -21,6 +21,7 @@ delabTy i n
21 = case lookupTy n (tt_ctxt i) of
21 = case lookupTy n (tt_ctxt i) of
22 (ty:_) -> case lookupCtxt n (idris_implicits i) of
22 (ty:_) -> case lookupCtxt n (idris_implicits i) of
23 (imps:_) -> delabTy' i imps ty False
23 (imps:_) -> delabTy' i imps ty False
24+ _ -> delabTy' i [] ty False
24
25
25delab' :: IState -> Term -> Bool -> PTerm
26delab' :: IState -> Term -> Bool -> PTerm
26delab' i t f = delabTy' i [] t f
27delab' i t f = delabTy' i [] t f