git.iko.soy/Idris-dev
on master help sign in
Remove the last occurrence of "force".
c1f89faMatus Tejiscak
src/IRTS/Compiler.hs+1−1
compare with master
unifiedsplit
@@ -177,7 +177,7 @@ instance ToIR (TT Name) where
177 = do arg' <- ir' env arg
177 = do arg' <- ir' env arg
178 return $ LForce arg'
178 return $ LForce arg'
179 -- Laziness, the new way
179 -- Laziness, the new way
180− | (P _ (UN l) _, [arg]) <- unApply tm,
180+ | (P _ (UN l) _, [_, arg]) <- unApply tm,
181 l == txt "Delay"
181 l == txt "Delay"
182 = do arg' <- ir' env arg
182 = do arg' <- ir' env arg
183 return $ LLazyExp arg'
183 return $ LLazyExp arg'
src/Idris/ElabTerm.hs+1−1
@@ -724,7 +724,7 @@ elab ist info pattern opts fn tm
724 = elabArgs ist ina failed fc r f ns force args
724 = elabArgs ist ina failed fc r f ns force args
725 elabArgs ist ina failed fc r f ((argName, holeName):ns) force ((lazy, t) : args)
725 elabArgs ist ina failed fc r f ((argName, holeName):ns) force ((lazy, t) : args)
726 | lazy && not pattern
726 | lazy && not pattern
727− = elabArg argName holeName (PApp bi (PRef bi (sUN "lazy"))
727+ = elabArg argName holeName (PApp bi (PRef bi (sUN "Delay"))
728 [pimp (sUN "a") Placeholder True,
728 [pimp (sUN "a") Placeholder True,
729 pexp t])
729 pexp t])
730 | otherwise = elabArg argName holeName t
730 | otherwise = elabArg argName holeName t