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>
12 lines
1 KiB
Text
12 lines
1 KiB
Text
2115.lean:16:0-16:36: warning: Definition `foo` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
|
||
def foo : {α : Type} → [D α] → A α :=
|
||
fun {α : Type} [inst : D α] => @inferInstance.{1} (A α) (@B.toA α (@D.toB α inst))
|
||
2115.lean:21:0-21:36: warning: Definition `bla` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
|
||
def bla : {α : Type} → [D α] → A α :=
|
||
fun {α : Type} [inst : D α] => @inferInstance.{1} (A α) (@C.toA α (@D.toC α inst))
|
||
2115.lean:26:0-26:36: warning: Definition `boo` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
|
||
def boo : {α : Type} → [D α] → A α :=
|
||
fun {α : Type} [inst : D α] => @inferInstance.{1} (A α) (@B.toA α (@D.toB α inst))
|
||
2115.lean:31:0-31:37: warning: Definition `boo2` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
|
||
def boo2 : {α : Type} → [D α] → A α :=
|
||
fun {α : Type} [inst : D α] => @inferInstance.{1} (A α) (@C.toA α (@D.toC α inst))
|