From e3f32a61086eab4c311765fb14d1a8a81a70f7a1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 2 May 2019 15:02:35 -0700
Subject: [PATCH] chore(library/init/lean/compiler): cleanup

---
 library/init/lean/compiler/elimdead.lean | 2 +-
 library/init/lean/compiler/ir.lean       | 2 +-
 library/init/lean/compiler/pushproj.lean | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/library/init/lean/compiler/elimdead.lean b/library/init/lean/compiler/elimdead.lean
index 7ce008bebd..36799982a8 100644
--- a/library/init/lean/compiler/elimdead.lean
+++ b/library/init/lean/compiler/elimdead.lean
@@ -35,7 +35,7 @@ partial def FnBody.elimDead : FnBody → FnBody
   let bs         := modifyJPVals bs FnBody.elimDead in
   let term       := match term with
     | FnBody.case tid x alts :=
-      let alts := alts.hmap $ λ alt, alt.modifyBody $ λ b, FnBody.elimDead b in
+      let alts := alts.hmap $ λ alt, alt.modifyBody FnBody.elimDead in
       FnBody.case tid x alts
     | other := other in
   reshapeWithoutDead bs term
diff --git a/library/init/lean/compiler/ir.lean b/library/init/lean/compiler/ir.lean
index d880333bcf..d0f1f0d04d 100644
--- a/library/init/lean/compiler/ir.lean
+++ b/library/init/lean/compiler/ir.lean
@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.lean.name init.lean.kvmap init.lean.format init.data.array
-
 /-
 Implements (extended) λPure and λRc proposed in the article
 "Counting Immutable Beans", Sebastian Ullrich and Leonardo de Moura.
@@ -581,6 +580,7 @@ partial def formatFnBody (indent : Nat := 2) : FnBody → Format
 | FnBody.unreachable         := "⊥"
 
 instance fnBodyHasFormat : HasFormat FnBody := ⟨formatFnBody⟩
+instance fnBodyHasToString : HasToString FnBody := ⟨λ b, (format b).pretty⟩
 
 def formatDecl (indent : Nat := 2) : Decl → Format
 | (Decl.fdecl f xs ty b) := "def " ++ format f ++ formatArray xs ++ format " : " ++ format ty ++ " :=" ++ Format.nest indent (Format.line ++ formatFnBody indent b)
diff --git a/library/init/lean/compiler/pushproj.lean b/library/init/lean/compiler/pushproj.lean
index 4373fa3d27..aede9f72bc 100644
--- a/library/init/lean/compiler/pushproj.lean
+++ b/library/init/lean/compiler/pushproj.lean
@@ -41,7 +41,7 @@ partial def FnBody.pushProj : FnBody → FnBody
   | FnBody.case tid x alts :=
     let afvs       := alts.map $ λ alt, alt.body.freeVars in
     let (bs, alts) := pushProjs bs alts afvs Array.empty {x.idx} in
-    let alts       := alts.hmap $ λ alt, alt.modifyBody $ λ b, FnBody.pushProj b in
+    let alts       := alts.hmap $ λ alt, alt.modifyBody FnBody.pushProj in
     let term       := FnBody.case tid x alts in
     reshape bs term
   | other := reshape bs term