refactor: rename instance_reducible to implicit_reducible#12567
Merged
leodemoura merged 2 commits intomasterfrom Feb 18, 2026
Merged
refactor: rename instance_reducible to implicit_reducible#12567leodemoura merged 2 commits intomasterfrom
leodemoura merged 2 commits intomasterfrom
Conversation
This PR renames the `ReducibilityStatus.instanceReducible` constructor to `implicitReducible` and adds a new `[implicit_reducible]` attribute. The old `[instance_reducible]` attribute is kept as an alias for backward compatibility. The rename reflects the broader role of this transparency level: it covers not just type class instances but any definition that needs to be unfolded when checking implicit arguments (e.g., `Nat.add`, `Array.size`). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds the `backward.isDefEq.implicitBump` option (default: `false`) that controls whether all implicit arguments get their transparency bumped to `TransparencyMode.instances` during `isDefEq`, not just instance-implicit ones. When enabled, `[implicit_reducible]` definitions like `Nat.add` and `Array.size` are unfolded when checking implicit arguments, closing the gap between instance-implicit and regular implicit argument handling. The default is `false` for staging purposes. After stage0 is updated, the default will be flipped to `true`. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
github-merge-queue bot
pushed a commit
that referenced
this pull request
Feb 20, 2026
This PR is part 2 of the `implicit_reducible` refactoring (part 1: #12567). **Background.** When Lean checks definitional equality of function applications `f a₁ ... aₙ =?= f b₁ ... bₙ`, it compares arguments `aᵢ =?= bᵢ` at a transparency level determined by the binder type. Previously, only instance-implicit (`[C]`) arguments received a transparency bump to `.instances`. With `backward.isDefEq.implicitBump` enabled, ALL implicit arguments (`{x}`, `⦃x⦄`, and `[x]`) are bumped to `.instances`, so that definitions marked `[implicit_reducible]` unfold when comparing implicit arguments. This is important because implicit arguments often carry type information (e.g., `P (i + 0)` vs `P i`) where the mismatch is in non-proof positions (Sort arguments to `cast`) — proof irrelevance does not help here, so the relevant definitions must actually unfold. **`[implicit_reducible]`** (renamed from `[instance_reducible]` in part 1) marks definitions that should unfold at `TransparencyMode.instances` — between `[reducible]` (unfolds at `.reducible` and above) and the default `[semireducible]` (unfolds only at `.default` and above). This is the right level for core arithmetic operations that appear in type indices. ## Changes - **Enable `backward.isDefEq.implicitBump` by default** and set it in `stage0/src/stdlib_flags.h` so stage0 also compiles with it - **Mark `Nat.add`, `Nat.mul`, `Nat.sub`, `Array.size` as `[implicit_reducible]`** so they unfold when comparing implicit arguments at `.instances` transparency - **Remove redundant unification hints** (`n + 0 =?= n`, `n - 0 =?= n`, `n * 0 =?= 0`) that are now handled by `[implicit_reducible]` - **Rename all remaining `[instance_reducible]` attribute usages** to `[implicit_reducible]` across the codebase (the old name remains as an alias) - **Remove 28 `set_option backward.isDefEq.respectTransparency false in`** workarounds that are no longer needed 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
kim-em
added a commit
to leanprover/doc-gen4
that referenced
this pull request
Feb 21, 2026
Adapts to leanprover/lean4#12567 which renamed `ReducibilityStatus.instanceReducible` to `implicitReducible`. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
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
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 renames
instance_reducibletoimplicit_reducibleand adds a newbackward.isDefEq.implicitBumpoption to prepare for treating all implicitarguments uniformly during definitional equality checking.
Changes
Rename
instance_reducible→implicit_reducible:ReducibilityStatus.instanceReducibleconstructor toimplicitReducible[implicit_reducible]attribute, keep[instance_reducible]as aliasisInstanceReducible→isImplicitReducible(with deprecated aliases)The rename reflects that this reducibility level is used not just for instances
but for any definition that needs unfolding during implicit argument resolution
(e.g.,
Nat.add,Array.size).Add
backward.isDefEq.implicitBumpoption:true(+respectTransparency), bumps transparency to.instancesforALL implicit arguments in
isDefEqArgs, not just instance-implicit onesfalsefor staging compatibility — will be flipped totrueafterstage0 update
// update me!tostage0/src/stdlib_flags.hto trigger CI stage0 updateFollow-up (after stage0 update)
backward.isDefEq.implicitBumpdefault totrue🤖 Generated with Claude Code
Co-Authored-By: Claude Opus 4.6 noreply@anthropic.com