Interpret applied lets as lambdas.
commit4caab41778b98c207d3b49ab2c3ac0d8d0708552
authorMatus Tejiscak <ziman@functor.sk>
dateTue 28 Jan 2014, 16:29 (13 years ago)
parentb1bef1c
src/Idris/Erasure.hs+4
@@ -211,6 +211,10 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
211211 -- we interpret applied lambdas as lets in order to reuse code here
212212 Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)
213213
214+ -- and we interpret applied lets as lambdas
215+ Bind n ( Let ty t') t -> getDepsTerm vs bs cd (App (Bind n (Lam ty) t) t')
216+ Bind n (NLet ty t') t -> getDepsTerm vs bs cd (App (Bind n (Lam ty) t) t')
217+
214218 _ -> error $ "cannot analyse application of: " ++ show fun
215219 where
216220 ins = M.insertWith S.union cd