chore: move Bootstrap.Dynamic -> Init.Dynamic

src/Bootstrap.lean

@@ -3,4 +3,4 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Bootstrap.Dynamic
+import Bootstrap.Empty

src/Init.lean

@@ -15,6 +15,7 @@ import Init.WFTactics
 import Init.Data
 import Init.System
 import Init.Util
+import Init.Dynamic
 import Init.ShareCommon
 import Init.Meta
 import Init.NotationExtra

src/Init/Dynamic.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: Gabriel Ebner
 -/
+prelude
+import Init.Core
 
-namespace Std
 open Lean
 
 -- Implementation detail of TypeName, since classes cannot be opaque

src/Lean/Elab/Deriving/TypeName.lean

@@ -14,13 +14,12 @@ private def deriveTypeNameInstance (declNames : Array Name) : CommandElabM Bool
     let cinfo ← getConstInfo declName
     unless cinfo.levelParams.isEmpty do
       throwError m!"{mkConst declName} has universe level parameters"
-    let TypeName := mkIdent `TypeName
     elabCommand <| ← withFreshMacroScope `(
-      unsafe def instImpl : $TypeName @$(mkCIdent declName) := .mk _ $(quote declName)
-      @[implementedBy instImpl] opaque inst : $TypeName @$(mkCIdent declName)
-      instance : $TypeName @$(mkCIdent declName) := inst
+      unsafe def instImpl : TypeName @$(mkCIdent declName) := .mk _ $(quote declName)
+      @[implementedBy instImpl] opaque inst : TypeName @$(mkCIdent declName)
+      instance : TypeName @$(mkCIdent declName) := inst
     )
   return true
 
 initialize
-  registerDerivingHandler `TypeName deriveTypeNameInstance
+  registerDerivingHandler ``TypeName deriveTypeNameInstance

src/Lean/Server/Rpc/Basic.lean

@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wojciech Nawrocki
 -/
 import Lean.Data.Json
-import Bootstrap.Dynamic
 
 /-! Allows LSP clients to make Remote Procedure Calls to the server.
 

src/Lean/Widget/Basic.lean

@@ -18,9 +18,9 @@ functionality is purpose-specific to showing the contents of infoview popups.
 structure InfoWithCtx where
   ctx  : Elab.ContextInfo
   info : Elab.Info
-  deriving Inhabited, Std.TypeName
+  deriving Inhabited, TypeName
 
-deriving instance Std.TypeName for MessageData
+deriving instance TypeName for MessageData
 
 instance : ToJson FVarId := ⟨fun f => toJson f.name⟩
 instance : ToJson MVarId := ⟨fun f => toJson f.name⟩

src/Lean/Widget/InteractiveDiagnostic.lean

@@ -19,7 +19,7 @@ inductive StrictOrLazy (α β : Type) : Type
 structure LazyTraceChildren where
   indent : Nat
   children : Array (WithRpcRef MessageData)
-  deriving Std.TypeName
+  deriving TypeName
 
 inductive MsgEmbed where
   | expr : CodeWithInfos → MsgEmbed

tests/lean/derivingRpcEncoding.lean

@@ -14,7 +14,7 @@ def test (α : Type) [RpcEncodable α] (a : α) := M.run do
 
 structure FooRef where
   a : Array Nat
-  deriving Inhabited, Std.TypeName
+  deriving Inhabited, TypeName
 
 #check instTypeNameFooRef
 #eval test (WithRpcRef FooRef) default

tests/lean/derivingRpcEncoding.lean.expected.out

@@ -1,4 +1,4 @@
-instTypeNameFooRef : Std.TypeName FooRef
+instTypeNameFooRef : TypeName FooRef
 ok: {"p": "0"}
 instRpcEncodableBar : RpcEncodable Bar
 ok: {"fooRef": {"p": "0"}, "fooJson": {"s": ""}}