lean4/tests/elab/664.lean 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

8 lines

175 B

Lean4

Raw Permalink Blame History

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

 set_option warn.classDefReducibility false
 class A (α : Type _) where  a : α → Unit
 instance : A Empty where a x := nomatch x
 def test : A Empty where a x := nomatch x