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

chore(library/init/lean/compiler/pushproj): cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-02 15:45:56 -07:00
parent 02da0177bb
commit fb8bbee609
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/lean/compiler/pushproj.lean
View file

@ -14,7 +14,7 @@ partial def pushProjs : Array FnBody → Array Alt → Array IndexSet → Array
else
let b := bs.back in
let bs := bs.pop in
let done (_ : Unit) := ((bs.push b) ++ ps.reverse, alts) in
let done (_ : Unit) := (bs.push b ++ ps.reverse, alts) in
let skip (_ : Unit) := pushProjs bs alts afvs (ps.push b) (b.collectFreeVars vs) in
match b with
| FnBody.vdecl x t v _ :=