lean4-htt/tests/elab/inductionTacticBug.lean at master - max/lean4-htt - maxgit: wireguard access, git repository.

max/lean4-htt

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

219 B

Text

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
 def ex {α} : Subsingleton (Squash α) := Subsingleton.intro $ by
   intro a b
   induction a using Squash.ind
   induction b using Squash.ind
   apply Quot.sound
   exact trivial