mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
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>
21 lines
349 B
Lean4
21 lines
349 B
Lean4
set_option warn.classDefReducibility false
|
||
|
||
class WrappedNat (α : Type) where
|
||
n : Nat
|
||
|
||
inductive FalseContainer where
|
||
| nat (n : Nat)
|
||
| oops (f : Prop → False)
|
||
|
||
def f (x : FalseContainer) : WrappedNat FalseContainer :=
|
||
match x with
|
||
| .nat n => { n }
|
||
| .oops f => (f (0 == 0)).rec
|
||
|
||
/--
|
||
info: 1
|
||
-/
|
||
#guard_msgs in
|
||
#eval f (.nat 1) |>.n
|
||
|