@@ -211,6 +211,10 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
211 -- we interpret applied lambdas as lets in order to reuse code here
211 -- we interpret applied lambdas as lets in order to reuse code here
212 Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)
212 Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)
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')
214 _ -> error $ "cannot analyse application of: " ++ show fun
218 _ -> error $ "cannot analyse application of: " ++ show fun
216 ins = M.insertWith S.union cd
220 ins = M.insertWith S.union cd