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

feat: add convenience functions for constructing a LeanTrace

Browse source
This commit is contained in:
tydeu 2021-07-15 13:04:31 -04:00
parent b14eef6e06
commit 93c9543976
1 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
Lake/BuildTrace.lean
View file

@ -48,3 +48,13 @@ structure LeanTrace where
hash : Hash
mtime : MTime
deriving Inhabited
namespace LeanTrace
def fromHash (hash : Hash) : LeanTrace :=
LeanTrace.mk hash 0
def fromMTime (mtime : MTime) : LeanTrace :=
LeanTrace.mk 0 mtime
end LeanTrace