From 9bed367cc06751caa974ed2fb2a761e300296422 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 26 Jul 2019 16:46:03 -0700
Subject: [PATCH] feat(library/init/lean/modulename): add helper functions

---
 library/init/lean/modulename.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

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