fix: normalize nonDep flag for letE expressions #11
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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: ammkrn@eb023e5 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jan 6, 2026
This PR adds a new daily CI job that verifies Mathlib using [nanoda_lib](https://github.com/ammkrn/nanoda_lib), an independent Lean 4 type checker written in Rust. Like lean4checker, this runs daily on both master and nightly-testing, and reports results to Zulip (in the `nightly-testing` stream, topic `nanoda` for successes and `nanoda failure` for failures). **Temporary workaround**: This uses a fork of lean4export with leanprover/lean4export#11 applied, which fixes nonDep normalization for export. Once that PR is merged, we can switch back to the official repo. 🤖 Prepared with Claude Code
kim-em
added a commit
to kim-em/mathlib4
that referenced
this pull request
Jan 6, 2026
…3648) This PR adds a new daily CI job that verifies Mathlib using [nanoda_lib](https://github.com/ammkrn/nanoda_lib), an independent Lean 4 type checker written in Rust. Like lean4checker, this runs daily on both master and nightly-testing, and reports results to Zulip (in the `nightly-testing` stream, topic `nanoda` for successes and `nanoda failure` for failures). **Temporary workaround**: This uses a fork of lean4export with leanprover/lean4export#11 applied, which fixes nonDep normalization for export. Once that PR is merged, we can switch back to the official repo. 🤖 Prepared with Claude Code
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR cherry-picks a fix from the ammkrn fork that normalizes the
nonDepflag tofalseforletEexpressions during export.Original commit: ammkrn@eb023e5
The Problem
Lean's
BEqimplementation forExprconsiders thenonDepflag when comparing expressions. However,nonDepis just an optimization hint that doesn't affect semantics - it indicates whether the body of a let-binding uses the bound variable.Without normalization, semantically identical expressions can appear twice in the export with different indices:
nonDep = truenonDep = falseExternal type checkers expect unique indices for identical expressions, causing parse errors like:
The Fix
Always normalize
nonDeptofalseduring export, as originally implemented by @ammkrn.Testing
With this fix, nanoda_lib successfully verifies:
🤖 Prepared with Claude Code