diff --git a/library/init/lean/modulename.lean b/library/init/lean/modulename.lean
index 6132b0d9fa..f3dab3f39b 100644
--- a/library/init/lean/modulename.lean
+++ b/library/init/lean/modulename.lean
@@ -18,6 +18,17 @@ instance : Inhabited ModuleName := ⟨ModuleName.explicit Name.anonymous⟩
 
 instance : HasCoe Name ModuleName := ⟨explicit⟩
 
+def quickLt : ModuleName → ModuleName → Bool
+| (explicit n₁)    (explicit n₂)    := Name.quickLt n₁ n₂
+| (explicit _)     (relative _ _)   := true
+| (relative _ _)   (explicit _)     := false
+| (relative r₁ n₁) (relative r₂ n₂) := r₁ < r₂ || (r₁ == r₂ && Name.quickLt n₁ n₂)
+
+instance : HasToString ModuleName :=
+⟨fun n => match n with
+ | explicit n   => toString n
+ | relative r n => "".pushn '.' r ++ toString n⟩
+
 end ModuleName
 
 end Lean