Inductive commands now run beforeElaboration attrs correctly (
ad1c983)
beforeElaboration attributes were being skipped on inductive/structure/coinductive commands; this fixes that regression and closes #13433. The patch also includes a small MutualInductive refactor and avoids repeated re-elaboration of variables for a mild performance win.
#where now reports module scope features (47e96cd)
#where can now show module-related scope state such as @[expose], public, noncomputable, and meta section markers. It also reports omitted variables, making the command more faithful in module files.
Structure instance elaboration gets a quadratic-time fix (1842bb5)
Structure instance notation now beta-reduces substituted structure parameters and field types while elaborating large instances. This should remove a source of quadratic behavior when many fields are involved, which matters for big autogenerated or heavily nested structures.
Proof-mode tactics stop leaking hypothesis metadata (
ed790e9)
mconstructor, mleft, mright, and mspecialize now work again in the affected proof-mode scenarios by stripping hypothesis-naming Expr.mdata at the right non-leaf positions. This fixes failures inside mhave blocks and after mrevert; mintro round trips.
Verso docstring extensions are now enforced as meta in modules (
acfe1d1)
Custom docstring extensions now error early if they are not meta when used in module mode, and the generated getArgs wrapper is marked meta as well. That tightens the discipline around elaboration-time docstring hooks and fixes module-file support for @[doc_role], @[doc_code_block], @[doc_directive], and @[doc_command].
Other misc changes
- App elaboration semantics change with a breaking tweak: beta-reduction now happens while substituting arguments into expected types, which may require simplifying some tactic proofs.
- Small doc fix for
String.split. - Internal string-processing cleanup and assorted
try-based compatibility adjustments inInit/Lakecode.