This PR extends Lean's syntax to allow explicit universe levels in
expressions such as `e.f.{u,v}`, `(f e).g.{u}`, and `e |>.f.{u,v} x y
z`. It fixes a bug where universe levels would be attributed to the
wrong expression; for example `x.f.{u}` would be interpreted as
`x.{u}.f`. It also changes the syntax of top-level declarations to not
allow space between the identifier and the universe level list, and it
fixes a bug in the `checkWsBefore` parser where it would not detect
whitespace across `optional` parsers.
Closes#8743
This PR fixes universe unification for `for` loops with `mut` variables
whose types span multiple implicit universes. The old approach used
`ensureHasType (mkSort mi.u.succ)` per variable, which generated
constraints like `max (?u+1) (?v+1) =?= ?u+1` that the universe solver
cannot decompose. The new approach uses `getDecLevel`/`isLevelDefEq` on
the decremented level, producing `max ?u ?v =?= ?u` which `solveSelfMax`
handles directly.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR wraps the top-level command parser with `withPosition` to
enforce indentation in `by` blocks, combined with an empty-by fallback
for better error messages.
This subsumes #3215 (which introduced `withPosition commandParser` but
without the empty-by fallback). It is also related to #9524, which
explores elaboration with empty tactic sequences — this PR reuses that
idea for the empty-by fallback, so that a `by` not followed by an
indented tactic produces an elaboration error (unsolved goals) rather
than a parse error.
**Changes:**
- `topLevelCommandParserFn` now uses `(withPosition commandParser).fn`,
setting the saved position at the start of each top-level command
- `tacticSeqIndentGt` gains an empty tactic sequence fallback
(`pushNone`) so that missing indentation produces an elaboration error
(unsolved goals) instead of a parse error
- `isEmptyBy` in `goalsAt?` removed: with strict `by` indentation, empty
`by` blocks parse successfully via `pushNone` (producing empty nodes)
rather than producing `.missing` syntax, making the `isEmptyBy` check
dead code. The `isEmpty` helper in `isSyntheticTacticCompletion`
continues to work correctly because it handles both `.missing` and empty
nodes from `pushNone` (via the vacuously-true `args.all isEmpty` on
`#[]`)
- Test files updated to indent `by` blocks and expression continuations
that were previously at column 0
**Behavior:**
- Top-level `by` blocks now require indentation (column > 0 for commands
at column 0)
- Commands indented inside `section` require proofs to be indented past
the command's column
- `#guard_msgs in example : True := by` works because tactic indentation
is checked against the outermost command's column
- Expression continuations (not just `by`) must also be indented past
the command, which is slightly more strict but more consistent
- `have : True := by` followed by a dedent now correctly puts `this` in
scope in the outer tactic block (the `have` is structurally complete
with an unsolved-goal error, rather than a parse error)
**Code changes observed in practice (lean4 test suite + Mathlib):**
- `by` blocks: top-level `theorem ... := by` / `decreasing_by` followed
by tactics at column 0 must be indented
- `variable` continuations: `variable {A : Type*} [Foo A]\n{B : Type*}`
where the second line starts at column 0 must be indented (most common
category in Mathlib)
- Expression continuations: `def f : T :=\nexpr` or `#synth Foo\n[args]`
where the body/arguments start at column 0
- Structure literals: `.symm\n{ toFun := ...` where the struct literal
starts at column 0
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR wires the `PowIdentity` typeclass (from
https://github.com/leanprover/lean4/pull/13086) into the `grind` ring
solver's Groebner basis engine.
When a ring has a `PowIdentity α p` instance, the solver pushes `x ^ p =
x` as a new fact for each variable `x`, which becomes `x^p - x = 0` in
the Groebner basis. Since `p` is an `outParam`, instance discovery is
decoupled from `IsCharP` — the solver synthesizes `PowIdentity α ?p`
with a fresh metavar and lets instance search find both the instance and
the exponent.
This correctly handles non-prime finite fields: for `F_4` (char 2, 4
elements), Mathlib would provide `PowIdentity F_4 4` and the solver
would discover `p = 4`, not `p = 2`.
Note: the original motivating example `(x + y)^2 = x^128 + y^2` from
https://github.com/leanprover/lean4/issues/12842 does not yet work
because the `ToInt` module lifts `Fin 2` expressions to integers and
expands `x^128` via the binomial theorem before the ring solver can
reduce it. Addressing that is a separate deeper change.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR amends #13317 to suggest `:= (rfl)` as the recommended way to
avoid a theorem to be automatically marked `[defeq]`, for consistency
with existing documentation. Rationale: the special treatment of `:=
rfl` is based on syntax, not the proof term, so it’s appropriate to use
different syntax. And also I like the way it reads like a “muted whisper
of `rfl`”.
This PR adds a warning preventing a user from applying global attribute
using `... in ...`, e.g.
```lean4
theorem a : True := trivial
attribute [simp] a in
def b : True := a
```
This PR adds an opt-in linter (`set_option simp.rfl.checkTransparency
true`) that warns when a `rfl` simp theorem's LHS and RHS are not
definitionally equal at `.instances` transparency. Bad rfl-simp theorems
— those that only hold at higher transparency — create problems
throughout the system because `simp` and `dsimp` operate at restricted
transparency. The linter suggests two fixes: use `id rfl` as the proof
(to remove the `rfl` status), or mark relevant constants as
`[implicit_reducible]`.
This is part of a broader effort to ensure `isDefEq` respects
transparency levels. The linter helps systematically identify
problematic rfl-simp theorems so they can be fixed incrementally.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR makes the delta-deriving handler create `theorem` declarations
instead of `def` declarations when the instance type is a `Prop`.
Previously, `deriving instance Nonempty for Foo` would always create a
`def`, which is inconsistent with the behavior of a handwritten
`instance` declaration.
For example, given:
```lean
def Foo (α : Type u) := List α
deriving instance Nonempty for Foo
```
Before: `@[implicit_reducible] def instNonemptyFoo ...`
After: `@[implicit_reducible] theorem instNonemptyFoo ...`
The implementation checks `isProp result.type` after constructing the
instance closure, and uses `mkThmOrUnsafeDef` for the Prop case (which
also handles the unsafe fallback correctly). The noncomputable check is
skipped for Prop-typed instances since theorems can freely reference
noncomputable constants.
Closes#13295🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR adds the shared infrastructure for arithmetic normalization in
`Sym.Arith/`,
laying the groundwork for both `Sym.simp`'s arith pre-simproc and the
eventual
unification of grind's `CommRing` module.
The key components:
- **`Types.lean`**: Classification structures (`Semiring`, `Ring`,
`CommRing`,
`CommSemiring`) stored in a `SymExtension`. These are the
classification-only
subset of grind's ring types — no solver state. Includes
`withExpThreshold` for
controlling exponent evaluation limits.
- **`EvalNum.lean`**: `evalNat?`/`evalInt?` for evaluating ground
Nat/Int
expressions in type classes (e.g., `IsCharP`), adapted from grind to
`SymM`.
- **`Classify.lean`**: Algebraic structure detection (CommRing > Ring >
CommSemiring > Semiring) with a single `typeClassify : PHashMap ExprPtr
ClassifyResult` cache.
Detects `IsCharP`, `NoNatZeroDivisors`, and `Field` instances.
- **Type classes**: `MonadCanon`, `MonadRing`/`MonadCommRing`,
`MonadSemiring`/`MonadCommSemiring`, `MonadGetVar`/`MonadMkVar` —
abstract over
the monad so the same code works in both `SymM` and grind's
`RingM`/`SemiringM`.
Grind's `MonadCanon` is deleted; grind's monads inherit it from `SymM`
via
`MonadLift`.
- **`Functions.lean`**: Cached function getters (`getAddFn`, `getMulFn`,
etc.)
generic over the type classes. Synthesizes instances, validates via
`isDefEqI`,
canonicalizes via `canonExpr`.
- **`Reify.lean`**: Converts Lean expressions into
`RingExpr`/`SemiringExpr` for
reflection-based normalization. Variable creation abstracted via
`MonadMkVar`.
- **`DenoteExpr.lean`**: Converts reified expressions back to Lean
`Expr`s.
Roundtrip tests confirm reify→denote produces definitionally equal
results.
- **`ToExpr.lean`**, **`VarRename.lean`**, **`Poly.lean`**: Moved from
`Grind.Arith.CommRing/` — pure utilities on `Grind.CommRing` types with
no
solver dependencies.
- **Tests**: Unit tests for classification (`Int` → commRing, `Nat` →
commSemiring,
`Rat` → commRing), `evalNat?`/`evalInt?`, exp threshold, and
reify-denote roundtrips.
**TODO**: use abstractions to implement `grind` ring module, and delete
code duplication.
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR marks any exposed (non-private) auxiliary match declaration as
`[implicit_reducible]`. This is essential when the outer declaration is
marked as `instance_reducible` — without it, reduction is blocked at the
match auxiliary. We do not inherit the attribute from the parent
declaration because match auxiliary declarations are reused across
definitions, and the reducibility setting of the parent can change
independently. This change prepares for implementing the TODO at
`ExprDefEq.lean:465`, which would otherwise cause too many failures
requiring manual `[implicit_reducible]` annotations on match
declarations whose names are not necessarily derived from the outer
function.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR extends the sym canonicalizer to apply reductions (projection,
match/ite/cond, Nat
arithmetic) in all positions, not just inside types. Previously, a value
`v` appearing in a
type `T(v)` could remain unreduced while `T(v)` was normalized, breaking
the invariant that
definitionally equal types are structurally identical after
canonicalization.
Changes:
- Remove `insideType` guards from `canonApp` and `canonProj`, so
reductions apply unconditionally
(eta reduction remains type-only, to preserve lambda structure for
`grind`)
- Add `canonInstDecCore` to handle `Decidable` instances in
`if-then-else` expressions, dispatching
`Grind.nestedDecidable` to `canonInstDec` and falling back silently for
other instances
- Add `report` parameter to `canonInstCore`/`canonInst'`/`canonInst` to
allow suppressing issue
reporting for propositional and decidable instances that cannot be
resynthesized (common with
`haveI`-provided instances that propagate into types through forward
dependencies)
- Update module documentation to reflect the new reduction scope and the
`haveI` reporting tradeoff
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR refactors instance canonicalization in the sym canonicalizer to
properly handle
\`Grind.nestedProof\` and \`Grind.nestedDecidable\` markers. Previously,
the canonicalizer
would report an issue when it failed to resynthesize propositional
instances that were
provided by \`grind\` itself or by the user via \`haveI\`. Now,
resynthesis failure gracefully
falls back to the original instance in value positions, while remaining
strict inside types.
Changes:
- Extract \`canonInstCore\` as the shared resynthesis + defEq-check
logic
- Add \`canonInstProp\` for \`Grind.nestedProof\`: canonicalize the
proposition, attempt resynthesis, fall back silently (proof irrelevance
means no defEq check needed)
- Add \`canonInstDec\`/\`canonInstDec'\` for \`Grind.nestedDecidable\`:
canonicalize the proposition, attempt resynthesis with defEq guard, fall
back silently
- Remove the separate \`cacheInsts\` cache in favor of the existing
type/value caches via \`withCaching\`
- Update module-level documentation
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR verifies the `String.dropWhile` and `String.takeWhile`
functions.
It also includes a refactor of the `PatternModel` class so that the
`not_matches_empty` condition is moved into a separate typeclass
`StrictPatternModel`. This allows string patterns to implement
`LawfulForwardPatternModel` unconditionally, which means that more of
the general theory about patterns directly applies to string patterns
without having to do a case distinction for empty strings.
This PR also includes a study of the `PatternModel` machinery given to
slices `s` and `t` such that `s.copy = t.copy`. From these results, we
deduce statements like `s.copy.startsWith pat = s.startsWith pat` (which
is far from obvious!).
This PR changes the counter-example accumulator in the match compiler
from
a `List` (built with cons, producing reverse order) to an `Array` (built
with push, preserving declaration order). Missing cases are now reported
in
the order constructors appear in the inductive type definition.
For example, given `inductive Enum | a | b | c | d`, missing cases `c`
and
`d` were previously shown as `d, c` and are now shown as `c, d`.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
privateConstantMap capacity was inflated by IR extraConstNames that are
only inserted into const2ModIdx. const2ModIdx capacity included
numPublicConsts even though public constants are never inserted into it.
This PR adds a `match.maxCounterExamples` option (default 5) to bound
the
number of "missing cases" counter-examples the match compiler generates.
When the match compiler runs out of alternatives for a variable, it
case-splits to explore missing cases. Previously, this would recursively
split all inductive-typed fields of each constructor, leading to
O(K^fields)
counter-examples for types with K constructors per field. For nested
incomplete matches on types like `Op w` (20 constructors with `Operand
w`
fields having 8 constructors each), this produced thousands of
counter-examples and took several seconds.
The fix checks the counter-example count in `isConstructorTransition`:
once
the limit is reached and there are no remaining alternatives, the match
compiler stops exploring further case splits. The error message notes
when
output has been truncated and names the option. The existing protection
against infinite recursion on recursive types is preserved.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR changes elaboration of structure instance notation when used in
patterns (e.g. `s matches { x := 1, y := [] }`) so that the structure's
default values are not used to elaborate the pattern. The motivation is
that default values frequently lead to surprisingly over-specific
patterns. It will now report "field missing" errors. The error can be
suppressed using `{ x := 1, .. }` ellipsis notation, which has the same
behavior as before. The pretty printer is also modified to stay in sync
with this feature. **Breaking change:** patterns using structure
instance notation may need missing fields or a `..` added, as
appropriate.
The rationale for the previous behavior is that with `..` you could
opt-in to not using default values, and now with this PR's behavior you
cannot opt-in. However, default values in structure instance patterns
are very likely to silently cause bugs. There are a couple examples in
this PR of unintentional default values in patterns in core Lean
(luckily these were not triggering bugs). With the new behavior, you can
now tell for sure whether every explicit field in a structure is being
matched explicitly or not, by the absence or presence of `..`.
Closes#10753
This PR adds support for marking options as deprecated. When a
deprecated option is used via `set_option`, a warning is emitted
(controlled by `linter.deprecated.options`).
An `OptionDeprecation` structure with a required `since` field and an
optional `text?` field is added to `OptionDecl`. Each `set_option`
elaborator (command, term, tactic, grind) calls `checkDeprecatedOption`
to emit warnings. The C++ `register_option` is updated to account for
the new field.
As a first use, `backward.eqns.nonrecursive` and
`backward.eqns.deepRecursiveSplit` are marked deprecated. Continues
earlier work done in #11096.
This PR adds test infrastructure and tests for tactic completion in
empty `by` blocks.
**Test runner improvements (`src/Lean/Server/Test/Runner.lean`):**
- Add `--⬑` marker variant that targets the column of `--` itself,
enabling column 0 tests (which `--^` cannot reach since `^` is always at
column 2+).
**New test file (`tests/server_interactive/completionEmptyBy.lean`):**
- Tests tactic completion in empty `by` blocks for both top-level `by`
and nested `by` (inside `id <| have := by`).
- Tests at various column positions on the line below `by`: indented
past `by`, at column 2, and at column 0.
- Tests on the `by` token itself (no completions expected).
- All positions below `by` currently offer tactic completions.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds support for let configuration options (`(eq := h)`,
`+nondep`, `+usedOnly`, `+zeta`) in `do` block `let` and `have`
declarations, matching the behavior available in term-level
`let`/`have`. Configuration options are rejected with `let mut` since
they are incompatible with mutable bindings. `+postponeValue` and
`+generalize` are also rejected in `do` blocks.
Follow-up to #13250 which added the parser support. Now that stage0 is
updated, this PR replaces the backward-compat index helpers with proper
quotation patterns and implements the actual `letConfig` elaboration.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR removes a FIXME in Sym-based mvcgen' concerning a hardcoded step
limit for grind simplification. I tested that this is no longer
necessary even at highest setting for the GetThrowSetGrind benchmark.
This PR extends Lean syntax for dotted function notation (`.f`) to add
support for explicit mode (`@.f`), explicit universes (`.f.{u,v}`), and
both simultaneously (`@.f.{u,v}`). This also includes a fix for a bug
involving overloaded functions, where it used to give erroneous
deprecation warnings about declarations that the function did not
elaborate to.
Closes#10984
This PR improves pretty printing of level metavariables: they now print
with a per-definition index rather than their per-module internal
identifiers. Furthermore, `+` is printed uniformly in level expressions
with surrounding spaces. **Breaking metaprogramming change:** level
pretty printing should use `delabLevel` or `MessageData.ofLevel`;
functions such as `format` or `toString` do not have access to the
indices, since they are stored in the current metacontext. Absent index
information, metavariables print with the raw internal identifier as
`?_mvar.nnn`. **Note:** The heartbeat counter also increases quicker due
to counting allocations that record level metavariable indices. In some
tests we needed to increase `maxHeartbeats` by 20–50% to compensate,
without a corresponding slowdown.
This PR fixes a panic when compiling mutually recursive definitions that
use `casesOn` on indexed inductive types (e.g. `Vect`). The
`splitMatchOrCasesOn` function in `WF.Unfold` asserted
`matcherInfo.numDiscrs = 1`, but for indexed types the casesOn recursor
has multiple discriminants (indices + major premise). The fix uses the
last discriminant (the major premise) and lets the `cases` tactic handle
index discriminants automatically.
Closes#13015
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a `deprecated_module` command that marks the current module
as deprecated. When another module imports a deprecated module, a
warning is emitted during elaboration suggesting replacement imports.
Example usage:
```lean
deprecated_module "use NewModule instead" (since := "2026-03-30")
```
The warning message is optional but recommended. The `since` parameter
is required. Warnings can be disabled, by setting
`linter.deprecated.module` option to false in the command line. Because
the check happens when importing , using `set_option
linter.deprecated.module` in the source file won't affect the warnings.
Instead, a whole file can be marked not to display depreciation
warnings, by putting a comment `deprecated_module: ignore` next to
`module` keyword. Similarly, individual keywords can be silenced.
A `#show_deprecated_modules` command is also provided for inspecting
which modules in the current environment are deprecated.
`linter.deprecated.module` has no effect on this command, and hence one
can view deprecated modules, even when having warnings silenced.
This PR fixes `FirstTokens.seq (.optTokens s) .unknown` to return
`.unknown`. This occurs e.g. when an optional (with first tokens
`.optTokens s`) is followed by a parser category (with first tokens
`.unknown`). Previously `FirstTokens.seq` returned `.optTokens s`,
ignoring the fact that the optional may be empty and then the parser
category may have any first token. The correct behavior here is to
return `.unknown`, which indicates that the first token may be anything.
Closes#13203
This PR adds a `deprecated_syntax` command that marks syntax kinds as
deprecated. When deprecated syntax is elaborated (in terms, tactics, or
commands), a linter warning is emitted. The warning is also emitted
during quotation precheck when a macro definition uses deprecated syntax
in its expansion.
The `deprecated_syntax` command takes a syntax node kind, an optional
message, and a `(since := "...")` clause. Deprecation warnings correctly
attribute the warning to macro call sites when the deprecated syntax is
produced by macro expansion, including through nested macro chains.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR adds an `unlock_limits` command that sets `maxHeartbeats`,
`maxRecDepth`, and `synthInstance.maxHeartbeats` to 0, disabling all
core resource limits. Also makes `maxRecDepth 0` mean "no limit"
(matching the existing behavior of `maxHeartbeats 0`).
This PR moves `hasAssignableMVar`, `hasAssignableLevelMVar`, and
`isLevelMVarAssignable` from `MetavarContext.lean` to a new
`Lean.Meta.HasAssignableMVar` module, changing them from generic `[Monad
m] [MonadMCtx m]` functions to `MetaM` functions. This enables adding
`checkSystem` calls in the recursive traversal, which ensures
cancellation and heartbeat checks happen during what can be a very
expensive computation.
All callers of these functions were already in `MetaM`, so this change
is safe. The motivating case is the `4595_slowdown.lean` test, where
`hasAssignableMVar` (with `PersistentHashMap.find?` lookups on
`mctx.lDepth`) was the dominant CPU cost during elaboration of category
theory definitions. Without `checkSystem` calls, cancellation requests
could be delayed by over 2 seconds.
The test file `4595_slowdown.lean` gets a slightly increased
`maxHeartbeats` limit because `checkSystem` now detects heartbeat
exhaustion mid-traversal rather than after the function returns.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR replaces eager let-expression zeta-reduction in the sym-based
mvcgen with on-demand unfolding that mirrors the production mvcgen's
behavior.
Previously, all let-expressions in the program head were immediately
zeta-reduced. Now, let-expressions are hoisted to the top of the goal
target, and the value is only inlined if it is duplicable (literals,
fvars, consts, `OfNat.ofNat`). Complex values are introduced into the
local context via `introsSimp`, preserving SymM's maximal sharing
invariants, and unfolded on demand when the fvar later appears as the
program head.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR extends the `missingDocs` linter to detect and warn about empty
doc strings (e.g. `/---/` or `/-- -/`), in addition to missing doc
strings. Previously, an empty doc comment would silence the linter even
though it provides no documentation value. Now empty doc strings produce
a distinct "empty doc string for ..." warning, while `@[inherit_doc]`
still suppresses warnings as before.
This PR switches the mvcgen worklist from BFS (queue) to DFS (stack)
ordering for subgoal processing.
With the new do elaborator, `if`-without-`else` generates asymmetric
bind depth between branches (`pure () >>= cont` is optimized to just
`cont` in the else branch). This caused BFS-based VC numbering to depend
on elaborator internals, swapping vc10/vc11 in test cases. DFS ordering
follows the syntactic program structure more naturally and is robust to
such bind-depth asymmetries.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes the handling of anonymous dependent `if` (`if _ : cond
then ... else ...`) inside `do` blocks when using the new do elaborator.
The `_%$tk` binder pattern was incorrectly quoted as `$(⟨tk⟩):hole` in
the generated `dite` syntax, causing "elaboration function for
`termDepIfThenElse` has not been implemented" errors. The fix quotes it
correctly as `_%$tk`.
A test case is added to verify both anonymous (`if _ : ...`) and named
(`if h : ...`) dependent `if` work in do blocks.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a `@[deprecated_arg]` attribute that marks individual
function parameters as deprecated. When a caller uses the old parameter
name, the elaborator emits a deprecation warning with a code action hint
to rename or delete the argument, and silently forwards the value to the
correct binder.
Supported forms:
- `@[deprecated_arg old new (since := "...")]` — renamed parameter,
warns and forwards
- `@[deprecated_arg old new "reason" (since := "...")]` — with custom
message
- `@[deprecated_arg removed (since := "...")]` — removed parameter,
errors with delete hint
- `@[deprecated_arg removed "reason" (since := "...")]` — removed with
custom message
A warning is emitted if `(since := "...")` is omitted.
When a parameter is deprecated without a replacement, the elaborator
treats it as no longer present: using it as a named argument produces an
error. Note that positional uses of deprecated arguments are not checked
— if a function's arity changed, the caller will simply get a "function
expected" error.
The `linter.deprecated.arg` option (default `true`) controls behavior:
when enabled, renamed args produce warnings and removed args produce
specific deprecation errors with code action hints; when disabled, both
fall through to the standard "invalid argument name" error. This lets
library authors phase out old parameter names without breaking
downstream code immediately.
Example (renamed parameter):
```lean
@[deprecated_arg old new (since := "2026-03-18")]
def f (new : Nat) : Nat := new
/--
warning: parameter `old` of `f` has been deprecated, use `new` instead
Hint: Rename this argument:
o̵l̵d̵n̲e̲w̲
---
info: f 42 : Nat
-/
#guard_msgs in
#check f (old := 42)
```
Example (removed parameter):
```lean
@[deprecated_arg removed (since := "2026-03-18")]
def g (x : Nat) : Nat := x
/--
error: parameter `removed` of `g` has been deprecated
Hint: Delete this argument:
(̵r̵e̵m̵o̵v̵e̵d̵ ̵:̵=̵ ̵4̵2̵)̵
-/
#guard_msgs in
#check g (removed := 42)
```
This PR adds `simplifying_assumptions [Nat.add_assoc]` to the
`vcgen_get_throw_set_grind` benchmark, recovering hypothesis
simplification lost in a54eafb ("refactor: decouple solve from grind").
That refactor introduced `PreTac.processHypotheses` which wraps
`simpNewHyps`, but the call sites in `work` and `main` call
`Grind.processHypotheses` directly, leaving `simpNewHyps` as dead code.
Without it, long `s + 1 + … + 1` chains are never collapsed, causing an
asymptotic slowdown visible by a factor of 2 at n=150 (largest radar
input size).
Benchmark results (VCGen time in ms):
| n | Before | After | Speedup |
|---|--------|-------|---------|
| 50 | 222 | 186 | 1.2× |
| 100 | 391 | 251 | 1.6× |
| 150 | 647 | 329 | 2.0× |
| 200 | 995 | 415 | 2.4× |
| 300 | 1894 | 589 | 3.2× |
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds `@[expose]` to `Lean.Grind.abstractFn` and
`Lean.Grind.simpMatchDiscrsOnly` so that the kernel can unfold them when
type-checking `grind`-produced proofs inside `module` blocks. Other
similar gadgets (`nestedDecidable`, `PreMatchCond`, `alreadyNorm`) were
already exposed; these two were simply missed.
Closes https://github.com/leanprover/lean4/issues/13167
This PR introduces the `Body` type class, the `ChunkStream` and `Full`
types that are used to represent streaming bodies of Requests and
Responses.
This contains the same code as #10478, divided into separate pieces to
facilitate easier review.
The pieces of this feature are:
- Core data structures: #12126
- Headers: #12127
- URI: #12128
- Body: #12144
- H1: #12146
- Server: #12151
- Client:
---------
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
This PR replaces the `grind` canonicalizer with a new type-directed
normalizer (`Sym.canon`) that goes inside binders and applies targeted
reductions in type positions, eliminating the O(n^2) `isDefEq`-based
approach.
The old canonicalizer maintained a map from `(function,
argument_position)` to previously seen arguments, iterating the list and
calling `isDefEq` for each new argument. This produced performance
problems in some goal. For example, for a goal containing `n` numeric
literals, it would produce O(n^2) `isDefEq` comparisons.
The new canonicalizer normalizes types directly:
- **Instances**: re-synthesized via `synthInstance` with the type
normalized first, so `OfNat (Fin (2+1)) 0` and `OfNat (Fin 3) 0` produce
the same instance.
- **Types**: normalized with targeted reductions — eta, projection,
match/ite/cond, and Nat arithmetic (`n.succ + 1` → `n + 2`, `2 + 1` →
`3`).
- **Values**: traversed but not reduced, preserving lambdas for grind's
beta module.
The canonicalizer enters binders (the old one did not), using separate
caches for type-level and value-level contexts. Propositions are not
normalized to avoid interfering with grind's proposition handling.
Move `SynthInstance` from `Grind` to `Sym` since the canonicalizer now
lives in `Sym` and needs instance synthesis. The `Grind` namespace
re-exports the key functions.
Add `no_index` annotations to `val_addNat` and `val_castAdd` patterns in
`Fin/Lemmas.lean` — arithmetic in type positions is now normalized, so
patterns must not rely on the un-normalized form for e-matching
indexing.
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
