db6aa9d8d3
This PR adds a warning to any `def` of class type that does not also declare an appropriate reducibility. The warning check runs after elaboration (checking the actual reducibility status via `getReducibilityStatus`) rather than syntactically checking modifiers before elaboration. This is necessary to accommodate patterns like `@[to_additive (attr := implicit_reducible)]` in Mathlib, where the reducibility attribute is applied during `.afterCompilation` by another attribute, and would be missed by a purely syntactic check. --------- Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
42 lines
1.3 KiB
Text
42 lines
1.3 KiB
Text
module
|
|
|
|
/-! Applying `[instance]` after the fact should check for appropriate reducibility. -/
|
|
|
|
/-- warning: Definition `unexposed` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` -/
|
|
#guard_msgs in
|
|
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
|
|
|
|
/-- warning: Definition `exposed` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` -/
|
|
#guard_msgs in
|
|
@[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, implicit_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
|