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