From 69bd25af4ffacd3fd64d8ac789abe50cce72886b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 9 Nov 2022 14:35:57 -0800
Subject: [PATCH] chore: add `Repr` and `Inhabited` instances for `Import`

---
 src/Lean/Environment.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 252fdbb503..2741057a5b 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -31,6 +31,7 @@ abbrev ConstMap := SMap Name ConstantInfo
 structure Import where
   module      : Name
   runtimeOnly : Bool := false
+  deriving Repr, Inhabited
 
 instance : ToString Import := ⟨fun imp => toString imp.module ++ if imp.runtimeOnly then " (runtime)" else ""⟩