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>
11 lines
568 B
Plaintext
11 lines
568 B
Plaintext
tcloop.lean:14:2-14:15: error: failed to synthesize
|
|
B Nat
|
|
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached
|
|
|
|
Note: Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.
|
|
|
|
Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
|
|
|
|
Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
|
|
tcloop.lean:13:0-14:15: warning: Definition `f` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
|