max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/pkg/user_attr
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
..
UserAttr fix: run beforeElaboration attributes on inductives (#13813) 2026-05-21 19:45:59 +00:00
lakefile.lean
lean-toolchain chore: relative lean-toolchains (#12652) 2026-02-25 10:23:35 +00:00
run_test.sh test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
UserAttr.lean fix: reject attribute uses whose module is reachable only via IR (#13613) 2026-05-06 11:55:43 +00:00