From 6a496844fd96dfa2ef9b8e5a893e04202f3beb29 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 6 May 2019 18:38:03 -0700 Subject: [PATCH] chore(library/init/lean/compiler/ir/freevars): simplify code using "no shadowing" assumption --- library/init/lean/compiler/ir/freevars.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/lean/compiler/ir/freevars.lean b/library/init/lean/compiler/ir/freevars.lean index 7b2467934a..6782500714 100644 --- a/library/init/lean/compiler/ir/freevars.lean +++ b/library/init/lean/compiler/ir/freevars.lean @@ -209,8 +209,8 @@ def visitExpr (w : Index) : Expr → Bool | (Expr.isTaggedPtr x) := visitVar w x partial def visitFnBody (w : Index) : FnBody → Bool -| (FnBody.vdecl x _ v b) := visitExpr w v || (!visitVar w x && visitFnBody b) -| (FnBody.jdecl j ys _ v b) := (!visitParams w ys && visitFnBody v) || (!visitJP w j && visitFnBody b) +| (FnBody.vdecl x _ v b) := visitExpr w v || visitFnBody b +| (FnBody.jdecl j ys _ v b) := visitFnBody v || visitFnBody b | (FnBody.set x _ y b) := visitVar w x || visitVar w y || visitFnBody b | (FnBody.uset x _ y b) := visitVar w x || visitVar w y || visitFnBody b | (FnBody.sset x _ _ y _ b) := visitVar w x || visitVar w y || visitFnBody b