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

chore: more code cleanup

Browse source
This commit is contained in:
tydeu 2021-08-01 18:46:48 -04:00
parent 3643b8e424
commit ba52b36ef8
1 changed files with 8 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
Lake/BuildTarget.lean
View file

@ -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