b668a18a9d
This PR renames `instance_reducible` to `implicit_reducible` and adds a new `backward.isDefEq.implicitBump` option to prepare for treating all implicit arguments uniformly during definitional equality checking. ## Changes **Rename `instance_reducible` → `implicit_reducible`:** - Rename `ReducibilityStatus.instanceReducible` constructor to `implicitReducible` - Register new `[implicit_reducible]` attribute, keep `[instance_reducible]` as alias - Rename `isInstanceReducible` → `isImplicitReducible` (with deprecated aliases) - Update all references across src/ and tests/ 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.implicitBump` option:** - When `true` (+ `respectTransparency`), bumps transparency to `.instances` for ALL implicit arguments in `isDefEqArgs`, not just instance-implicit ones - Defaults to `false` for staging compatibility — will be flipped to `true` after stage0 update - Adds `// update me!` to `stage0/src/stdlib_flags.h` to trigger CI stage0 update ## Follow-up (after stage0 update) - Flip `backward.isDefEq.implicitBump` default to `true` - Fix resulting test/module failures 🤖 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>
38 lines
1 KiB
Text
38 lines
1 KiB
Text
module
|
|
|
|
/-! Applying `[instance]` after the fact should check for appropriate reducibility. -/
|
|
|
|
public def unexposed : Inhabited Nat := inferInstance
|
|
|
|
/-- warning: instance `unexposed` must be marked with `@[expose]` -/
|
|
#guard_msgs in
|
|
attribute [instance] unexposed
|
|
|
|
/-- warning: instance `unexposed` must be marked with `@[reducible]` or `@[implicit_reducible]` -/
|
|
#guard_msgs in
|
|
attribute [local instance] unexposed
|
|
|
|
@[expose]
|
|
public def exposed : Inhabited Nat := inferInstance
|
|
|
|
/-- warning: instance `exposed` must be marked with `@[reducible]` or `@[implicit_reducible]` -/
|
|
#guard_msgs in
|
|
attribute [instance] exposed
|
|
|
|
/-- warning: instance `exposed` must be marked with `@[reducible]` or `@[implicit_reducible]` -/
|
|
#guard_msgs in
|
|
attribute [local instance] exposed
|
|
|
|
@[expose, instance_reducible]
|
|
public def exposedAndReducible : Inhabited Nat := inferInstance
|
|
|
|
#guard_msgs in
|
|
attribute [instance] exposedAndReducible
|
|
|
|
#guard_msgs in
|
|
attribute [local instance] exposedAndReducible
|
|
|
|
instance bla : Add Int := ⟨Int.add⟩
|
|
|
|
#guard_msgs in
|
|
attribute [irreducible] bla
|