feat: add the nondep field of Expr.letE to the C++ data model
#8751
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This PR adds the `nonDep` field of `Expr.letE` to the C++ data model. Previously this was unused, and in followup PRs the elaborator will use it to encode `have` expressions (non-dependent `let`s). The kernel does not verify that `nonDep` is correctly applied during typechecking. Breaking change: now `Expr.updateLet!` is `Expr.updateLetE!`. This PR also fixes a bug in `Expr.letFun?` and `Expr.letFunAppArgs?` when the body is not a lambda. In any case, these functions will be removed once the `Expr.letE (nonDep := true)` encoding of `have` expressions is complete.
github-actions
bot
added
the
toolchain-available
Collaborator
|
Mathlib CI status (docs):
|
Rob23oba
reviewed
Jun 12, 2025
zwarich
reviewed
Jun 12, 2025
src/kernel/expr.cpp
Outdated
| } | ||
|
|
||
| extern "C" uint8 lean_expr_isHave(object * e); | ||
| bool let_nonDep_core(expr const & e) { |
Contributor
There was a problem hiding this comment.
Similarly to lean_expr_isHave making more sense as lean_expr_is_have, I think let_nonDep_core makes more sense as let_non_dep_core, and similarly for other uses of non_dep. The camel case really sticks out like a sore thumb (hump?) in the C++ code.
Collaborator
Author
There was a problem hiding this comment.
Given that nondependent is a word, I went with let_nondep and let_nondep_core. Any objection to that? (I might switch nonDep to nondep in Lean later.)
Contributor
There was a problem hiding this comment.
Yeah that seems fine. There's already an is_nondep_elim in lcnf.cpp.
kmill
changed the title
nonDep field of Expr.letE to the C++ data modelnondep field of Expr.letE to the C++ data model
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 13, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 13, 2025
leanprover-community-bot
added
breaks-mathlib
leodemoura
reviewed
Jun 14, 2025
| match f with | ||
| | .lam n _ b _ => some (n, t, v, b) | ||
| | _ => some (.anonymous, t, v, .app f (.bvar 0)) | ||
| | _ => some (.anonymous, t, v, .app (f.liftLooseBVars 0 1) (.bvar 0)) |
Member
There was a problem hiding this comment.
Did you hit this bug when implementing this PR?
Collaborator
Author
There was a problem hiding this comment.
Sorry, this wasn't good PR hygiene. I found this bug in other work, and I was extracting changes to Expr.lean to make this PR.
I plan to deprecate/delete this function anyway, but I left in the change because it does fix a bug.
kmill
added a commit
to kmill/lean4
that referenced
this pull request
Jun 14, 2025
This PR adds `have` forms of simp lemmas that will be used in a future `have` simplifier. This depends on leanprover#8751 and future elaboration changes, since these are meant to elaborate using `Expr.letE (nondep := true) ..` expressions; otherwise they are duplicates of the `letFun_*` lemmas.
github-merge-queue bot
pushed a commit
that referenced
this pull request
Jun 14, 2025
This PR adds `have` forms of simp lemmas that will be used in a future `have` simplifier. This depends on #8751 and future elaboration changes, since these are meant to elaborate using `Expr.letE (nondep := true) ..` expressions; for now they are duplicates of the `letFun_*` lemmas.
kmill
added a commit
to kmill/lean4
that referenced
this pull request
Jun 16, 2025
This PR implements first-class support for nondependent let expressions in the elaborator; recall that a let expression `let x := v; b` is called *nondependent* if `fun x => b` typechecks, and the notation for a nondependent let expression is `have x := v; b`. Previously we encoded `have` using the `letFun` function, but now we make use of the `nondep` flag in the `Expr.letE` constructor for the encoding. This has been fully supported throughout the metaprogramming interface and the elaborator. Note that nondependence of lets is not checked by the kernel. Follows up from leanprover#8751, which made sure the nondep flag was preserved in the C++ interface.
jcommelin
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 16, 2025
* Update lean-toolchain for testing leanprover/lean4#8584 * chore: adaptations for nightly-2025-06-02 * change phrasing of comments * chore(Geometry/Manifold): two simp-lemmas can be proven by simp * fix two lint problems * Trigger CI for leanprover/lean4#8519 * chore: bump to nightly-2025-06-03 * fix * fix * Update lean-toolchain for testing leanprover/lean4#8610 * fix * revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <[email protected]> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Jovan Gerbscheid <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Mario Carneiro <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]>
jcommelin
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 17, 2025
* chore: bump to nightly-2025-06-03 * fix * fix * Update lean-toolchain for testing leanprover/lean4#8610 * fix * revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <[email protected]> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: Jovan Gerbscheid <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Mario Carneiro <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]>
jcommelin
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 17, 2025
* revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <[email protected]> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 --------- Co-authored-by: Jovan Gerbscheid <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Mario Carneiro <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Rob23oba <[email protected]>
algebraic-dev
pushed a commit
to algebraic-dev/lean4
that referenced
this pull request
Jun 18, 2025
…anprover#8751) This PR adds the `nondep` field of `Expr.letE` to the C++ data model. Previously this field has been unused, and in followup PRs the elaborator will use it to encode `have` expressions (non-dependent `let`s). The kernel does not verify that `nondep` is correctly applied during typechecking. The `letE` delaborator now prints `have`s when `nondep` is true, though `have` still elaborates as `letFun` for now. Breaking change: `Expr.updateLet!` is renamed to `Expr.updateLetE!`. This PR also fixes a bug in `Expr.letFun?` and `Expr.letFunAppArgs?` when the body is not a lambda. In any case, these functions will be removed once the `Expr.letE (nondep := true)` encoding of `have` expressions is complete.
algebraic-dev
pushed a commit
to algebraic-dev/lean4
that referenced
this pull request
Jun 18, 2025
This PR adds `have` forms of simp lemmas that will be used in a future `have` simplifier. This depends on leanprover#8751 and future elaboration changes, since these are meant to elaborate using `Expr.letE (nondep := true) ..` expressions; for now they are duplicates of the `letFun_*` lemmas.
kmill
added a commit
to kmill/lean4
that referenced
this pull request
Jun 18, 2025
This PR implements first-class support for nondependent let expressions in the elaborator; recall that a let expression `let x := v; b` is called *nondependent* if `fun x => b` typechecks, and the notation for a nondependent let expression is `have x := v; b`. Previously we encoded `have` using the `letFun` function, but now we make use of the `nondep` flag in the `Expr.letE` constructor for the encoding. This has been fully supported throughout the metaprogramming interface and the elaborator. Note that nondependence of lets is not checked by the kernel. Follows up from leanprover#8751, which made sure the nondep flag was preserved in the C++ interface.
jcommelin
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 19, 2025
* bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <[email protected]> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Kim Morrison <[email protected]> * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: Jovan Gerbscheid <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Mario Carneiro <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]>
jcommelin
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 20, 2025
* Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <[email protected]> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Kim Morrison <[email protected]> * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * chore: bump to nightly-2025-06-19 * fix * remove mul_hmul * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Mario Carneiro <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]>
kmill
added a commit
to kmill/lean4
that referenced
this pull request
Jun 22, 2025
This PR implements first-class support for nondependent let expressions in the elaborator; recall that a let expression `let x := v; b` is called *nondependent* if `fun x => b` typechecks, and the notation for a nondependent let expression is `have x := v; b`. Previously we encoded `have` using the `letFun` function, but now we make use of the `nondep` flag in the `Expr.letE` constructor for the encoding. This has been fully supported throughout the metaprogramming interface and the elaborator. Note that nondependence of lets is not checked by the kernel. Follows up from leanprover#8751, which made sure the nondep flag was preserved in the C++ interface.
github-merge-queue bot
pushed a commit
that referenced
this pull request
Jun 22, 2025
This PR implements first-class support for nondependent let expressions in the elaborator; recall that a let expression `let x : t := v; b` is called *nondependent* if `fun x : t => b` typechecks, and the notation for a nondependent let expression is `have x := v; b`. Previously we encoded `have` using the `letFun` function, but now we make use of the `nondep` flag in the `Expr.letE` constructor for the encoding. This has been given full support throughout the metaprogramming interface and the elaborator. Key changes to the metaprogramming interface: - Local context `ldecl`s with `nondep := true` are generally treated as `cdecl`s. This is because in the body of a `have` expression the variable is opaque. Functions like `LocalDecl.isLet` by default return `false` for nondependent `ldecl`s. In the rare case where it is needed, they take an additional optional `allowNondep : Bool` flag (defaults to `false`) if the variable is being processed in a context where the value is relevant. - Functions such as `mkLetFVars` by default generalize nondependent let variables and create lambda expressions for them. The `generalizeNondepLet` flag (default true) can be set to false if `have` expressions should be produced instead. **Breaking change:** Uses of `letLambdaTelescope`/`mkLetFVars` need to use `generalizeNondepLet := false`. See the next item. - There are now some mapping functions to make telescoping operations more convenient. See `mapLetTelescope` and `mapLambdaLetTelescope`. There is also `mapLetDecl` as a counterpart to `withLetDecl` for creating `let`/`have` expressions. - Important note about the `generalizeNondepLet` flag: it should only be used for variables in a local context that the metaprogram "owns". Since nondependent let variables are treated as constants in most cases, the `value` field might refer to variables that do not exist, if for example those variables were cleared or reverted. Using `mapLetDecl` is always fine. - The simplifier will cache its let dependence calculations in the nondep field of let expressions. - The `intro` tactic still produces *dependent* local variables. Given that the simplifier will transform lets into haves, it would be surprising if that would prevent `intro` from creating a local variable whose value cannot be used. Note that nondependence of lets is not checked by the kernel. To external checker authors: If the elaborator gets the nondep flag wrong, we consider this to be an elaborator error. Feel free to typecheck `letE n t v b true` as if it were `app (lam n t b default) v` and please report issues. This PR follows up from #8751, which made sure the nondep flag was preserved in the C++ interface.
wkrozowski
pushed a commit
to wkrozowski/lean4
that referenced
this pull request
Jun 24, 2025
…anprover#8751) This PR adds the `nondep` field of `Expr.letE` to the C++ data model. Previously this field has been unused, and in followup PRs the elaborator will use it to encode `have` expressions (non-dependent `let`s). The kernel does not verify that `nondep` is correctly applied during typechecking. The `letE` delaborator now prints `have`s when `nondep` is true, though `have` still elaborates as `letFun` for now. Breaking change: `Expr.updateLet!` is renamed to `Expr.updateLetE!`. This PR also fixes a bug in `Expr.letFun?` and `Expr.letFunAppArgs?` when the body is not a lambda. In any case, these functions will be removed once the `Expr.letE (nondep := true)` encoding of `have` expressions is complete.
wkrozowski
pushed a commit
to wkrozowski/lean4
that referenced
this pull request
Jun 24, 2025
This PR adds `have` forms of simp lemmas that will be used in a future `have` simplifier. This depends on leanprover#8751 and future elaboration changes, since these are meant to elaborate using `Expr.letE (nondep := true) ..` expressions; for now they are duplicates of the `letFun_*` lemmas.
wkrozowski
pushed a commit
to wkrozowski/lean4
that referenced
this pull request
Jun 24, 2025
…prover#8804) This PR implements first-class support for nondependent let expressions in the elaborator; recall that a let expression `let x : t := v; b` is called *nondependent* if `fun x : t => b` typechecks, and the notation for a nondependent let expression is `have x := v; b`. Previously we encoded `have` using the `letFun` function, but now we make use of the `nondep` flag in the `Expr.letE` constructor for the encoding. This has been given full support throughout the metaprogramming interface and the elaborator. Key changes to the metaprogramming interface: - Local context `ldecl`s with `nondep := true` are generally treated as `cdecl`s. This is because in the body of a `have` expression the variable is opaque. Functions like `LocalDecl.isLet` by default return `false` for nondependent `ldecl`s. In the rare case where it is needed, they take an additional optional `allowNondep : Bool` flag (defaults to `false`) if the variable is being processed in a context where the value is relevant. - Functions such as `mkLetFVars` by default generalize nondependent let variables and create lambda expressions for them. The `generalizeNondepLet` flag (default true) can be set to false if `have` expressions should be produced instead. **Breaking change:** Uses of `letLambdaTelescope`/`mkLetFVars` need to use `generalizeNondepLet := false`. See the next item. - There are now some mapping functions to make telescoping operations more convenient. See `mapLetTelescope` and `mapLambdaLetTelescope`. There is also `mapLetDecl` as a counterpart to `withLetDecl` for creating `let`/`have` expressions. - Important note about the `generalizeNondepLet` flag: it should only be used for variables in a local context that the metaprogram "owns". Since nondependent let variables are treated as constants in most cases, the `value` field might refer to variables that do not exist, if for example those variables were cleared or reverted. Using `mapLetDecl` is always fine. - The simplifier will cache its let dependence calculations in the nondep field of let expressions. - The `intro` tactic still produces *dependent* local variables. Given that the simplifier will transform lets into haves, it would be surprising if that would prevent `intro` from creating a local variable whose value cannot be used. Note that nondependence of lets is not checked by the kernel. To external checker authors: If the elaborator gets the nondep flag wrong, we consider this to be an elaborator error. Feel free to typecheck `letE n t v b true` as if it were `app (lam n t b default) v` and please report issues. This PR follows up from leanprover#8751, which made sure the nondep flag was preserved in the C++ interface.
kim-em
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jun 29, 2025
* chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <[email protected]> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Kim Morrison <[email protected]> * Update lean-toolchain for testing leanprover/lean4#8577 * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8804 * Update lean-toolchain for testing leanprover/lean4#8699 * bump Qq and batteries * meta adaptations * bump aesop * fix * fix (adaptation note) * Update lean-toolchain for leanprover/lean4#8699 * shake * chore: bump to nightly-2025-06-19 * fix * Update lean-toolchain for leanprover/lean4#8699 * fix: correct memoFix's use of unsafe code * fix: adjust noncomputable annotations for new compiler * fix: replace use of `open private _ in` with `open private _ from` The implementation of `open private _ from` relies on specific internals of the old compiler and will no longer work. * remove mul_hmul * chore: adjust one maxHeartbeats for the new compiler * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 * Update lean-toolchain for testing leanprover/lean4#8914 * chore: bump to nightly-2025-06-21 * fix * fixes * fixes * fixes * updated lake manifest * comment out tests * chore: fix for nightly-testing (leanprover-community#26246) * fix * fix * fix grind typeclasses * chore: adaptations for nightly-2025-06-20 * lake update * Update lean-toolchain for leanprover/lean4#8914 * fix grind instance * chore: bump to nightly-2025-06-22 * chore: bump to nightly-2025-06-23 * chore: rm unused `Lean.Util.Paths` import & use updated batteries * Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist) * merge lean-pr-testing-8804 * Bump dependencies and silence linter. * Fixes (Now `elabSimpArgs` already handles `*`, so we can delete the associated code.) * lake update; disable unusedSimpArgs in Batteries * lkae update aesop * disable unusedSimpArgs in MathlibTest * fix grind instance priorities * comment out MathlibTest/zmod with adaptation note * touch for CI * chore: bump to nightly-2025-06-24 * Kick CI * Bump batteries * Guessing adaption for leanprover/lean4#8929 * chore: bump to nightly-2025-06-25 * fix: workflow merging master into nightly-testing * fix * chore: cache get uses tracking remote * touch for new CI * restart CI * chore: bump to nightly-2025-06-26 * Update lean-toolchain for testing leanprover/lean4#8928 * Teach Mathlib about `mrefine` * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8980 * chore: update linter warning test outputs * chore: remove excess line break in deprecation lint now that notes add their own line breaks * chore: more test cleanup * . * cleanup adaptation notes * fix * fix * chore: bump to nightly-2025-06-27 * Merge master into nightly-testing * Merge master into nightly-testing * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * fix tests * chore: bump to nightly-2025-06-28 * Merge master into nightly-testing * lintining * lint --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Cameron Zwarich <[email protected]> Co-authored-by: Mac Malone <[email protected]> Co-authored-by: Anne C.A. Baanen <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Sebastian Graf <[email protected]> Co-authored-by: Joseph Rotella <[email protected]>
kim-em
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jun 30, 2025
* cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Kim Morrison <[email protected]> * Update lean-toolchain for testing leanprover/lean4#8577 * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8804 * Update lean-toolchain for testing leanprover/lean4#8699 * bump Qq and batteries * meta adaptations * bump aesop * fix * fix (adaptation note) * Update lean-toolchain for leanprover/lean4#8699 * shake * chore: bump to nightly-2025-06-19 * fix * Update lean-toolchain for leanprover/lean4#8699 * fix: correct memoFix's use of unsafe code * fix: adjust noncomputable annotations for new compiler * fix: replace use of `open private _ in` with `open private _ from` The implementation of `open private _ from` relies on specific internals of the old compiler and will no longer work. * remove mul_hmul * chore: adjust one maxHeartbeats for the new compiler * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 * Update lean-toolchain for testing leanprover/lean4#8914 * chore: bump to nightly-2025-06-21 * fix * fixes * fixes * fixes * updated lake manifest * comment out tests * chore: fix for nightly-testing (leanprover-community#26246) * fix * fix * fix grind typeclasses * chore: adaptations for nightly-2025-06-20 * lake update * Update lean-toolchain for leanprover/lean4#8914 * fix grind instance * chore: bump to nightly-2025-06-22 * chore: bump to nightly-2025-06-23 * chore: rm unused `Lean.Util.Paths` import & use updated batteries * Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist) * merge lean-pr-testing-8804 * Bump dependencies and silence linter. * Fixes (Now `elabSimpArgs` already handles `*`, so we can delete the associated code.) * lake update; disable unusedSimpArgs in Batteries * lkae update aesop * disable unusedSimpArgs in MathlibTest * fix grind instance priorities * comment out MathlibTest/zmod with adaptation note * touch for CI * chore: bump to nightly-2025-06-24 * Kick CI * Bump batteries * Guessing adaption for leanprover/lean4#8929 * chore: bump to nightly-2025-06-25 * fix: workflow merging master into nightly-testing * fix * chore: cache get uses tracking remote * touch for new CI * restart CI * chore: bump to nightly-2025-06-26 * Update lean-toolchain for testing leanprover/lean4#8928 * Teach Mathlib about `mrefine` * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8980 * chore: update linter warning test outputs * chore: remove excess line break in deprecation lint now that notes add their own line breaks * chore: more test cleanup * . * cleanup adaptation notes * fix * fix * chore: bump to nightly-2025-06-27 * Merge master into nightly-testing * Merge master into nightly-testing * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * fix tests * chore: bump to nightly-2025-06-28 * Merge master into nightly-testing * lintining * Merge master into nightly-testing * unused simp args * chore: bump to nightly-2025-06-29 * chore: adaptations for nightly-2025-06-29 * Merge master into nightly-testing * chore: robustify `open Mathlib` benchmark * deprecations * Update lean-toolchain for testing leanprover/lean4#9086 * Merge master into nightly-testing * fixes * chore: bump to nightly-2025-06-30 * lake update * lake update * lake update * lake update * lake update * . --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Cameron Zwarich <[email protected]> Co-authored-by: Mac Malone <[email protected]> Co-authored-by: Anne C.A. Baanen <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Sebastian Graf <[email protected]> Co-authored-by: Joseph Rotella <[email protected]>
kim-em
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jul 3, 2025
* fix * fixes * chore: adaptations for nightly-2025-06-16 (leanprover-community#25994) * chore: bump to nightly-2025-06-03 * fix * fix * Update lean-toolchain for testing leanprover/lean4#8610 * fix * revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <[email protected]> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: Jovan Gerbscheid <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Mario Carneiro <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 (leanprover-community#26043) * revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <[email protected]> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 --------- Co-authored-by: Jovan Gerbscheid <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Mario Carneiro <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Rob23oba <[email protected]> * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Kim Morrison <[email protected]> * Update lean-toolchain for testing leanprover/lean4#8577 * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8804 * Update lean-toolchain for testing leanprover/lean4#8699 * bump Qq and batteries * meta adaptations * bump aesop * fix * fix (adaptation note) * Update lean-toolchain for leanprover/lean4#8699 * shake * chore: adaptations for nightly-2025-06-18 (leanprover-community#26077) * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <[email protected]> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Kim Morrison <[email protected]> * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: Jovan Gerbscheid <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Mario Carneiro <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> * chore: bump to nightly-2025-06-19 * feat: add algebra shims for Grind.Nat/IntModule (leanprover-community#26133) This PR adds shims so `grind` will understand Mathlib's `AddCommMonoid` and `AddCommGroup`. (Subsequent shims will connect up the order structures for modules and rings.) * fix * Update lean-toolchain for leanprover/lean4#8699 * fix: correct memoFix's use of unsafe code * fix: adjust noncomputable annotations for new compiler * fix: replace use of `open private _ in` with `open private _ from` The implementation of `open private _ from` relies on specific internals of the old compiler and will no longer work. * remove mul_hmul * chore: adjust one maxHeartbeats for the new compiler * linter * feat: generalize grind algebra shims (leanprover-community#26131) This PR extends the shims converting from Mathlib to `Lean.Grind` typeclasses, now that `grind` knows about (non-commutative)-(semi)-rings. * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 (leanprover-community#26209) * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <[email protected]> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Kim Morrison <[email protected]> * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * chore: bump to nightly-2025-06-19 * fix * remove mul_hmul * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Mario Carneiro <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> * Update lean-toolchain for testing leanprover/lean4#8914 * chore: bump to nightly-2025-06-21 * fix * fixes * fixes * fixes * updated lake manifest * comment out tests * chore: fix for nightly-testing (leanprover-community#26246) * fix * fix * fix grind typeclasses * chore: adaptations for nightly-2025-06-20 * lake update * Update lean-toolchain for leanprover/lean4#8914 * fix grind instance * chore: bump to nightly-2025-06-22 * chore: bump to nightly-2025-06-23 * chore: rm unused `Lean.Util.Paths` import & use updated batteries * Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist) * merge lean-pr-testing-8804 * Bump dependencies and silence linter. * Fixes (Now `elabSimpArgs` already handles `*`, so we can delete the associated code.) * lake update; disable unusedSimpArgs in Batteries * lkae update aesop * disable unusedSimpArgs in MathlibTest * fix grind instance priorities * comment out MathlibTest/zmod with adaptation note * touch for CI * chore: bump to nightly-2025-06-24 * Kick CI * Bump batteries * Guessing adaption for leanprover/lean4#8929 * chore: bump to nightly-2025-06-25 * fix: workflow merging master into nightly-testing * fix * chore: cache get uses tracking remote * touch for new CI * restart CI * chore: bump to nightly-2025-06-26 * Update lean-toolchain for testing leanprover/lean4#8928 * Teach Mathlib about `mrefine` * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8980 * chore: update linter warning test outputs * chore: remove excess line break in deprecation lint now that notes add their own line breaks * chore: more test cleanup * . * cleanup adaptation notes * fix * fix * chore: bump to nightly-2025-06-27 * chore: adaptations for nightly-2025-06-26 (#2) * Merge master into nightly-testing * Merge master into nightly-testing * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * chore: adaptations for nightly-2025-06-27 (#3) * fix tests * chore: bump to nightly-2025-06-28 * Merge master into nightly-testing * lintining * Merge master into nightly-testing * unused simp args * chore: bump to nightly-2025-06-29 * chore: adaptations for nightly-2025-06-29 * chore: adaptations for nightly-2025-06-28 (#5) * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <[email protected]> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Kim Morrison <[email protected]> * Update lean-toolchain for testing leanprover/lean4#8577 * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8804 * Update lean-toolchain for testing leanprover/lean4#8699 * bump Qq and batteries * meta adaptations * bump aesop * fix * fix (adaptation note) * Update lean-toolchain for leanprover/lean4#8699 * shake * chore: bump to nightly-2025-06-19 * fix * Update lean-toolchain for leanprover/lean4#8699 * fix: correct memoFix's use of unsafe code * fix: adjust noncomputable annotations for new compiler * fix: replace use of `open private _ in` with `open private _ from` The implementation of `open private _ from` relies on specific internals of the old compiler and will no longer work. * remove mul_hmul * chore: adjust one maxHeartbeats for the new compiler * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 * Update lean-toolchain for testing leanprover/lean4#8914 * chore: bump to nightly-2025-06-21 * fix * fixes * fixes * fixes * updated lake manifest * comment out tests * chore: fix for nightly-testing (leanprover-community#26246) * fix * fix * fix grind typeclasses * chore: adaptations for nightly-2025-06-20 * lake update * Update lean-toolchain for leanprover/lean4#8914 * fix grind instance * chore: bump to nightly-2025-06-22 * chore: bump to nightly-2025-06-23 * chore: rm unused `Lean.Util.Paths` import & use updated batteries * Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist) * merge lean-pr-testing-8804 * Bump dependencies and silence linter. * Fixes (Now `elabSimpArgs` already handles `*`, so we can delete the associated code.) * lake update; disable unusedSimpArgs in Batteries * lkae update aesop * disable unusedSimpArgs in MathlibTest * fix grind instance priorities * comment out MathlibTest/zmod with adaptation note * touch for CI * chore: bump to nightly-2025-06-24 * Kick CI * Bump batteries * Guessing adaption for leanprover/lean4#8929 * chore: bump to nightly-2025-06-25 * fix: workflow merging master into nightly-testing * fix * chore: cache get uses tracking remote * touch for new CI * restart CI * chore: bump to nightly-2025-06-26 * Update lean-toolchain for testing leanprover/lean4#8928 * Teach Mathlib about `mrefine` * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8980 * chore: update linter warning test outputs * chore: remove excess line break in deprecation lint now that notes add their own line breaks * chore: more test cleanup * . * cleanup adaptation notes * fix * fix * chore: bump to nightly-2025-06-27 * Merge master into nightly-testing * Merge master into nightly-testing * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * fix tests * chore: bump to nightly-2025-06-28 * Merge master into nightly-testing * lintining * lint --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Cameron Zwarich <[email protected]> Co-authored-by: Mac Malone <[email protected]> Co-authored-by: Anne C.A. Baanen <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Sebastian Graf <[email protected]> Co-authored-by: Joseph Rotella <[email protected]> * Merge master into nightly-testing * chore: robustify `open Mathlib` benchmark * deprecations * Update lean-toolchain for testing leanprover/lean4#9086 * Merge master into nightly-testing * fixes * chore: bump to nightly-2025-06-30 * lake update * lake update * lake update * lake update * lake update * . * Merge master into nightly-testing * Merge master into nightly-testing * Merge master into nightly-testing * Merge master into nightly-testing * cleanup * unusedSimpArgs * bump toolchain * lake update * Merge master into nightly-testing * Merge master into nightly-testing * chore: adaptations for nightly-2025-07-01 * add adaptation note * add adaptation note * chore: bump to nightly-2025-07-02 * fixes * Merge master into nightly-testing * fixes * update test output * Merge master into nightly-testing * Merge master into nightly-testing * chore: bump to nightly-2025-07-03 * chore: adaptations for nightly-2025-07-03 --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: github-actions <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: Jovan Gerbscheid <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Mario Carneiro <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Cameron Zwarich <[email protected]> Co-authored-by: Mac Malone <[email protected]> Co-authored-by: Anne C.A. Baanen <[email protected]> Co-authored-by: Sebastian Graf <[email protected]> Co-authored-by: Joseph Rotella <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds the
nondepfield ofExpr.letEto the C++ data model. Previously this field has been unused, and in followup PRs the elaborator will use it to encodehaveexpressions (non-dependentlets). The kernel does not verify thatnondepis correctly applied during typechecking. TheletEdelaborator now printshaves whennondepis true, thoughhavestill elaborates asletFunfor now. Breaking change:Expr.updateLet!is renamed toExpr.updateLetE!.This PR also fixes a bug in
Expr.letFun?andExpr.letFunAppArgs?when the body is not a lambda. In any case, these functions will be removed once theExpr.letE (nondep := true)encoding ofhaveexpressions is complete.