c1f89fa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Remove the last occurrence of "force".

commitc1f89fa808061fdba7ed46ca39771cae7d9952cb authorMatus Tejiscak <ziman@functor.sk> dateTue 18 Feb 2014, 15:33 (13 years ago) parentda28373

2 files changed+2−2

unifiedsplit

src/IRTS/Compiler.hs+1−1

@@ -177,7 +177,7 @@ instance ToIR (TT Name) where

177177 = do arg' <- ir' env arg

178178 return $ LForce arg'

179179 -- Laziness, the new way

180− | (P _ (UN l) _, [arg]) <- unApply tm,

180+ | (P _ (UN l) _, [_, arg]) <- unApply tm,

181181 l == txt "Delay"

182182 = do arg' <- ir' env arg

183183 return $ LLazyExp arg'

src/Idris/ElabTerm.hs+1−1

@@ -724,7 +724,7 @@ elab ist info pattern opts fn tm

724724 = elabArgs ist ina failed fc r f ns force args

725725 elabArgs ist ina failed fc r f ((argName, holeName):ns) force ((lazy, t) : args)

726726 | lazy && not pattern

727− = elabArg argName holeName (PApp bi (PRef bi (sUN "lazy"))

727+ = elabArg argName holeName (PApp bi (PRef bi (sUN "Delay"))

728728 [pimp (sUN "a") Placeholder True,

729729 pexp t])

730730 | otherwise = elabArg argName holeName t