max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/pkg
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
..
builtin_attr test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
cbv_attr test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
collectAxioms test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
debug test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
def_clash test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
deprecated_arg test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
deprecated_module test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
deprecated_option test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
deriving test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
frontend test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
homo test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
initialize test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
issue12825 test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
leanchecker test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
linter_set test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
misc test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
mod_clash chore: improve how test suite interacts with stages (#12913) 2026-03-16 15:20:03 +00:00
module test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
path with spaces test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
prv test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
rebuild test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
setup chore: improve how test suite interacts with stages (#12913) 2026-03-16 15:20:03 +00:00
signal test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
structure_docstrings test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
sym_ext test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
sym_simp_attr test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
test_extern test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
user_attr fix: run beforeElaboration attributes on inductives (#13813) 2026-05-21 19:45:59 +00:00
user_attr_app test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
user_ext test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
user_opt test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
user_plugin fix: change plugin separator to = (#13737) 2026-05-15 08:28:21 +00:00
ver_clash chore: clean up old test artifacts (#13179) 2026-03-30 08:02:52 +00:00
.gitignore chore: migrate pkg tests (#12889) 2026-03-11 18:55:46 +00:00