From f4aabaecae6f250f6314f634a556ec078a1ccc0d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 17 Sep 2020 07:51:06 -0700
Subject: [PATCH] refactor: move `Lean.quote` to `LeanInit`

cc @Kha
---
 src/Init/LeanInit.lean | 37 +++++++++++++++++++++++++++++++++++++
 src/Lean/Syntax.lean   | 37 -------------------------------------
 2 files changed, 37 insertions(+), 37 deletions(-)

diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean
index 790759176b..4750eddb54 100644
--- a/src/Init/LeanInit.lean
+++ b/src/Init/LeanInit.lean
@@ -762,6 +762,43 @@ def find? (stx : Syntax) (p : Syntax → Bool) : Option Syntax :=
 findAux p stx
 
 end Syntax
+
+/-- Reflect a runtime datum back to surface syntax (best-effort). -/
+class HasQuote (α : Type) :=
+(quote : α → Syntax)
+
+export HasQuote (quote)
+
+instance Syntax.HasQuote : HasQuote Syntax := ⟨id⟩
+instance String.HasQuote : HasQuote String := ⟨mkStxStrLit⟩
+instance Nat.HasQuote : HasQuote Nat := ⟨fun n => mkStxNumLit $ toString n⟩
+instance Substring.HasQuote : HasQuote Substring := ⟨fun s => mkCAppStx `String.toSubstring #[quote s.toString]⟩
+
+private def quoteName : Name → Syntax
+| Name.anonymous => mkCIdent `Lean.Name.anonymous
+| Name.str n s _ => mkCAppStx `Lean.mkNameStr #[quoteName n, quote s]
+| Name.num n i _ => mkCAppStx `Lean.mkNameNum #[quoteName n, quote i]
+
+instance Name.hasQuote : HasQuote Name := ⟨quoteName⟩
+
+instance Prod.hasQuote {α β : Type} [HasQuote α] [HasQuote β] : HasQuote (α × β) :=
+⟨fun ⟨a, b⟩ => mkCAppStx `Prod.mk #[quote a, quote b]⟩
+
+private def quoteList {α : Type} [HasQuote α] : List α → Syntax
+| []      => mkCIdent `List.nil
+| (x::xs) => mkCAppStx `List.cons #[quote x, quoteList xs]
+
+instance List.hasQuote {α : Type} [HasQuote α] : HasQuote (List α) := ⟨quoteList⟩
+
+instance Array.hasQuote {α : Type} [HasQuote α] : HasQuote (Array α) :=
+⟨fun xs => mkCAppStx `List.toArray #[quote xs.toList]⟩
+
+private def quoteOption {α : Type} [HasQuote α] : Option α → Syntax
+| none     => mkIdent `Option.none
+| (some x) => mkCAppStx `Option.some #[quote x]
+
+instance Option.hasQuote {α : Type} [HasQuote α] : HasQuote (Option α) := ⟨quoteOption⟩
+
 end Lean
 
 namespace Array
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index d5c20e8312..f328ff2899 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -431,41 +431,4 @@ mkStxStrLit val
 def mkStxNumLitAux (val : Nat) : Syntax :=
 mkStxNumLit (toString val)
 
-
-/-- Reflect a runtime datum back to surface syntax (best-effort). -/
-class HasQuote (α : Type) :=
-(quote : α → Syntax)
-
-export HasQuote (quote)
-
-instance Syntax.HasQuote : HasQuote Syntax := ⟨id⟩
-instance String.HasQuote : HasQuote String := ⟨mkStxStrLit⟩
-instance Nat.HasQuote : HasQuote Nat := ⟨fun n => mkStxNumLit $ toString n⟩
-instance Substring.HasQuote : HasQuote Substring := ⟨fun s => mkCAppStx `String.toSubstring #[quote s.toString]⟩
-
-private def quoteName : Name → Syntax
-| Name.anonymous => mkCIdent `Lean.Name.anonymous
-| Name.str n s _ => mkCAppStx `Lean.mkNameStr #[quoteName n, quote s]
-| Name.num n i _ => mkCAppStx `Lean.mkNameNum #[quoteName n, quote i]
-
-instance Name.hasQuote : HasQuote Name := ⟨quoteName⟩
-
-instance Prod.hasQuote {α β : Type} [HasQuote α] [HasQuote β] : HasQuote (α × β) :=
-⟨fun ⟨a, b⟩ => mkCAppStx `Prod.mk #[quote a, quote b]⟩
-
-private def quoteList {α : Type} [HasQuote α] : List α → Syntax
-| []      => mkCIdent `List.nil
-| (x::xs) => mkCAppStx `List.cons #[quote x, quoteList xs]
-
-instance List.hasQuote {α : Type} [HasQuote α] : HasQuote (List α) := ⟨quoteList⟩
-
-instance Array.hasQuote {α : Type} [HasQuote α] : HasQuote (Array α) :=
-⟨fun xs => mkCAppStx `List.toArray #[quote xs.toList]⟩
-
-private def quoteOption {α : Type} [HasQuote α] : Option α → Syntax
-| none     => mkIdent `Option.none
-| (some x) => mkCAppStx `Option.some #[quote x]
-
-instance Option.hasQuote {α : Type} [HasQuote α] : HasQuote (Option α) := ⟨quoteOption⟩
-
 end Lean