@@ -49,12 +49,12 @@ names over '_', patterns over names, etc.
49-- variable updates
49-- variable updates
50split :: Name -> PTerm -> Idris [[(Name, PTerm)]]
50split :: Name -> PTerm -> Idris [[(Name, PTerm)]]
52+ = do ist <- getIState
52− = do (tm, ty, pats) <- elabValBind toplevel True t'
53+ (tm, ty, pats) <- elabValBind toplevel True (addImplPat ist t')
53 logLvl 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)
54 logLvl 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)
55-- iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))
55-- iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))
56-- iputStrLn (show pats)
56-- iputStrLn (show pats)
57− let t = mergeUserImpl (addImpl ist t') (delab ist tm) -- addImplPat ist t'
57+ let t = mergeUserImpl (addImplPat ist t') (delab ist tm)
58 let ctxt = tt_ctxt ist
58 let ctxt = tt_ctxt ist
59 case lookup n pats of
59 case lookup n pats of
60 Nothing -> fail $ show n ++ " is not a pattern variable"
60 Nothing -> fail $ show n ++ " is not a pattern variable"