lean4/tests/elab/grind_cat2.lean.out.expected at master - lean4 - Gitea: Git with a cup of tea

sdgoij/lean4

mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00

Files

Sebastian Ullrich db6aa9d8d3 feat: move instance-class check to declaration site (#12325 )

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>

2026-03-06 03:23:27 +00:00

3 lines

128 B

Plaintext

Raw Permalink Blame History

	grind_cat2.lean:179:4-179:14: warning: declaration uses `sorry`
	grind_cat2.lean:244:4-244:19: warning: declaration uses `sorry`