on master help sign in
Account for 'let' with unbound implicits
32c2467Edwin Brady
src/Idris/AbsSyntaxTree.hs+2
@@ -2472,6 +2472,8 @@ implicitNamesIn uvars ist tm
2472 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2472 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2473 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2473 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2474 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2474 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2475+ ni 0 env (PLet fc n _ ty val sc) = do ni 0 env ty;
2476+ ni 0 env val; ni 0 (n:env) sc
2475 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2477 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2476 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2478 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2477 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2479 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r