The Lean Language Reference

Lean 4.2.0 (2023-10-31)🔗

  • isDefEq cache for terms not containing metavariables..

  • Make Environment.mk and Environment.add private, and add replay as a safer alternative.

  • IO.Process.output no longer inherits the standard input of the caller.

  • Do not inhibit caching of default-level match reduction.

  • List the valid case tags when the user writes an invalid one.

  • The derive handler for DecidableEq now handles mutual inductive types.

  • Show path of failed import in Lake.

  • Fix linker warnings on macOS.

  • Lake: Add postUpdate? package configuration option. Used by a package to specify some code which should be run after a successful lake update of the package or one of its downstream dependencies. (lake#185)

  • Improvements to Lake startup time (#2572, #2573)

  • refine e now replaces the main goal with metavariables which were created during elaboration of e and no longer captures pre-existing metavariables that occur in e (#2502).

    • This is accomplished via changes to withCollectingNewGoalsFrom, which also affects elabTermWithHoles, refine', calc (tactic), and specialize. Likewise, all of these now only include newly-created metavariables in their output.

    • Previously, both newly-created and pre-existing metavariables occurring in e were returned inconsistently in different edge cases, causing duplicated goals in the infoview (issue #2495), erroneously closed goals (issue #2434), and unintuitive behavior due to refine e capturing previously-created goals appearing unexpectedly in e (no issue; see PR).