This PR makes the elaborator reject `@[foo]` when the module that
registers `foo` is not visibly imported into the current file but merely
loaded as IR. Previously such uses silently elaborated but led to
divergence of cmdline and server behavior and caused `lake shake --fix`
to flip-flop on successive runs (#13599).
This PR renames the `lake lint --clippy` flag to `--extra` and broadens
its scope so that it runs the default builtin linters together with the
non-default ones, instead of only the non-default ones. Use `--lint-all`
to additionally enable any other off-by-default linters.
The matching internal names follow: the namespace `Lean.Linter.Clippy`
becomes `Lean.Linter.Extra`, the option `linter.clippy` becomes
`linter.extra`, and the env-linter attribute form `@[builtin_env_linter
clippy]` becomes `@[builtin_env_linter extra]`.
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR adds the ability to specify a name for the initialization
function of a Lean plugin on load.
* The `Lean.loadPlugin` API has gained a `initFn?` argument that
defaults to `none`. When `none`, the initialization function name will
be inferred from the shared library's name (as before).
* The CLI `--plugin` option can now have a initialization function
specified via `--plugin=path:initFn`.
* The `--setup` JSON configuration now also accepts`{"path": ...,
"initFn": ...}` for plugins.
This PR fixes the termination checker reporting errors at the wrong
recursive call site when a function contains structurally-identical
recursive calls at different source locations.
The `_recApp` `MData` attached to recursive applications carried the
attached `Syntax`, but two structurally-equal `MData` wrappers could be
merged by hashconsing/simplification, so the syntax of the first call
ended up associated with both call sites. We now also store the source
byte position as `_recAppPos`, which keeps the wrappers distinct.
Closes#13444.
This PR makes radar use the LLVM that we actually ship to users (stored
at https://github.com/leanprover/lean-llvm). In doing so it also makes
the lake build compatible with lean-llvm, allowing us to do potential
release builds with lake in the future.
This PR brings the Sym-based `mvcgen'` to feature parity with `mvcgen`;
the only remaining gap is `+jp` (join-point handling).
The slight benchmark regressions are due to simplifying VCs out of
`SPred` form, hitting hardest on cases with linearly many VCs like
`PurePreCond`. The ~10% vcgen slowdown is worth it for the cleaner
user-visible VCs.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a trace event emitted whenever a `dsimp` (or rfl-only
`simp`) rewrite fires
because of a `[backward_defeq]`-tagged theorem (i.e., one that would not
have applied without `set_option backward.defeqAttrib.useBackward
true`).
Useful for finding where downstream code is silently relying on the
backwards escape hatch — a precursor to either re-tagging the lemma as
`[defeq]` or restructuring the proof so it works under the strict
defeq rules.
This PR fixes a `Sym.simp` panic ("unexpected kernel projection term
during simplification") that triggered when matcher iota-reduction
exposed kernel `Expr.proj` terms via struct-eta. For example, a `do`
block with a `for` loop whose state is a tuple, where `Sym.simp`
unfolds the equational lemma and then descends into a destructuring
match.
This PR fixes a Lake issue where the IR for a `meta import`'s transitive
imports was not included in the import artifacts Lake provided to Lean
(e.g., via `--setup`). When using the Lake artifact cache, this could
produce "missing data file" errors due to absent IR.
Closes#13419
---------
Co-authored-by: Claude Code <noreply@anthropic.com>
This PR fixes a `grind` congruence-table invariant violation that could
panic
when an `ite` branch was internalized lazily (after the condition became
`True`
or `False`) and that branch's equivalence class was later merged with
another.
`Internalize.lean` has a special case for `ite` that internalizes only
the
condition; the `then`/`else` branches are skipped and only internalized
later
on demand by `propagateIte`. The on-demand path (`applyCongrFun`) called
`internalize` for the branch but never called `registerParent` to add
the
parent `ite` to the branch's parent set in the e-graph. Subsequent
merges of
the branch's equivalence class then skipped re-hashing the `ite` in the
congruence table, leaving an orphan entry whose `congr` chain no longer
matched
the table's representative.
The fix adds the explicit `registerParent e rhs` that the standard
`for arg in args` loop in `Internalize.lean` would have made for an
ordinary
application argument; we are simply mirroring that pattern lazily. The
same
helper is reused by `propagateDIte`, but with parent registration
disabled
(controlled by a new `ite : Bool` parameter): for `dite` the `rhs`
propagated
upwards is a *constructed* reduction (built via `mkApp` from `e`'s
children,
possibly post-`preprocess`), not a structural argument of `e`, so
registering
`e` as its parent would be incorrect. The lambda branches of a `dite`
are
already eagerly internalized as parents of `e` by `Internalize.lean`, so
this
case does not need the fix.
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR fixes a `grind` internal error triggered when `cast` (or
`Eq.rec`, `Eq.ndrec`, `Eq.recOn`) is applied to an argument that has not
yet been internalized. `pushCastHEqs` was emitting `e ≍ a` before
internalizing the args of `e`, so the `rhs` of the heq had no enode and
the debug sanity check tripped. The call now runs after the args are
internalized.
This PR adds infrastructure to help diagnose cases where tactics like
`unfold`
leave the goal in a state that is type-correct only at `.default`
transparency,
causing `rw`/`simp` to fail at `.instances` transparency.
Changes:
- Add a `transparency` parameter to `Meta.check` (defaults to `.all`)
- Add `withInstancesTypeCheckNote` which appends a
lazy note to tactic errors when the target is not type-correct at
`.instances`
- Wrap `rw`, `simp`, `dsimp`, and `simp_all` at the Elab level
- Add opt-in `linter.tacticCheckInstances` that proactively checks every
tactic goal and reports semireducible defs that should be marked
`@[implicit_reducible]`, using diagnostic counter diffing between
`.default`
and `.instances` checks
This PR extends the procedure behind `inferInstanceAs`/`def ...
deriving` to continue recursion through the class graph even when a
(local) instance to wrap was found in order to re-use already-wrapped
instance of subclasses.
This PR ensures consistent metavariable behavior between Verso
docstrings and Verso moduledocs by sharing more code between their
elaborators. It also improves the error message when a metavariable leak
is prevented.
This PR disables model-based theory combination (`mbtc`) in `grind`'s
`NoopConfig`, which is the base configuration used by the derived
tactics `lia`, `linarith`, `cutsat`, `order`, and `ring`. Without this
fix, these tactics could engage in wasteful reasoning via theory
combination, causing them to run for a long time (or hit the
deterministic timeout) on problems they are not designed to solve. With
this fix, these tactics fail quickly on out-of-scope problems, as
expected.
Closes#13573.
This PR makes `lia` (and `grind`'s arithmetic case-split heuristic)
recognize
implications whose antecedent is an `And` or `Or` of arithmetic
predicates as
relevant case-split candidates. Previously, `Arith.isRelevantPred` only
matched
`Not`, `LE`, `LT`, `Eq`, and `Dvd`. With `splitImp := false` (the
default),
implications `p → q` are added as split candidates only when `p` is
arith-relevant, so a hypothesis like `(b ≤ e ∧ e < b + c → a ≤ e ∧ e < a
+ d)`
was never registered as a candidate. cutsat/lia would then find a
satisfying
assignment for the constraints it had been told about, but that
assignment
would not necessarily satisfy the original implication, yielding the bad
counterexample reported in #13575.
After this change, `isRelevantPred` recurses through `And` and `Or`
(returning
`true` if either operand is relevant), so the implication is split,
modus
ponens fires in the True branch, and cutsat/lia closes the False branch
via the
disjunction over negated atoms.
Closes#13575.
This PR adds a `ringMaxDegree` configuration option (default `1024`)
that bounds the maximum degree of polynomials processed by the `grind`
ring solver. Equality constraints whose polynomial exceeds this
threshold are discarded (with an issue reported once per goal),
preventing pathological degree explosion on inputs such as `r ^ (2 ^ 250
- 1)`.
This PR also introduces `Poly.simpM?`, a monadic version of `Poly.simp?`
built on the existing safe arithmetic primitives (`mulMonM`, `combineM`,
`mulConstM`) in `Grind.Arith.CommRing.SafePoly`. The previous
reflection-oriented `Poly.simp?` in `Sym.Arith.Poly` lacked the abort
mechanisms needed during proof search, so the simplification path used
by `EqCnstr` now goes through the safe variant. A regression test
`tests/elab/grind_ring_degree_explosion.lean` ensures `grind` fails
quickly on high-degree problems.
This PR gives the `specialize` tactic the ability to instantiate
universal quantifiers other than the first using `specialize h (y := v)`
syntax. It also fixes an issue where `MVarId.assertAfter` did not record
variable alias information, and an issue where `MVarId.replace` and
`MVarId.replaceLocalDecl` did not take metavariables into account when
calculating dependencies. Additionally it fixes some uninstantiated
metavariables bugs, including one in the Infoview tactic state
hypothesis diff.
The `specialize` tactic now uses `Lean.MVarId.replace` to simplify the
implementation, and as a consequence it tries to keep the specialized
hypothesis close to its original spot in the local context.
Additional metaprogramming API:
- `Lean.Expr.getLambdaBody` to accompany `Lean.Expr.getNumHeadLambdas`
- `Lean.LocalContext.setType`, `Lean.MetavarContext.setFVarType`,
`Lean.MVarId.setFVarType`
- `Lean.MVarId.assertAfter'` to assert a new hypothesis as early as
possibly in the context where it is well-formed, as a frontend to
`Lean.MVarId.assertAfter`, which assumes the new hypothesis is
well-formed
Breaking change: metaprograms cannot assume that `MVarId`s change if
metavariables are assigned. For example, the `change` tactic will no
longer change `MVarId`s if the only effect is incidental metavariable
assignments.
Mathlib impact: this revealed many `dsimp`s that did nothing and could
be deleted.
Closes#9893
This PR fixes parallel tactic combinators (`attempt_all_par`,
`first_par`) leaking their subtasks when the server cancels elaboration
on re-elaboration. Subtasks spawned via `CoreM.asTask` (and its
`MetaM`/`TermElabM`/`TacticM` variants) get a fresh `IO.CancelToken`,
which previously had no link to the parent token; `cancelRec` would set
the command-level token but the children kept running.
The fix is one line in `CoreM.asTask`: when a parent token is in scope,
register `cancelToken.set` as an `onSet` callback on the parent.
Server-level cancellation now flows down to every parallel subtask, and
`Core.checkInterrupted` inside the child sees the token set as expected.
Fixes#13300.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR upstreams `unnecessarySeqFocus` linter from batteries to core
lean as a "clippy" linter - i.e. one that is disabled by default and
executed by `lake lint --clippy`.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>
This PR adds regression tests for `do`-notation issues that the new
elaborator fixes:
* `tests/elab/doNotation7.lean` collects reproducers for #2663, #2676,
#3126, #5607, #6426, and #8119.
* `tests/elab/12229.lean` covers the `logInfo` and `Std.TreeMap`
reproducers from #12229.
This PR upstreams `dupNamespace` linter from batteries to work with new
core environment linting framework, as a "clippy" linter - i.e. one that
is not enabled by default.
Stacked on top of #13513.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>
This PR adds the option `grind.ematch.diagnostics`, which tracks how
E-matching theorem instances depend on each other. When enabled, `grind`
records, for every new theorem instance, the set of previous instances
whose generated terms participated in the match. This produces a
hyper-graph `{thm_1, ..., thm_n} => thm` describing the provenance of
each instantiation.
The hyper-graph is stored in `Grind.Result` so downstream tooling can
inspect it. The trace class `trace.grind.ematch.diagnostics.compact`
prints a compact textual view of the hyper-graph, restricted to
constant-name origins. Example output:
```
[grind.ematch.diagnostics.compact] ✅️ instances
[inst] [] => th1
[inst] [th1] => th3
[inst] [th1] => th2
[inst] [th2, th3] => th4
[inst] [th4] => th5
```
The implementation stores an `ematchDiagSource` field on each `ENode`
and threads a `withEmatchDiagSource` reader through fact assertion so
that newly internalized terms inherit the origin of the instance that
produced them. During E-matching, `Choice` collects the sources of every
matched argument, and the resulting set becomes the predecessor set of
the new instance.
This PR addresses two review points on `IO.CancelToken`:
* `set` now resolves the underlying promise *before* writing the `Bool`
fast-path flag, so observing `isSet = true` implies any synchronously
chained `onSet` callback has already run. The previous order (flag
first,
then resolve) was a subtle footgun: code seeing `isSet = true` could not
rely on the cancellation task having fired.
* The underlying promise and the task it produces are kept private. The
prior `task : Task (Option Unit)` accessor is removed; consumers should
use `onSet` to react to cancellation. A comment on the structure records
that re-exposing the task in the future requires re-auditing the order
in `set` for races between the promise and the `Bool` flag.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
This PR fixes a bug in `propagateBetaEqs` (in
`Lean.Meta.Tactic.Grind.Beta`)
where new equalities/terms introduced by beta reduction were added to
the goal
without checking the generation threshold. The generation of the new
fact
is the maximum generation of the lambda, the function `f`, and its
arguments, plus one. Without the threshold check, beta reduction can
cascade indefinitely on self-similar lambdas such as
`(fun b => f (b + 1)) = fun b => f b`, which kept producing
`f n = f (n + 1)` for every `n`. The fix aggregates argument generations
before the threshold check and bails out when the resulting generation
reaches `maxGeneration`.
This PR moves `IO.CancelToken` from `Init.System.IO` to its own file
`Init.System.CancelToken`, backed by `IO.Promise Unit` instead of
`IO.Ref Bool`. This enables non-polling cancellation propagation: the
token's underlying promise can be used directly with `IO.waitAny`, and
callbacks can be registered to fire when cancellation is requested.
The structure carries both the promise *and* a plain `IO.Ref Bool` flag,
set in lockstep by `set`. `isSet` reads the flag directly (used on hot
paths like `Core.checkInterrupted`); `task`/`onSet` go through the
promise. The avoids a ~0.4% regression that a pure-promise
representation introduced.
API additions:
- `CancelToken.task : Task (Option Unit)`. Returns the underlying
promise's `result?` task directly — the same task object on every call,
so further `Task.map`/`BaseIO.bindTask` dependencies can be safely
attached. Resolves with `some ()` when `set` is called, or `none` if the
token is dropped without ever being set.
- `CancelToken.onSet : BaseIO Unit → BaseIO Unit`. Registers a callback
that runs synchronously on the cancelling thread when `set` is called
(or immediately if the token is already set). Implemented via
`BaseIO.chainTask` on `result?`, so no fresh `Task.map` per call and no
GC hazard.
Runtime cleanup:
- Add `LEAN_TASK_STATE_{WAITING,RUNNING,FINISHED}` constants in `lean.h`
matching `IO.TaskState`.
- Factor `lean::promise_is_resolved` inline in `object.h`, replacing
three open-coded `lean_io_get_task_state_core(...) == 2` checks (in
`interrupt.cpp`, `uv/timer.cpp`, `uv/signal.cpp`).
- Drop the manual `inc_ref(g_cancel_tk)` in `check_interrupted`; the
token is owned by the enclosing `scope_cancel_tk` for the duration of
the call (documented).
- Replace the bare `lean_always_assert(g_task_manager)` in
`lean_promise_new` with an explicit `lean_internal_panic` carrying a
message that names `Promise.new`, identifies the typical trigger
(`initialize` blocks, transitively via `IO.CancelToken.new`), and
recommends lazy construction. Without this, users got an opaque "LEAN
ASSERTION VIOLATION ... Condition: g_task_manager" with no actionable
hint.
Behavioural notes documented inline:
- `new` cannot be called from `initialize` blocks (task manager not
running yet); construct lazily.
- `task` documents the dropped-promise case (`none`) and steers callers
to `onSet` for callback chaining.
A consumer of `onSet` for parent → child cancel-token propagation in
parallel tactic combinators is in #13428 (fixes#13300).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR extends `lake lint --builtin-lint` to also support text linters
(i.e. those using `logLint`/`logLintIf`), in addition to the environment
linters added in #13431. Text-linter warnings emitted during the build
are persisted into each module's `.olean` via a new
`Lean.Linter.lintLogExt` environment extension; `lake lint` re-runs the
build for the target modules and reads the entries back, reporting them
alongside the environment linter output.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>
This PR adds a `try? => tac` syntax that runs `evalSuggest` directly on
a given tactic, useful for testing the `try?` machinery in isolation. It
also adds a server_interactive test (`cancellation_par.lean`) that
demonstrates a cancellation bug with parallel tactic combinators.
The test contrasts three combinators:
- **`first`** (sequential): cancellation works correctly — the tactic
runs on the main elaboration thread and shares its cancel token.
- **`attempt_all_par`** (parallel): cancellation is broken — the subtask
spawned via `asTask` gets a fresh cancel token that is never set on
re-elaboration.
- **`first_par`** (parallel): same bug as `attempt_all_par`.
The test uses a `check_cancel <label>` helper tactic that detects leaked
cancel tokens without any timing dependency: the second invocation (from
re-elaboration) signals the first, which then checks whether its cancel
token was set.
Related issue: #13300
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR replaces the catch-all "unsupported pattern in syntax match"
error that the new `do` elaborator produces for typical pattern mistakes
(#2215, #8304, #10393) with the proper diagnostics from the regular
pattern-var collector (e.g. "Invalid pattern: Expected a constructor or
constant marked with `[match_pattern]`", "ambiguous pattern, use fully
qualified name"), pointing at the offending pattern.
`getPatternVarsEx` / `getPatternsVarsEx` in `Lean.Elab.Do` now try the
syntax-quotation collector first (cheaply handling identifiers, holes,
and antiquotations) and fall back to the regular pattern-var collector
for everything else. When both fail, the regular collector's error wins
via `<|>` semantics.
The legacy `do` elaborator is intentionally left untouched, so the
existing `tests/elab/doSyntaxPatternError.lean` guards (which capture
the cryptic messages produced under legacy default) are unchanged. They
will need updating when the new `do` elaborator becomes default.
Fixes#2215, #8304, and #10393 for the new `do` elaborator.
This PR adds a `linter.redundantExpose` option (default `true`) that
warns when `@[expose]` or `@[no_expose]` attributes have no effect:
- `@[expose]` on `abbrev` (always exposed) or non-Prop `instance`
(always exposed)
- `@[expose]` on a `def` inside an `@[expose] section` (already exposed
by the section)
- `@[expose]`/`@[no_expose]` in a non-`module` file (no module system)
- `@[no_expose]` on a declaration that wouldn't be exposed by default
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR introduces stricter inference for the `@[defeq]` attribute and a
companion `@[backward_defeq]` attribute that preserves the pre-PR
behavior
as an opt-in.
### What changed
* `@[defeq]` is now inferred only when the equation holds at
`.instances` transparency (the transparency `dsimp` operates at).
* `@[backward_defeq]` is the old set: every theorem whose `rfl` proof
the legacy inference would have accepted is tagged `@[backward_defeq]`,
so `defeq ⊆ backward_defeq` holds by construction.
* The option `backward.defeqAttrib.useBackward` (default `false`) makes
`dsimp` also use `@[backward_defeq]` theorems, restoring the pre-PR
behavior for a specific proof or file.
* The option is eqn-affecting: its value at the point of a function's
definition is recorded so that the equation lemmas later generated for
that function use the same value, regardless of the ambient option at
the use site.
### Mathlib adaption
A companion adaption branch (`lean-pr-testing-backward-defeq-attrib` on
mathlib4) builds cleanly against this PR and passes `lake test` without
warnings. Most adaption changes are scoped
`set_option backward.defeqAttrib.useBackward true in` additions on the
failing declarations; a small number of files needed proof-level edits
where the stored form of a `dsimp%`/`@[reassoc]`/`@[elementwise]`
/`@[simps]`/`@[to_app]`-generated lemma had drifted under the stricter
regime.
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR generalizes the `while` syntax in `do` blocks so that the
condition can be any `doIfCond`, the same condition form already
accepted by `if`. As a result, `while let pat := e do …` and `while let
pat ← e do …` are now supported in addition to `while cond do …` and
`while h : cond do …`. The previously separate `doWhile` and `doWhileH`
parsers and their accompanying macros are unified into a single
`doWhile` parser whose macro delegates to the existing `doIf`
desugaring.
This PR notifies satellite solvers about asserted equalities `lhs = rhs`
even though `lhs = rhs` is not internalized in the E-graph (an existing
optimization). The notification lets solvers that do not inspect
equivalence classes (such as the homomorphism extension) react to
asserted equalities directly. It fires before the equivalence-class
merge so that solvers that mark `lhs` and `rhs` as their internal terms
have them registered before `Solvers.mergeTerms` fires `processNewEq`.
`cutsat` opts out of the notification when the equality has not been
internalized, since it already handles equalities through its `newEq`
handler. The homomorphism demo opts in by forcing `e` to be
internalized, enabling its rewrite rules to apply to asserted equalities
(e.g., `add b b = b` rewrites via `a = b ↔ toInt a = toInt b`).
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR allows tactic macros and elaborators to opt out of automatic
fallback to previous macros/elabs on failure. `throwUnsupportedSyntax`
is unaffected.
This PR removes the Makefile-based Lake test runner and replaces it with
`run_test.sh` and `run_clean.sh`. These are still not designed for use
with the `with_*.sh` runners, but this a step closer to that
eventuality.
It also adds a line to `CLAUDE.md` informing Claude how to build and run
a single Lake test.
This PR replaces the transparency bump from `.reducible` to `.instances`
in `whnfMatcher` with an explicit allowlist in `canUnfoldAtMatcher`.
Previously, `whnfMatcher` would unfold all `implicitReducible`
definitions and all `fromClass` projections when reducing match
discriminants. This made it impossible to mark definitions as
`implicit_reducible` without silently affecting match reduction
behavior.
The new `canUnfoldAtMatcher` delegates to `canUnfoldDefault` first
(respecting the ambient transparency), then allows unfolding of
`match_pattern`-attributed definitions, and finally checks an explicit
allowlist:
- `OfNat.ofNat` — numeric literals in match discriminants
- `NatCast.natCast` — `↑m` coercions (pervasive in Int proofs)
- `Zero.zero`, `One.one` — `0`/`1` class projections in match
discriminants
- `Fin.ofNat`, `HMod.hMod`, `Mod.mod` — Fin literal reduction
- `decEq`, `Nat.decEq` — decidable equality
- `Char.ofNat`, `Char.ofNatAux` — character literals
- `String.decEq`, `List.hasDecEq` — string/list equality
- `UInt{8,16,32,64}.{ofNat,decEq}` — unsigned integer literals and
equality
The key change is removing the blanket `implicitReducible` and
`fromClass` checks, so that marking definitions as `implicit_reducible`
no longer silently affects match reduction.
Additionally, `reduceMatcher?` and `reduceRecMatcher?` now call
`consumeMData` on their input to handle mdata-wrapped matcher
expressions.
Mathlib adaptation: the removal of the `fromClass` projection check
means class projections like `CategoryStruct.comp`, `CategoryStruct.id`,
`Min.min` etc. are no longer auto-unfolded in match discriminants.
Affected proofs add these projections explicitly to `simp`/`dsimp`
calls.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR appends `unreachable!` to the expansion of `break`-less `repeat`
when the expected result type does not unify with `PUnit`. The
continuation then has a polymorphic value, so the enclosing do block's
result type is inferred without a user-written filler, and `ControlInfo`
for break-less `repeat` can report `noFallthrough` honestly — dead-code
warnings on subsequent elements are now actionable.
Co-authored-by: Rob23oba <robin.arnez@web.de>
This PR exposes the `Pure.pure` / `Bind.bind` applications emitted by
the `do` elaborator as pluggable closures, so external surface syntaxes
(e.g. an `ido` notation for indexed monads) can reuse the full `do`
machinery while emitting alternate constants.
`Context` carries a new `DoOps` record (wrapped via an opaque `DoOpsRef`
to break the cycle with `DoElabM`) with `mkPureApp`, `mkBindApp`, and
`isPureApp?` fields. `mkPureApp` and `mkBindApp` become thin
dispatchers; the original bodies move to `DoOps.default`. `isPureApp?`
returns the pure value as an `Expr` rather than a `Bool`, so overrides
aren't locked into `Pure.pure`'s 4-argument layout. A new `elabDoWith`
entry point takes a `DoOps` plus a `doSeq`; `elabDo` is now `elabDoWith
.default` applied to a matched ``(do $doSeq)``.
Control-flow features (`mut`, `return`, `break`, `continue`, `for`) and
the transformer stack (`StateT`, `OptionT`, `ExceptT`, `EarlyReturnT`,
`BreakT`, `ContinueT`) remain hard-coded to `Monad`; generalising them
is deferred to a follow-up. A new
`tests/elab/doNotationPluggableOps.lean` registers an Atkey-style
indexed monad and an `ido` surface syntax that drives `elabDoWith`,
covering the forms of `do` that are supported under the minimal scope.
