From 93c954397622a569eba014abe9eb2cf0341f2358 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Thu, 15 Jul 2021 13:04:31 -0400
Subject: [PATCH] feat: add convenience functions for constructing a
 `LeanTrace`

---
 Lake/BuildTrace.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/Lake/BuildTrace.lean b/Lake/BuildTrace.lean
index 5710f483aa..7aa9b9523b 100644
--- a/Lake/BuildTrace.lean
+++ b/Lake/BuildTrace.lean
@@ -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