From 0c79a8b2ac305ee24af24c76883501c47691b030 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Tue, 25 Aug 2026 13:49:48 -0400
Subject: [PATCH] fix: omit partial declarations unless exportUnsafe is true

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

diff --git a/Export.lean b/Export.lean
index e77a14f..cda1993 100644
--- a/Export.lean
+++ b/Export.lean
@@ -235,7 +235,7 @@ partial def dumpExpr (e : Expr) : M Nat := do
 partial def dumpConstant (c : Name) : M Unit := do
   let some declar := (← read).env.find? c
     | if (← get).ignoreMissing then return else panic! s!"Constant {c} not found in environment."
-  if (declar.isUnsafe && !(← get).exportUnsafe) || (← get).visitedConstants.contains c then
+  if ((declar.isUnsafe || declar.isPartial) && !(← get).exportUnsafe) || (← get).visitedConstants.contains c then
     return
   modify fun st => { st with visitedConstants := st.visitedConstants.insert c }
   match declar with