60dbc48 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add %instance for explicit access to resolveTC tactic

60dbc48Edwin Brady14 years ago

src/Idris/ElabTerm.hs+2−1

@@ -478,7 +478,8 @@ resolveTC :: Int -> Name -> IState -> ElabD ()

478resolveTC 0 fn ist = fail $ "Can't resolve type class"

479resolveTC 1 fn ist = try (trivial ist) (resolveTC 0 fn ist)

480resolveTC depth fn ist

481+ = do compute

481− = try (trivial ist)

482+ try (trivial ist)

482 (do t <- goal

483 (do t <- goal

483 let insts = findInstances ist t

484 let insts = findInstances ist t

484 let (tc, ttypes) = unApply t

485 let (tc, ttypes) = unApply t

src/Idris/Parser.hs+1

@@ -738,6 +738,7 @@ pTacticsExpr syn = do

738pSimpleExpr syn =

739 try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)

740 <|> do lchar '?'; x <- pName; return (PMetavar x)

741+ <|> do lchar '%'; fc <- pfc; reserved "instance"; return (PResolveTC fc)

741 <|> do reserved "refl"; fc <- pfc;

742 <|> do reserved "refl"; fc <- pfc;

742 tm <- option Placeholder (do lchar '{'; t <- pExpr syn; lchar '}';

743 tm <- option Placeholder (do lchar '{'; t <- pExpr syn; lchar '}';

743 return t)

744 return t)