4afe404 · Idris-dev · git.iko.soy

698 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

699 runT (Exact tm) = do elab ist toplevel False tm

700 when autoSolve solveAll

701− runT (Refine fn []) = do let imps = case lookupCtxt fn (idris_implicits ist) of

701+ runT (Refine fn []) = do imps <- case lookupCtxt fn (idris_implicits ist) of

702− Nothing -> []

702+ Nothing -> envArgs fn

703− Just args -> map isImp args

703+ Just args -> return $ map isImp args

704 ns <- apply (Var fn) imps

705 when autoSolve solveAll

706 where isImp (PImp _ _ _ _) = True

707 isImp _ = False

708+ envArgs n = do e <- get_env

709+ case lookup n e of

710+ Just t -> return $ map (const False)

711+ (getArgTys (binderTy t))

712+ _ -> return []

708 runT (Refine fn imps) = do ns <- apply (Var fn) imps

713 runT (Refine fn imps) = do ns <- apply (Var fn) imps

709 when autoSolve solveAll

714 when autoSolve solveAll

710 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

715 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that