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

Merge remote-tracking branch 'gebner/minmax'

Browse source
This commit is contained in:
tydeu 2022-10-25 20:58:41 -04:00
commit 17a4bcb3e1
3 changed files with 5 additions and 1 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

2
lean-toolchain
View file

@ -1 +1 @@
leanprover/lean4:nightly-2022-10-20
leanprover/lean4:nightly-2022-10-25