From 790f943e5f0e012212aca9af7dd778c72f89d2dc Mon Sep 17 00:00:00 2001
From: Johan <ago8e3j603@gmail.com>
Date: Wed, 28 Oct 2026 23:25:49 +0100
Subject: [PATCH 1/2] fix: key visited expressions by structural equality

---
 Export.lean | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

diff --git a/Export.lean b/Export.lean
index cda1993..ff518ff 100644
--- a/Export.lean
+++ b/Export.lean
@@ -32,10 +32,28 @@ def Lean.KVMap.toJson (kvs: Lean.KVMap) : Json :=
 structure Context where
   env : Environment
 
+/--
+A wrapper around `Expr` whose `BEq` uses structural equality. This keeps
+expressions that differ only in binder names or binder info distinct in
+`visitedExprs`, so an export does not depend on which declarations were
+exported before it.
+-/
+structure ExprKey where
+  expr : Expr
+  deriving Inhabited
+
+instance : BEq ExprKey where
+  beq a b := a.expr.equal b.expr
+
+instance : Hashable ExprKey where
+  -- `Expr.hash` ignores binder names, so it is compatible with the finer
+  -- `Expr.equal` relation used by `BEq`.
+  hash a := hash a.expr
+
 structure State where
   visitedNames : HashMap Name Nat := HashMap.emptyWithCapacity 200000 |>.insert .anonymous 0
   visitedLevels : HashMap Level Nat := HashMap.emptyWithCapacity 1000 |>.insert .zero 0
-  visitedExprs : HashMap Expr Nat := HashMap.emptyWithCapacity 10000000
+  visitedExprs : HashMap ExprKey Nat := HashMap.emptyWithCapacity 10000000
   visitedConstants : NameHashSet := {}
   noMDataExprs : HashMap Expr Expr := HashMap.emptyWithCapacity 100000
   exportMData : Bool := false
@@ -155,7 +173,7 @@ def removeMData (e : Expr) : M Expr := do
 mutual
 
 partial def dumpExprAux (e : Expr) : M Nat := do
-  getIdx e "ie" (·.visitedExprs) ({ · with visitedExprs := · }) do
+  getIdx (ExprKey.mk e) "ie" (·.visitedExprs) ({ · with visitedExprs := · }) do
     match e with
     | .fvar .. | .mvar .. => panic! "cannot export free variables or metavariables"
     | .mdata a e' =>

From 516949981281bb36449c9738f01bf7ca66c2bd40 Mon Sep 17 00:00:00 2001
From: Johan <ago8e3j603@gmail.com>
Date: Wed, 28 Oct 2026 23:25:55 +0100
Subject: [PATCH 2/2] test: cover expression cache with differing binders

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

diff --git a/Test.lean b/Test.lean
index c3a46da..bf23dd3 100644
--- a/Test.lean
+++ b/Test.lean
@@ -70,6 +70,22 @@ info: {"in":1,"str":{"pre":0,"str":"Prod"}}
 #guard_msgs in
 #eval run <| dumpExpr (.proj `Prod 1 (.bvar 0))
 
+/--
+info:
+{"in":1,"str":{"pre":0,"str":"x"}}
+{"ie":0,"sort":0}
+{"bvar":0,"ie":1}
+{"ie":2,"lam":{"binderInfo":"default","body":1,"name":1,"type":0}}
+{"in":2,"str":{"pre":0,"str":"y"}}
+{"ie":3,"lam":{"binderInfo":"implicit","body":1,"name":2,"type":0}}
+-/
+#guard_msgs in
+#eval runEmpty <| do
+  let e1 := .lam `x (.sort .zero) (.bvar 0) .default
+  let e2 := .lam `y (.sort .zero) (.bvar 0) .implicit
+  let _ ← dumpExpr e1
+  let _ ← dumpExpr e2
+
 /-- info: {"ie":0,"natVal":"100000000000000023456789"}
 -/
 #guard_msgs in