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>
28 lines
1,000 B
Text
28 lines
1,000 B
Text
import Std.Do
|
||
|
||
set_option warn.classDefReducibility false
|
||
|
||
/-
|
||
Section variables should not be included.
|
||
-/
|
||
variable {Q : Std.Do.PostCond α ps}
|
||
def Id.instLawfulMonad' : LawfulMonad Id := by
|
||
apply LawfulMonad.mk' <;> (simp only [Functor.map, id, Functor.mapConst, Seq.seq, SeqRight.seqRight, SeqLeft.seqLeft, bind, pure]; grind)
|
||
|
||
/-- info: Id.instLawfulMonad'.{u_1} : LawfulMonad Id -/
|
||
#guard_msgs in
|
||
#check Id.instLawfulMonad'
|
||
|
||
/-
|
||
Note that they are included when using `grind +revert`.
|
||
The problem is that the idiom `revert` and then re-`intro` while simplifying creates the
|
||
illusion that the section variables are needed.
|
||
-/
|
||
def Id.instLawfulMonad'' : LawfulMonad Id := by
|
||
apply LawfulMonad.mk' <;> (simp only [Functor.map, id, Functor.mapConst, Seq.seq, SeqRight.seqRight, SeqLeft.seqLeft, bind, pure]; grind +revert)
|
||
|
||
/--
|
||
info: Id.instLawfulMonad''.{u_1, u_2} {α : Type u_2} {ps : Std.Do.PostShape} {Q : Std.Do.PostCond α ps} : LawfulMonad Id
|
||
-/
|
||
#guard_msgs in
|
||
#check Id.instLawfulMonad''
|