From 1d6205d76b277401ce3b31f474afe989c03787c0 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 6 Jan 2026 13:39:58 +1100 Subject: [PATCH] fix: normalize `nonDep` flag for `letE` expressions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The `BEq` implementation for `Expr` considers the `nonDep` flag, but `nonDep` is just an optimization hint that doesn't affect semantics. External type checkers (e.g., nanoda_lib) treat expressions as identical regardless of this flag. Without normalization, the same expression can appear twice with different indices (once with `nonDep = true`, once with `nonDep = false`), causing parse errors in external type checkers that expect unique indices. This fix was originally implemented in the ammkrn fork: https://github.com/ammkrn/lean4export/commit/eb023e5 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 --- Export.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/Export.lean b/Export.lean index 8a00d1c..d823e8b 100644 --- a/Export.lean +++ b/Export.lean @@ -77,8 +77,13 @@ def removeMData (e : Expr) : M Expr := do pure <| e.updateApp! (← removeMData f) (← removeMData a) | .lam _ d b _ => pure <| e.updateLambdaE! (← removeMData d) (← removeMData b) - | .letE _ d v b nonDep => - pure <| e.updateLet! (← removeMData d) (← removeMData v) (← removeMData b) nonDep + | .letE _ d v b _ => + -- Normalize `nonDep` to `false` to avoid duplicate expression indices. + -- Lean's `BEq` for `Expr` considers the `nonDep` flag, but external type checkers + -- (e.g., nanoda_lib) treat expressions as identical regardless of this optimization hint. + -- Without normalization, the same expression can get different indices, causing parse errors. + -- See: https://github.com/ammkrn/lean4export/commit/eb023e5 + pure <| e.updateLet! (← removeMData d) (← removeMData v) (← removeMData b) false | .forallE _ d b _ => pure <| e.updateForallE! (← removeMData d) (← removeMData b) | .proj _ _ e2 =>