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

fix: make sure maxIndex takes into account dead variables too

Browse source
This commit is contained in:
Leonardo de Moura 2019-10-09 14:55:48 -07:00
parent b44e27c91c
commit 8ec03b09ec
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

@ -58,8 +58,8 @@ private def collectAlts (f : FnBody → Collector) (alts : Array Alt) : Collecto
collectArray alts $ fun alt => f alt.body
partial def collectFnBody : FnBody → Collector
| FnBody.vdecl x _ v b => collectExpr v >> collectFnBody b
| FnBody.jdecl j ys v b => collectFnBody v >> collectParams ys >> collectFnBody b
| FnBody.vdecl x _ v b => collectVar x >> collectExpr v >> collectFnBody b
| FnBody.jdecl j ys v b => collectJP j >> collectFnBody v >> collectParams ys >> collectFnBody b
| FnBody.set x _ y b => collectVar x >> collectArg y >> collectFnBody b
| FnBody.uset x _ y b => collectVar x >> collectVar y >> collectFnBody b
| FnBody.sset x _ _ y _ b => collectVar x >> collectVar y >> collectFnBody b