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>
14 lines
202 B
Text
14 lines
202 B
Text
set_option warn.classDefReducibility false
|
|
|
|
class MyMod :=
|
|
(a : Nat)
|
|
|
|
namespace MyMod
|
|
variable [MyMod]
|
|
def b := a + 1
|
|
end MyMod
|
|
|
|
def myMod1 : MyMod := ⟨0⟩
|
|
|
|
#guard myMod1.a == 0
|
|
#guard myMod1.b == 1
|