This PR modifies the app elaborator to beta reduce arguments while
substituting them into expected types for later arguments. This makes it
consistent with `inferType` and `instantiateMVars`, which both beta
reduce substitutions. In particular, this change ensures that the app
elaborator behaves as if it creates metavariables for each parameter and
assigns elaborated arguments to the metavariables. **Breaking change:**
tactic proofs may need to be modified to remove unnecessary steps, e.g.
`dsimp only` steps that were previously for beta reductions.
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>
This PR deprecates `levelZero` in favor of `Level.zero` and `levelOne`
in favor of the new `Level.one`, and updates all usages throughout the
codebase. The `levelZero` alias was previously required for computed
field `data` to work, but this is no longer needed.
🤖 Prepared with Claude Code
This PR sets up the new integrated test/bench suite. It then migrates
all benchmarks and some related tests to the new suite. There's also
some documentation and some linting.
For now, a lot of the old tests are left alone so this PR doesn't become
even larger than it already is. Eventually, all tests should be migrated
to the new suite though so there isn't a confusing mix of two systems.
2026-02-25 13:51:53 +00:00
Renamed from tests/lean/run/KyleAlg.lean (Browse further)
