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

chore: Min/Max typeclasses

Browse source
This commit is contained in:
Gabriel Ebner 2022-10-21 11:23:29 -07:00
parent 39feeaab74
commit 783a61ab76
2 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake/Build/Trace.lean
View file

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

2
Lake/Config/LeanConfig.lean
View file

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