Add %instance for explicit access to resolveTC tactic
commit60dbc48dc3f2761d1dfd55a9420e21fbedf71390
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateThu 20 Dec 2012, 00:58 (14 years ago)
parentbfd5b51
src/Idris/ElabTerm.hs+2−1
@@ -478,7 +478,8 @@ resolveTC :: Int -> Name -> IState -> ElabD ()
478478resolveTC 0 fn ist = fail $ "Can't resolve type class"
479479resolveTC 1 fn ist = try (trivial ist) (resolveTC 0 fn ist)
480480resolveTC depth fn ist
481− = try (trivial ist)
481+ = do compute
482+ try (trivial ist)
482483 (do t <- goal
483484 let insts = findInstances ist t
484485 let (tc, ttypes) = unApply t
src/Idris/Parser.hs+1
@@ -738,6 +738,7 @@ pTacticsExpr syn = do
738738pSimpleExpr syn =
739739 try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)
740740 <|> do lchar '?'; x <- pName; return (PMetavar x)
741+ <|> do lchar '%'; fc <- pfc; reserved "instance"; return (PResolveTC fc)
741742 <|> do reserved "refl"; fc <- pfc;
742743 tm <- option Placeholder (do lchar '{'; t <- pExpr syn; lchar '}';
743744 return t)