From 783a61ab7642ff98ea4cd9a1ace4ca6339325f0d Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 21 Oct 2022 11:23:29 -0700 Subject: [PATCH] chore: Min/Max typeclasses --- Lake/Build/Trace.lean | 2 ++ Lake/Config/LeanConfig.lean | 2 ++ 2 files changed, 4 insertions(+) diff --git a/Lake/Build/Trace.lean b/Lake/Build/Trace.lean index 7dd8045d8e..4b7141e573 100644 --- a/Lake/Build/Trace.lean +++ b/Lake/Build/Trace.lean @@ -153,6 +153,8 @@ instance : Repr MTime := inferInstanceAs (Repr SystemTime) instance : Ord MTime := inferInstanceAs (Ord SystemTime) instance : LT MTime := ltOfOrd instance : LE MTime := leOfOrd +instance : Min MTime := minOfLe +instance : Max MTime := maxOfLe instance : NilTrace MTime := ⟨0⟩ instance : MixTrace MTime := ⟨max⟩ diff --git a/Lake/Config/LeanConfig.lean b/Lake/Config/LeanConfig.lean index 6110a01560..7a84bcc1f4 100644 --- a/Lake/Config/LeanConfig.lean +++ b/Lake/Config/LeanConfig.lean @@ -36,6 +36,8 @@ deriving Inhabited, Repr, DecidableEq, Ord instance : LT BuildType := ltOfOrd instance : LE BuildType := leOfOrd +instance : Min BuildType := minOfLe +instance : Max BuildType := maxOfLe /-- The arguments to pass to `leanc` based on the build type. -/ def BuildType.leancArgs : BuildType → Array String