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>
19 lines
1.3 KiB
Text
19 lines
1.3 KiB
Text
simproc_timeout.lean:54:8-54:23: warning: declaration uses `sorry`
|
|
simproc_timeout.lean:71:4-71:19: warning: declaration uses `sorry`
|
|
simproc_timeout.lean:75:4-75:17: warning: declaration uses `sorry`
|
|
simproc_timeout.lean:79:4-79:11: warning: declaration uses `sorry`
|
|
simproc_timeout.lean:85:9-85:32: warning: declaration uses `sorry`
|
|
simproc_timeout.lean:100:9-100:31: warning: declaration uses `sorry`
|
|
simproc_timeout.lean:118:4-118:7: warning: declaration uses `sorry`
|
|
simproc_timeout.lean:149:9-149:30: warning: declaration uses `sorry`
|
|
simproc_timeout.lean:185:26-185:39: warning: declaration uses `sorry`
|
|
simproc_timeout.lean:187:9-187:15: warning: declaration uses `sorry`
|
|
simproc_timeout.lean:200:18-200:24: warning: declaration uses `sorry`
|
|
simproc_timeout.lean:202:8-202:12: warning: declaration uses `sorry`
|
|
simproc_timeout.lean:211:9-211:13: warning: declaration uses `sorry`
|
|
simproc_timeout.lean:222:8-222:11: warning: declaration uses `sorry`
|
|
simproc_timeout.lean:224:8-224:11: warning: declaration uses `sorry`
|
|
simproc_timeout.lean:237:8-237:21: warning: declaration uses `sorry`
|
|
simproc_timeout.lean:248:8-248:19: warning: declaration uses `sorry`
|
|
simproc_timeout.lean:275:9-275:13: warning: declaration uses `sorry`
|
|
simproc_timeout.lean:285:8-285:17: warning: declaration uses `sorry`
|