From ba52b36ef8049945a8b87782e2099aba5c852e60 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Sun, 1 Aug 2021 18:46:48 -0400
Subject: [PATCH] chore: more code cleanup

---
 Lake/BuildTarget.lean | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean
index 533e63e5ed..86678d1310 100644
--- a/Lake/BuildTarget.lean
+++ b/Lake/BuildTarget.lean
@@ -45,7 +45,7 @@ end Target
 
 -- ## Active Build Target
 
-abbrev ActiveBuildTarget (t : Type) (a : Type) :=
+abbrev ActiveBuildTarget t a :=
   Target t IOTask a
 
 namespace ActiveBuildTarget
@@ -83,7 +83,7 @@ end ActiveBuildTarget
 
 -- ## Build Target
 
-abbrev BuildTarget (t : Type) (a : Type) :=
+abbrev BuildTarget t a :=
   Target t (IO ∘ IOTask) a
 
 namespace BuildTarget
@@ -117,7 +117,8 @@ open System
 
 -- ## File Target
 
-abbrev FileTarget := BuildTarget MTime FilePath
+abbrev FileTarget :=
+  BuildTarget MTime FilePath
 
 namespace FileTarget
 
@@ -131,7 +132,8 @@ end FileTarget
 
 -- ## Active File Target
 
-abbrev ActiveFileTarget := ActiveBuildTarget MTime FilePath
+abbrev ActiveFileTarget :=
+  ActiveBuildTarget MTime FilePath
 
 namespace ActiveFileTarget
 
@@ -142,14 +144,14 @@ def pure (file : FilePath) (depMTime : MTime) : ActiveFileTarget :=
   ActiveBuildTarget.pure file depMTime
 
 end ActiveFileTarget
-
 end
 
 --------------------------------------------------------------------------------
 -- # Lean Target
 --------------------------------------------------------------------------------
 
-abbrev LeanTarget a := ActiveBuildTarget LeanTrace a
+abbrev LeanTarget a :=
+  ActiveBuildTarget LeanTrace a
 
 namespace LeanTarget