feat: export Quot-package together

Export.lean

@@ -286,16 +286,21 @@ partial def dumpConstant (c : Name) : M Unit := do
         ("all", ← dumpNames val.all)
       ])
     ]
-  | .quotInfo val =>
-    dumpDeps val.type
-    dumpObj [
-      ("quot", .mkObj [
-        ("name", ← dumpName val.name),
-        ("levelParams", ← dumpUparams val.levelParams),
-        ("type", ← dumpExpr val.type),
-        ("kind", val.kind.toJson)
-      ])
-    ]
+  | .quotInfo _ =>
+    -- Always dump full Quot package in the sensible order
+    dumpConstant ``Eq
+    for c in [`Quot, ``Quot.mk, ``Quot.lift, ``Quot.ind] do
+      let some (.quotInfo val) := (← read).env.find? c
+        | panic! s!"Constant {c} not found in environment."
+      modify fun st => { st with visitedConstants := st.visitedConstants.insert c }
+      dumpObj [
+        ("quot", .mkObj [
+          ("name", ← dumpName val.name),
+          ("levelParams", ← dumpUparams val.levelParams),
+          ("type", ← dumpExpr val.type),
+          ("kind", val.kind.toJson)
+        ])
+      ]
   | .inductInfo baseIndVal => do
     let mut indVals := #[]
     let mut ctorVals := #[]

Test.lean

@@ -310,7 +310,22 @@ info: Eq
 Eq.refl
 Eq.rec
 Quot
+Quot.mk
 Quot.lift
+Quot.ind
+-/
+#guard_msgs in
+#eval runParserTest do
+  dumpConstant `Quot.mk
+
+/--
+info: Eq
+Eq.refl
+Eq.rec
+Quot
+Quot.mk
+Quot.lift
+Quot.ind
 -/
 #guard_msgs in
 #eval runParserTest do