max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/lean/compiler/ir/freevars): simplify code using "no shadowing" assumption

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-06 18:38:03 -07:00
parent 1295bf52bc
commit 6a496844fd
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/lean/compiler/ir/freevars.lean
View file

@ -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