From fb8bbee6097a3bae26447442b059f8b30f0274e9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 May 2019 15:45:56 -0700 Subject: [PATCH] chore(library/init/lean/compiler/pushproj): cleanup --- library/init/lean/compiler/pushproj.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/lean/compiler/pushproj.lean b/library/init/lean/compiler/pushproj.lean index 146d22bfcf..7548d10003 100644 --- a/library/init/lean/compiler/pushproj.lean +++ b/library/init/lean/compiler/pushproj.lean @@ -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 _ :=