max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/pkg/user_attr/UserAttr
History
Exact
Kyle Miller ad1c983a43
fix: run beforeElaboration attributes on inductives (#13813) 
This PR fixes an issue where `beforeElaboration` attributes were not
being run on `inductive`/`structure`/`coinductive` commands. Closes
#13433.

There is also light refactoring of MutualInductive, as well as a mild
performance enhancement to avoid repeated re-elaboration of `variable`s.
2026-05-21 19:45:59 +00:00
..
BlaAttr.lean fix: run beforeElaboration attributes on inductives (#13813) 2026-05-21 19:45:59 +00:00
MetaMid.lean fix: reject attribute uses whose module is reachable only via IR (#13613) 2026-05-06 11:55:43 +00:00
MetaUser.lean fix: reject attribute uses whose module is reachable only via IR (#13613) 2026-05-06 11:55:43 +00:00
Tst.lean fix: run beforeElaboration attributes on inductives (#13813) 2026-05-21 19:45:59 +00:00