From 706c92f7df4f279e989cb1f50748b05f9874f2c5 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 23 Feb 2026 17:11:30 +0100
Subject: [PATCH 1/6] feat: export `Eq` with every `Quot`-related declaration

This PR exports `Eq` with every `Quot`-related declaration. This is for
the benefit of checkers who want to create the whole `Quot` package
(including `Quot.lift`, which uses `Eq`) as soon as `Quot` is added, and
to allow such checkers to process pruned environments that may happen to
exclude `Quot.lift`.
---
 Export.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Export.lean b/Export.lean
index 1e99345..c976463 100644
--- a/Export.lean
+++ b/Export.lean
@@ -287,6 +287,7 @@ partial def dumpConstant (c : Name) : M Unit := do
       ])
     ]
   | .quotInfo val =>
+    dumpConstant ``Eq
     dumpDeps val.type
     dumpObj [
       ("quot", .mkObj [

From 54ace96bdf00e625be3955c734e6f750219856c1 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 23 Feb 2026 17:25:19 +0100
Subject: [PATCH 2/6] Always dump full quot package

---
 Export.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/Export.lean b/Export.lean
index c976463..4d60ebb 100644
--- a/Export.lean
+++ b/Export.lean
@@ -287,8 +287,12 @@ partial def dumpConstant (c : Name) : M Unit := do
       ])
     ]
   | .quotInfo val =>
-    dumpConstant ``Eq
-    dumpDeps val.type
+    -- Always dump full Quot package (also pulls in Eq)
+    dumpConstant ``Quot
+    dumpConstant ``Quot.mk
+    dumpConstant ``Quot.lift
+    dumpConstant ``Quot.ind
+    dumpConstant ``Quot.sound
     dumpObj [
       ("quot", .mkObj [
         ("name", ← dumpName val.name),

From ddae828063a3ccc5327b14e99b7f168ff3dcff44 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 23 Feb 2026 17:34:10 +0100
Subject: [PATCH 3/6] Like this?

---
 Export.lean | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

diff --git a/Export.lean b/Export.lean
index 4d60ebb..b59fd8d 100644
--- a/Export.lean
+++ b/Export.lean
@@ -286,21 +286,21 @@ partial def dumpConstant (c : Name) : M Unit := do
         ("all", ← dumpNames val.all)
       ])
     ]
-  | .quotInfo val =>
-    -- Always dump full Quot package (also pulls in Eq)
-    dumpConstant ``Quot
-    dumpConstant ``Quot.mk
-    dumpConstant ``Quot.lift
-    dumpConstant ``Quot.ind
-    dumpConstant ``Quot.sound
-    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.lift, ``Quot.ind, ``Quot.sound] 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 := #[]

From 249cb9bdb83b35ed0703fa15e9fbf7048a7c0c7a Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 23 Feb 2026 17:36:17 +0100
Subject: [PATCH 4/6] Like this?

---
 Export.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Export.lean b/Export.lean
index b59fd8d..32e34f8 100644
--- a/Export.lean
+++ b/Export.lean
@@ -289,7 +289,7 @@ partial def dumpConstant (c : Name) : M Unit := do
   | .quotInfo _ =>
     -- Always dump full Quot package in the sensible order
     dumpConstant ``Eq
-    for c in [`Quot, ``Quot.lift, ``Quot.ind, ``Quot.sound] do
+    for c in [`Quot, ``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 }

From 777c921eba89aac5f14cc388717935b5fa2cb739 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 23 Feb 2026 17:38:38 +0100
Subject: [PATCH 5/6] Like this?

---
 Export.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Export.lean b/Export.lean
index 32e34f8..2054d47 100644
--- a/Export.lean
+++ b/Export.lean
@@ -289,7 +289,7 @@ partial def dumpConstant (c : Name) : M Unit := do
   | .quotInfo _ =>
     -- Always dump full Quot package in the sensible order
     dumpConstant ``Eq
-    for c in [`Quot, ``Quot.lift, ``Quot.ind] do
+    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 }

From c38c9357cc390d140fc63ff2dc0243a07ccb78d1 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 23 Feb 2026 17:52:44 +0100
Subject: [PATCH 6/6] Update test

---
 Test.lean | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/Test.lean b/Test.lean
index 406e5c0..0394cfb 100644
--- a/Test.lean
+++ b/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