mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00

Files

Kim Morrison 4d0b7cf66c chore: begin development cycle for v4.11.0 (#4594 )

2024-06-30 23:28:48 +00:00

152 KiB

Raw Blame History

Lean 4 releases

We intend to provide regular "minor version" releases of the Lean language at approximately monthly intervals. There is not yet a strong guarantee of backwards compatibility between versions, only an expectation that breaking changes will be documented in this file.

This file contains work-in-progress notes for the upcoming release, as well as previous stable releases. Please check the releases page for the current status of each version.

v4.11.0

Development in progress.

v4.10.0

Release candidate, release notes will be copied from branch releases/v4.10.0 once completed.

v4.9.0

Language features, tactics, and metaprograms

Definition transparency
- #4053 adds the seal and unseal commands, which make definitions locally be irreducible or semireducible.
- #4061 marks functions defined by well-founded recursion with @[irreducible] by default, which should prevent the expensive and often unfruitful unfolding of such definitions (see breaking changes below).
Incrementality
- #3940 extends incremental elaboration into various steps inside of declarations: definition headers, bodies, and tactics. .
- 250994 and 67338b add @[incremental] attribute to mark an elaborator as supporting incremental elaboration.
- #4259 improves resilience by ensuring incremental commands and tactics are reached only in supported ways.
- #4268 adds special handling for := by so that stray tokens in tactic blocks do not inhibit incrementality.
- #4308 adds incremental have tactic.
- #4340 fixes incorrect info tree reuse.
- #4364 adds incrementality for careful command macros such as set_option in theorem, theorem foo.bar, and lemma.
- #4395 adds conservative fix for whitespace handling to avoid incremental reuse leading to goals in front of the text cursor being shown.
- #4407 fixes non-incremental commands in macros blocking further incremental reporting.
- #4436 fixes incremental reporting when there are nested tactics in terms.

Functional induction

#4135 ensures that the names used for functional induction are reserved.

#4327 adds support for structural recursion on reflexive types. For example,

inductive Many (α : Type u) where
  | none : Many α
  | more : α → (Unit → Many α) → Many α

def Many.map {α β : Type u} (f : α → β) : Many α → Many β
  | .none => .none
  | .more x xs => .more (f x) (fun _ => (xs ()).map f)

#check Many.map.induct
/-
Many.map.induct {α β : Type u} (f : α → β) (motive : Many α → Prop)
  (case1 : motive Many.none)
  (case2 : ∀ (x : α) (xs : Unit → Many α), motive (xs ()) → motive (Many.more x xs)) :
  ∀ (a : Many α), motive a
-/

#3903 makes the Lean frontend normalize all line endings to LF before processing. This lets Lean be insensitive to CRLF vs LF line endings, improving the cross-platform experience and making Lake hashes be faithful to what Lean processes.
#4130 makes the tactic framework be able to recover from runtime errors (for example, deterministic timeouts or maximum recursion depth errors).
split tactic
- #4211 fixes split at h when h has forward dependencies.
- #4349 allows split for if-expressions to work on non-propositional goals.
apply tactic
- #3929 makes error message for apply show implicit arguments in unification errors as needed. Modifies MessageData type (see breaking changes below).
cases tactic
- #4224 adds support for unification of offsets such as x + 20000 = 20001 in cases tactic.
omega tactic
- #4073 lets omega fall back to using classical Decidable instances when setting up contradiction proofs.
- #4141 and #4184 fix bugs.
- #4264 improves omega error message if no facts found in local context.
- #4358 improves expression matching in omega by using match_expr.
simp tactic
- #4176 makes names of erased lemmas clickable.
- #4208 adds a pretty printer for discrimination tree keys.
- #4202 adds Simp.Config.index configuration option, which controls whether to use the full discrimination tree when selecting candidate simp lemmas. When index := false, only the head function is taken into account, like in Lean 3. This feature can help users diagnose tricky simp failures or issues in code from libraries developed using Lean 3 and then ported to Lean 4.
  
  In the following example, it will report that foo is a problematic theorem.
```
opaque f : Nat → Nat → Nat

@[simp] theorem foo : f x (x, y).2 = y := by sorry

example : f a b ≤ b := by
  set_option diagnostics true in
  simp (config := { index := false })
/-
[simp] theorems with bad keys
  foo, key: f _ (@Prod.mk ℕ ℕ _ _).2
-/
```
  With the information above, users can annotate theorems such as foo using no_index for problematic subterms. Example:
```
opaque f : Nat → Nat → Nat

@[simp] theorem foo : f x (no_index (x, y).2) = y := by sorry

example : f a b ≤ b := by
  simp -- `foo` is still applied with `index := true`
```
- #4274 prevents internal match equational theorems from appearing in simp trace.
- #4177 and #4359 make simp continue even if a simp lemma does not elaborate, if the tactic state is in recovery mode.
- #4341 fixes panic when applying @[simp] to malformed theorem syntax.
- #4345 fixes simp so that it does not use the forward version of a user-specified backward theorem.
- #4352 adds missing dsimp simplifications for fixed parameters of generated congruence theorems.
- #4362 improves trace messages for simp so that constants are hoverable.
Elaboration
- #4046 makes subst notation (he ▸ h) try rewriting in both directions even when there is no expected type available.
- #3328 adds support for identifiers in autoparams (for example, rfl in (h : x = y := by exact rfl)).
- #4096 changes how the type in let and have is elaborated, requiring that any tactics in the type be evaluated before proceeding, improving performance.
- #4215 ensures the expression tree elaborator commits to the computed "max type" for the entire arithmetic expression.
- #4267 cases signature elaboration errors to show even if there are parse errors in the body.
- #4368 improves error messages when numeric literals fail to synthesize an OfNat instance, including special messages warning when the expected type of the numeral can be a proposition.
Metaprogramming
- #4167 adds Lean.MVarId.revertAll to revert all free variables.
- #4169 adds Lean.MVarId.ensureNoMVar to ensure the goal's target contains no expression metavariables.
- #4180 adds cleanupAnnotations parameter to forallTelescope methods.
- #4307 adds support for parser aliases in syntax quotations.
Work toward implementing grind tactic
- 0a515e and #4164 add grind_norm and grind_norm_proc attributes and @[grind_norm] theorems.
- #4170, #4221, and #4249 create grind preprocessor and core module.
- #4235 and d6709e add special cases tactic to grind along with @[grind_cases] attribute to mark types that this cases tactic should automatically apply to.
- #4243 adds special injection? tactic to grind.
Other fixes or improvements
- #4065 fixes a bug in the Nat.reduceLeDiff simproc.
- #3969 makes deprecation warnings activate even for generalized field notation ("dot notation").
- #4132 fixes the sorry term so that it does not activate the implicit lambda feature
- 9803c5 and 47c8e3 move cdot and calc parsers to Lean namespace.
- #4252 fixes the case tactic so that it is usable in macros by having it erase macro scopes from the tag.
- 26b671 and cc33c3 extract haveId syntax.
- #4335 fixes bugs in partial calc tactic when there is mdata or metavariables.
- #4329 makes termination_by? report unused each unused parameter as _.
Docs: #4238, #4294, #4338.

Language server, widgets, and IDE extensions

#4066 fixes features like "Find References" when browsing core Lean sources.
#4254 allows embedding user widgets in structured messages. Companion PR is vscode-lean4#449.
#4445 makes watchdog more resilient against badly behaving clients.

Library

#4059 upstreams many List and Array operations and theorems from Batteries.
#4055 removes the unused Inhabited instance for Subtype.
#3967 adds dates in existing @[deprecated] attributes.
#4231 adds boilerplate Char, UInt, and Fin theorems.
#4205 fixes the MonadStore type classes to use semiOutParam.
#4350 renames IsLawfulSingleton to LawfulSingleton.
Nat
- #4094 swaps Nat.zero_or and Nat.or_zero.
- #4098 and #4145 change the definition of Nat.mod so that n % (m + n) reduces when n is literal without relying on well-founded recursion, which becomes irreducible by default in #4061.
- #4188 redefines Nat.testBit to be more performant.
- Theorems: #4199.
Array
- #4074 improves the functional induction principle Array.feraseIdx.induct.
List
- #4172 removes @[simp] from List.length_pos.
Option
- #4037 adds theorems to simplify Option-valued dependent if-then-else.
- #4314 removes @[simp] from Option.bind_eq_some.
BitVec
- Theorems: #3920, #4095, #4075, #4148, #4165, #4178, #4200, #4201, #4298, #4299, #4257, #4179, #4321, #4187.
- #4193 adds simprocs for reducing x >>> i and x <<< i where i is a bitvector literal.
- #4194 adds simprocs for reducing (x <<< i) <<< j and (x >>> i) >>> j where i and j are natural number literals.
- #4229 redefines rotateLeft/rotateRight to use modulo reduction of shift offset.
- 0d3051 makes <num>#<term> bitvector literal notation global.
Char/String
- #4143 modifies String.substrEq to avoid linter warnings in downstream code.
- #4233 adds simprocs for Char and String inequalities.
- #4348 upstreams Mathlib lemmas.
- #4354 upstreams basic String lemmas.
HashMap
- #4248 fixes implicitness of typeclass arguments in HashMap.ofList.
IO
- #4036 adds IO.Process.getCurrentDir and IO.Process.setCurrentDir for adjusting the current process's working directory.
Cleanup: #4077, #4189, #4304.
Docs: #4001, #4166, #4332.

Lean internals

Defeq and WHNF algorithms
- #4029 remove unnecessary checkpointDefEq
- #4206 fixes isReadOnlyOrSyntheticOpaque to respect metavariable depth.
- #4217 fixes missing occurs check for delayed assignments.
Definition transparency
- #4052 adds validation to application of @[reducible]/@[semireducible]/@[irreducible] attributes (with local/scoped modifiers as well). Setting set_option allowUnsafeReductibility true turns this validation off.
Inductive types
- #3591 fixes a bug where indices could be incorrectly promoted to parameters.
- #3398 fixes a bug in the injectivity theorem generator.
- #4342 fixes elaboration of mutual inductives with instance parameters.
Diagnostics and profiling
- #3986 adds option trace.profiler.useHeartbeats to switch trace.profiler.threshold to being in terms of heartbeats instead of milliseconds.
- #4082 makes set_option diagnostics true report kernel diagnostic information.
Typeclass resolution
- #4119 fixes multiple issues with TC caching interacting with synthPendingDepth, adds maxSynthPendingDepth option with default value 1.
- #4210 ensures local instance cache does not contain multiple copies of the same instance.
- #4216 fix handling of metavariables, to avoid needing to set the option backward.synthInstance.canonInstances to false.
Other fixes or improvements
- #4080 fixes propagation of state for Lean.Elab.Command.liftCoreM and Lean.Elab.Command.liftTermElabM.
- #3944 makes the Repr deriving handler be consistent between structure and inductive for how types and proofs are erased.
- #4113 propagates maxHeartbeats to kernel to control "(kernel) deterministic timeout" error.
- #4125 reverts #3970 (monadic generalization of FindExpr).
- #4128 catches stack overflow in auto-bound implicits feature.
- #4129 adds tryCatchRuntimeEx combinator to replace catchRuntimeEx reader state.
- #4155 simplifies the expression canonicalizer.
- #4151 and #4369 add many missing trace classes.
- #4185 makes congruence theorem generators clean up type annotations of argument types.
- #4192 fixes restoration of infotrees when auto-bound implicit feature is activated, fixing a pretty printing error in hovers and strengthening the unused variable linter.
- dfb496 fixes declareBuiltin to allow it to be called multiple times per declaration.
- Cleanup: #4112, #4126, #4091, #4139, #4153.
- Tests: 030406, #4133.

Compiler, runtime, and FFI

#4100 improves reset/reuse algorithm; it now runs a second pass relaxing the constraint that reused memory cells must only be for the exact same constructor.
#2903 fixes segfault in old compiler from mishandling noConfusion applications.
#4311 fixes bug in constant folding.
#3915 documents the runtime memory layout for inductive types.

Lake

#4057 adds support for docstrings on require commands.
#4088 improves hovers for family_def and library_data commands.
#4147 adds default README.md to package templates
#4261 extends lake test help page, adds help page for lake check-test, adds lake lint and tag @[lint_driver], adds support for specifying test and lint drivers from dependencies, adds testDriverArgs and lintDriverArgs options, adds support for library test drivers, makes lake check-test and lake check-lint only load the package without dependencies.
#4270 adds lake pack and lake unpack for packing and unpacking Lake build artifacts from an archive.
#4083 Switches the manifest format to use major.minor.patch semantic versions. Major version increments indicate breaking changes (e.g., new required fields and semantic changes to existing fields). Minor version increments (after 0.x) indicate backwards-compatible extensions (e.g., adding optional fields, removing fields). This change is backwards compatible. Lake will still successfully read old manifests with numeric versions. It will treat the numeric version N as semantic version 0.N.0. Lake will also accept manifest versions with - suffixes (e.g., x.y.z-foo) and then ignore the suffix.
#4273 adds a lift from JobM to FetchM for backwards compatibility reasons.
#4351 fixes LogIO-to-CliM-lifting performance issues.
#4343 make Lake store the dependency trace for a build in the cached build long and then verifies that it matches the trace of the current build before replaying the log.
#4402 moves the cached log into the trace file (no more .log.json). This means logs are no longer cached on fatal errors and this ensures that an out-of-date log is not associated with an up-to-date trace. Separately, .hash file generation was changed to be more reliable as well. The .hash files are deleted as part of the build and always regenerate with --rehash.
Other fixes or improvements
- #4056 cleans up tests
- #4244 fixes noRelease test when Lean repo is tagged
- #4346 improves tests/serve
- #4356 adds build log path to the warning for a missing or invalid build log.

DevOps

#3984 adds a script (script/rebase-stage0.sh) for git rebase -i that automatically updates each stage0.
#4108 finishes renamings from transition to Std to Batteries.
#4109 adjusts the Github bug template to mention testing using live.lean-lang.org.
#4136 makes CI rerun only when full-ci label is added or removed.
#4175 and 72b345 switch to using #guard_msgs to run tests as much as possible.
#3125 explains the Lean4 pygments lexer.
#4247 sets up a procedure for preparing release notes.
#4032 modernizes build instructions and workflows.
#4255 moves some expensive checks from merge queue to releases.
#4265 adds aarch64 macOS as native compilation target for CI.
f05a82 restores macOS aarch64 install suffix in CI
#4317 updates build instructions for macOS.
#4333 adjusts workflow to update Batteries in manifest when creating lean-pr-testing-NNNN Mathlib branches.
#4355 simplifies lean4checker step of release checklist.
#4361 adds installing elan to pr-release CI step.

Breaking changes

While most changes could be considered to be a breaking change, this section makes special note of API changes.

Nat.zero_or and Nat.or_zero have been swapped (#4094).
IsLawfulSingleton is now LawfulSingleton (#4350).
BitVec.rotateLeft and BitVec.rotateRight now take the shift modulo the bitwidth (#4229).
These are no longer simp lemmas: List.length_pos (#4172), Option.bind_eq_some (#4314).
Types in let and have (both the expressions and tactics) may fail to elaborate due to new restrictions on what sorts of elaboration problems may be postponed (#4096). In particular, tactics embedded in the type will no longer make use of the type of value in expressions such as let x : type := value; body.
Now functions defined by well-founded recursion are marked with @[irreducible] by default (#4061). Existing proofs that hold by definitional equality (e.g. rfl) can be rewritten to explictly unfold the function definition (using simp, unfold, rw), or the recursive function can be temporarily made semireducible (using unseal f in before the command), or the function definition itself can be marked as @[semireducible] to get the previous behavior.
Due to #3929:
- The MessageData.ofPPFormat constructor has been removed. Its functionality has been split into two:
  - for lazy structured messages, please use MessageData.lazy;
  - for embedding Format or FormatWithInfos, use MessageData.ofFormatWithInfos.
  An example migration can be found in #3929.
- The MessageData.ofFormat constructor has been turned into a function. If you need to inspect MessageData, you can pattern-match on MessageData.ofFormatWithInfos.

v4.8.0

Language features, tactics, and metaprograms

Functional induction principles. #3432, #3620, #3754, #3762, #3738, #3776, #3898.

Derived from the definition of a (possibly mutually) recursive function, a functional induction principle is created that is tailored to proofs about that function.

For example from:

def ackermann : Nat → Nat → Nat
  | 0, m => m + 1
  | n+1, 0 => ackermann n 1
  | n+1, m+1 => ackermann n (ackermann (n + 1) m)

we get

ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
  (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0)
  (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m))
  (x x : Nat) : motive x x

It can be used in the induction tactic using the using syntax:

induction n, m using ackermann.induct

The termination checker now recognizes more recursion patterns without an explicit termination_by. In particular the idiom of counting up to an upper bound, as in
```
def Array.sum (arr : Array Nat) (i acc : Nat) : Nat :=
  if _ : i < arr.size then
    Array.sum arr (i+1) (acc + arr[i])
  else
    acc
```
is recognized without having to say termination_by arr.size - i.
- #3630 makes termination_by? not use sizeOf when not needed
- #3652 improves the termination_by syntax.
- #3658 changes how termination arguments are elaborated.
- #3665 refactors GuessLex to allow inferring more complex termination arguments
- #3666 infers termination arguments such as xs.size - i
#3629, #3655, #3747: Adds @[induction_eliminator] and @[cases_eliminator] attributes to be able to define custom eliminators for the induction and cases tactics, replacing the @[eliminator] attribute. Gives custom eliminators for Nat so that induction and cases put goal states into terms of 0 and n + 1 rather than Nat.zero and Nat.succ n. Added option tactic.customEliminators to control whether to use custom eliminators. Added a hack for rcases/rintro/obtain to use the custom eliminator for Nat.
Shorter instances names. There is a new algorithm for generating names for anonymous instances. Across Std and Mathlib, the median ratio between lengths of new names and of old names is about 72%. With the old algorithm, the longest name was 1660 characters, and now the longest name is 202 characters. The new algorithm's 95th percentile name length is 67 characters, versus 278 for the old algorithm. While the new algorithm produces names that are 1.2% less unique, it avoids cross-project collisions by adding a module-based suffix when it does not refer to declarations from the same "project" (modules that share the same root). #3089 and #3934.
8d2adf Importing two different files containing proofs of the same theorem is no longer considered an error. This feature is particularly useful for theorems that are automatically generated on demand (e.g., equational theorems).
84b091 Lean now generates an error if the type of a theorem is not a proposition.
Definition transparency. 47a343. @[reducible], @[semireducible], and @[irreducible] are now scoped and able to be set for imported declarations.
simp/dsimp
- #3607 enables kernel projection reduction in dsimp
- b24fbf and acdb00: dsimproc command to define defeq-preserving simplification procedures.
- #3624 makes dsimp normalize raw nat literals as OfNat.ofNat applications.
- #3628 makes simp correctly handle OfScientific.ofScientific literals.
- #3654 makes dsimp? report used simprocs.
- dee074 fixes equation theorem handling in simp for non-recursive definitions.
- #3819 improved performance when simp encounters a loop.
- #3821 fixes discharger/cache interaction.
- #3824 keeps simp from breaking Char literals.
- #3838 allows Nat instances matching to be more lenient.
- #3870 documentation for simp configuration options.
- #3972 fixes simp caching.
- #4044 improves cache behavior for "well-behaved" dischargers.
omega
- #3639, #3766, #3853, #3875: introduces a term canonicalizer.
- #3736 improves handling of positivity for the modulo operator for Int.
- #3828 makes it work as a simp discharger.
- #3847 adds helpful error messages.
rfl
- #3671, #3708: upstreams the @[refl] attribute and the rfl tactic.
- #3751 makes apply_rfl not operate on Eq itself.
- #4067 improves error message when there are no goals.
#3719 upstreams the rw? tactic, with fixes and improvements in #3783, #3794, #3911.
conv
- #3659 adds a conv version of the calc tactic.
- #3763 makes conv clean up using try with_reducible rfl instead of try rfl.
#guard_msgs
- #3617 introduces whitespace protection using the ⏎ character.
- #3883: The #guard_msgs command now has options to change whitespace normalization and sensitivity to message ordering. For example, #guard_msgs (whitespace := lax) in cmd collapses whitespace before checking messages, and #guard_msgs (ordering := sorted) in cmd sorts the messages in lexicographic order before checking.
- #3931 adds an unused variables ignore function for #guard_msgs.
- #3912 adds a diff between the expected and actual outputs. This feature is currently disabled by default, but can be enabled with set_option guard_msgs.diff true. Depending on user feedback, this option may default to true in a future version of Lean.
do notation
- #3820 makes it an error to lift (<- ...) out of a pure if ... then ... else ...
Lazy discrimination trees
- #3610 fixes a name collision for LazyDiscrTree that could lead to cache poisoning.
- #3677 simplifies and fixes LazyDiscrTree handling for exact?/apply?.
- #3685 moves general exact?/apply? functionality into LazyDiscrTree.
- #3769 has lemma selection improvements for rw? and LazyDiscrTree.
- #3818 improves ordering of matches.
#3590 adds inductive.autoPromoteIndices option to be able to disable auto promotion of indices in the inductive command.
Miscellaneous bug fixes and improvements
- #3606 preserves cache and dischargeDepth fields in Lean.Meta.Simp.Result.mkEqSymm.
- #3633 makes elabTermEnsuringType respect errToSorry, improving error recovery of the have tactic.
- #3647 enables noncomputable unsafe definitions, for deferring implementations until later.
- #3672 adjust namespaces of tactics.
- #3725 fixes Ord derive handler for indexed inductive types with unused alternatives.
- #3893 improves performance of derived Ord instances.
- #3771 changes error reporting for failing tactic macros. Improves rfl error message.
- #3745 fixes elaboration of generalized field notation if the object of the notation is an optional parameter.
- #3799 makes commands such as universe, variable, namespace, etc. require that their argument appear in a later column. Commands that can optionally parse an ident or parse any number of idents generally should require that the ident use colGt. This keeps typos in commands from being interpreted as identifiers.
- #3815 lets the split tactic be used for writing code.
- #3822 adds missing info in induction tactic for with clauses of the form | cstr a b c => ?_.
- #3806 fixes withSetOptionIn combinator.
- #3844 removes unused trace.Elab.syntax option.
- #3896 improves hover and go-to-def for attribute command.
- #3989 makes linter options more discoverable.
- #3916 fixes go-to-def for syntax defined with @[builtin_term_parser].
- #3962 fixes how solveByElim handles symm lemmas, making exact?/apply? usable again.
- #3968 improves the @[deprecated] attribute, adding (since := "<date>") field.
- #3768 makes #print command show structure fields.
- #3974 makes exact?% behave like by exact? rather than by apply?.
- #3994 makes elaboration of he ▸ h notation more predictable.
- #3991 adjusts transparency for decreasing_trivial macros.
- #4092 improves performance of binop% and binrel% expression tree elaborators.
Docs: #3748, #3796, #3800, #3874, #3863, #3862, #3891, #3873, #3908, #3872.

Language server and IDE extensions

#3602 enables import auto-completions.
#3608 fixes issue leanprover/vscode-lean4#392. Diagnostic ranges had an off-by-one error that would misplace goal states for example.
#3014 introduces snapshot trees, foundational work for incremental tactics and parallelism. #3849 adds basic incrementality API.
#3271 adds support for server-to-client requests.
#3656 fixes jump to definition when there are conflicting names from different files. Fixes issue #1170.
#3691, #3925, #3932 keep semantic tokens synchronized (used for semantic highlighting), with performance improvements.
#3247 and #3730 add diagnostics to run "Restart File" when a file dependency is saved.
#3722 uses the correct module names when displaying references.
#3728 makes errors in header reliably appear and makes the "Import out of date" warning be at "hint" severity. #3739 simplifies the text of this warning.
#3778 fixes #3462, where info nodes from before the cursor would be used for computing completions.
#3985 makes trace timings appear in Infoview.

Pretty printing

#3797 fixes the hovers over binders so that they show their types.
#3640 and #3735: Adds attribute @[pp_using_anonymous_constructor] to make structures pretty print as ⟨x, y, z⟩ rather than as {a := x, b := y, c := z}. This attribute is applied to Sigma, PSigma, PProd, Subtype, And, and Fin.
#3749 Now structure instances pretty print with parent structures' fields inlined. That is, if B extends A, then { toA := { x := 1 }, y := 2 } now pretty prints as { x := 1, y := 2 }. Setting option pp.structureInstances.flatten to false turns this off.
#3737, #3744 and #3750: Option pp.structureProjections is renamed to pp.fieldNotation, and there is now a suboption pp.fieldNotation.generalized to enable pretty printing function applications using generalized field notation (defaults to true). Field notation can be disabled on a function-by-function basis using the @[pp_nodot] attribute. The notation is not used for theorems.
#4071 fixes interaction between app unexpanders and pp.fieldNotation.generalized
#3625 makes delabConstWithSignature (used by #check) have the ability to put arguments "after the colon" to avoid printing inaccessible names.
#3798, #3978, #3798: Adds options pp.mvars (default: true) and pp.mvars.withType (default: false). When pp.mvars is false, expression metavariables pretty print as ?_ and universe metavariables pretty print as _. When pp.mvars.withType is true, expression metavariables pretty print with a type ascription. These can be set when using #guard_msgs to make tests not depend on the particular names of metavariables.
#3917 makes binders hoverable and gives them docstrings.
#4034 makes hovers for RHS terms in match expressions in the Infoview reliably show the correct term.

Library

Bool/Prop
- #3508 improves simp confluence for Bool and Prop terms.
- Theorems: #3604
Nat
- #3579 makes Nat.succ_eq_add_one be a simp lemma, now that induction/cases uses n + 1 instead of Nat.succ n.
- #3808 replaces Nat.succ simp rules with simprocs.
- #3876 adds faster Nat.repr implementation in C.
Int
- Theorems: #3890
UInts
- #3960 improves performance of upcasting.
Array and Subarray
- #3676 removes Array.eraseIdxAux, Array.eraseIdxSzAux, and Array.eraseIdx'.
- #3648 simplifies Array.findIdx?.
- #3851 renames fields of Subarray.
List
- #3785 upstreams tail-recursive List operations and @[csimp] lemmas.
BitVec
- Theorems: #3593, #3593, #3597, #3598, #3721, #3729, #3880, #4039.
- #3884 protects Std.BitVec.
String
- #3832 fixes String.splitOn.
- #3959 adds String.Pos.isValid.
- #3959 UTF-8 string validation.
- #3961 adds a model implementation for UTF-8 encoding and decoding.
IO
- #4097 adds IO.getTaskState which returns whether a task is finished, actively running, or waiting on other Tasks to finish.
Refactors
- #3605 reduces imports for Init.Data.Nat and Init.Data.Int.
- #3613 reduces imports for Init.Omega.Int.
- #3634 upstreams Std.Data.Nat and #3635 upstreams Std.Data.Int.
- #3790 reduces more imports for omega.
- #3694 extends GetElem interface with getElem! and getElem? to simplify containers like RBMap.
- #3865 renames Option.toMonad (see breaking changes below).
- #3882 unifies lexOrd with compareLex.
Other fixes or improvements
- #3765 makes Quotient.sound be a theorem.
- #3645 fixes System.FilePath.parent in the case of absolute paths.
- #3660 ByteArray.toUInt64LE! and ByteArray.toUInt64BE! were swapped.
- #3881, #3887 fix linearity issues in HashMap.insertIfNew, HashSet.erase, and HashMap.erase. The HashMap.insertIfNew fix improves import performance.
- #3830 ensures linearity in Parsec.many*Core.
- #3930 adds FS.Stream.isTty field.
- #3866 deprecates Option.toBool in favor of Option.isSome.
- #3975 upstreams Data.List.Init and Data.Array.Init material from Std.
- #3942 adds instances that make ac_rfl work without Mathlib.
- #4010 changes Fin.induction to use structural induction.
- 02753f fixes bug in reduceLeDiff simproc.
- #4097 adds IO.TaskState and IO.getTaskState to get the task from the Lean runtime's task manager.
Docs: #3615, #3664, #3707, #3734, #3868, #3861, #3869, #3858, #3856, #3857, #3867, #3864, #3860, #3859, #3871, #3919.

Lean internals

Defeq and WHNF algorithms
- #3616 gives better support for reducing Nat.rec expressions.
- #3774 add tracing for "non-easy" WHNF cases.
- #3807 fixes an isDefEq performance issue, now trying structure eta after lazy delta reduction.
- #3816 fixes .yesWithDeltaI behavior to prevent increasing transparency level when reducing projections.
- #3837 improves heuristic at isDefEq.
- #3965 improves isDefEq for constraints of the form t.i =?= s.i.
- #3977 improves isDefEqProj.
- #3981 adds universe constraint approximations to be able to solve u =?= max u ?v using ?v = u. These approximations are only applied when universe constraints cannot be postponed anymore.
- #4004 improves isDefEqProj during typeclass resolution.
- #4012 adds backward.isDefEq.lazyProjDelta and backward.isDefEq.lazyWhnfCore backwards compatibility flags.
Kernel
- #3966 removes dead code.
- #4035 fixes mismatch for TheoremVal between Lean and C++.
Discrimination trees
- 423fed and 3218b2: simplify handling of dependent/non-dependent pi types.
Typeclass instance synthesis
- #3638 eta-reduces synthesized instances
- ce350f fixes a linearity issue
- 917a31 improves performance by considering at most one answer for subgoals not containing metavariables. #4008 adds backward.synthInstance.canonInstances backward compatibility flag.
Definition processing
- #3661, #3767 changes automatically generated equational theorems to be named using suffix .eq_<idx> instead of ._eq_<idx>, and .eq_def instead of ._unfold. (See breaking changes below.) #3675 adds a mechanism to reserve names. #3803 fixes reserved name resolution inside namespaces and fixes handling of matcher declarations and equation lemmas.
- #3662 causes auxiliary definitions nested inside theorems to become defs if they are not proofs.
- #4006 makes proposition fields of structures be theorems.
- #4018 makes it an error for a theorem to be extern.
- #4047 improves performance making equations for well-founded recursive definitions.
Refactors
- #3614 avoids unfolding in Lean.Meta.evalNat.
- #3621 centralizes functionality for Fix/GuessLex/FunInd in the ArgsPacker module.
- #3186 rewrites the UnusedVariable linter to be more performant.
- #3589 removes coercion from String to Name (see breaking changes below).
- #3237 removes the lines field from FileMap.
- #3951 makes msg parameter to throwTacticEx optional.
Diagnostics
- #4016, #4019, #4020, #4030, #4031, c3714b, #4049 adds set_option diagnostics true for diagnostic counters. Tracks number of unfolded declarations, instances, reducible declarations, used instances, recursor reductions, isDefEq heuristic applications, among others. This option is suggested in exceptional situations, such as at deterministic timeout and maximum recursion depth.
- 283587 adds diagnostic information for simp.
- #4043 adds diagnostic information for congruence theorems.
- #4048 display diagnostic information for set_option diagnostics true in <tactic> and set_option diagnostics true in <term>.
Other features
- #3800 adds environment extension to record which definitions use structural or well-founded recursion.
- #3801 trace.profiler can now export to Firefox Profiler.
- #3918, #3953 adds @[builtin_doc] attribute to make docs and location of a declaration available as a builtin.
- #3939 adds the lean --json CLI option to print messages as JSON.
- #3075 improves test_extern command.
- #3970 gives monadic generalization of FindExpr.
Docs: #3743, #3921, #3954.
Other fixes: #3622, #3726, #3823, #3897, #3964, #3946, #4007, #4026.

Compiler, runtime, and FFI

#3632 makes it possible to allocate and free thread-local runtime resources for threads not started by Lean itself.
#3627 improves error message about compacting closures.
#3692 fixes deadlock in IO.Promise.resolve.
#3753 catches error code from MoveFileEx on Windows.
#4028 fixes a double reset bug in ResetReuse transformation.
6e731b removes interpreter copy constructor to avoid potential memory safety issues.

Lake

TOML Lake configurations. #3298, #4104.

Lake packages can now use TOML as a alternative configuration file format instead of Lean. If the default lakefile.lean is missing, Lake will also look for a lakefile.toml. The TOML version of the configuration supports a restricted set of the Lake configuration options, only including those which can easily mapped to a TOML data structure. The TOML syntax itself fully compiles with the TOML v1.0.0 specification.

As part of the introduction of this new feature, we have been helping maintainers of some major packages within the ecosystem switch to this format. For example, the following is Aesop's new lakefile.toml:

leanprover-community/aesop/lakefile.toml
```
name = "aesop"
defaultTargets = ["Aesop"]
testRunner = "test"
precompileModules = false

[[require]]
name = "batteries"
git = "https://github.com/leanprover-community/batteries"
rev = "main"

[[lean_lib]]
name = "Aesop"

[[lean_lib]]
name = "AesopTest"
globs = ["AesopTest.+"]
leanOptions = {linter.unusedVariables = false}

[[lean_exe]]
name = "test"
srcDir = "scripts"
```
To assist users who wish to transition their packages between configuration file formats, there is also a new lake translate-config command for migrating to/from TOML.

Running lake translate-config toml will produce a lakefile.toml version of a package's lakefile.lean. Any configuration options unsupported by the TOML format will be discarded during translation, but the original lakefile.lean will remain so that you can verify the translation looks good before deleting it.
Build progress overhaul. #3835, #4115, #4127, #4220, #4232, #4236.

Builds are now managed by a top-level Lake build monitor, this makes the output of Lake builds more standardized and enables producing prettier and more configurable progress reports.

As part of this change, job isolation has improved. Stray I/O and other build related errors in custom targets are now properly isolated and caught as part of their job. Import errors no longer cause Lake to abort the entire build and are instead localized to the build jobs of the modules in question.

Lake also now uses ANSI escape sequences to add color and produce progress lines that update in-place; this can be toggled on and off using --ansi / --no-ansi.

--wfail and --iofail options have been added that causes a build to fail if any of the jobs log a warning (--wfail) or produce any output or log information messages (--iofail). Unlike some other build systems, these options do NOT convert these logs into errors, and Lake does not abort jobs on such a log (i.e., dependent jobs will still continue unimpeded).
lake test. #3779.

Lake now has a built-in test command which will run a script or executable labelled @[test_runner] (in Lean) or defined as the testRunner (in TOML) in the root package.

Lake also provides a lake check-test command which will exit with code 0 if the package has a properly configured test runner or error with 1 otherwise.
lake lean. #3793.

The new command lake lean <file> [-- <args...>] functions like lake env lean <file> <args...>, except that it builds the imports of file before running lean. This makes it very useful for running test or example code that imports modules that are not guaranteed to have been built beforehand.
Miscellaneous bug fixes and improvements
- #3609 LEAN_GITHASH environment variable to override the detected Git hash for Lean when computing traces, useful for testing custom builds of Lean.
- #3795 improves relative package directory path normalization in the pre-rename check.
- #3957 fixes handling of packages that appear multiple times in a dependency tree.
- #3999 makes it an error for there to be a mismatch between a package name and what it is required as. Also adds a special message for the std-to-batteries rename.
- #4033 fixes quiet mode.
Docs: #3704.

DevOps

#3536 and #3833 add a checklist for the release process.
#3600 runs nix-ci more uniformly.
#3612 avoids argument limits when building on Windows.
#3682 builds Lean's .o files in parallel to rest of core.
#3601 changes the way Lean is built on Windows (see breaking changes below). As a result, Lake now dynamically links executables with supportInterpreter := true on Windows to libleanshared.dll and libInit_shared.dll. Therefore, such executables will not run unless those shared libraries are co-located with the executables or part of PATH. Running the executable via lake exe will ensure these libraries are part of PATH.

In a related change, the signature of the nativeFacets Lake configuration options has changed from a static Array to a function (shouldExport : Bool) → Array. See its docstring or Lake's README for further details on the changed option.
#3690 marks "Build matrix complete" as canceled if the build is canceled.
#3700, #3702, #3701, #3834, #3923: fixes and improvements for std and mathlib CI.
#3712 fixes nix build . on macOS.
#3717 replaces shell.nix in devShell with flake.nix.
#3715 and #3790 add test result summaries.
#3971 prevents stage0 changes via the merge queue.
#3979 adds handling for changes-stage0 label.
#3952 adds a script to summarize GitHub issues.
18a699 fixes asan linking

Breaking changes

Due to the major Lake build refactor, code using the affected parts of the Lake API or relying on the previous output format of Lake builds is likely to have been broken. We have tried to minimize the breakages and, where possible, old definitions have been marked @[deprecated] with a reference to the new alternative.
Executables configured with supportInterpreter := true on Windows should now be run via lake exe to function properly.
Automatically generated equational theorems are now named using suffix .eq_<idx> instead of ._eq_<idx>, and .eq_def instead of ._unfold. Example:

def fact : Nat → Nat
  | 0 => 1
  | n+1 => (n+1) * fact n

theorem ex : fact 0 = 1 := by unfold fact; decide

#check fact.eq_1
-- fact.eq_1 : fact 0 = 1

#check fact.eq_2
-- fact.eq_2 (n : Nat) : fact (Nat.succ n) = (n + 1) * fact n

#check fact.eq_def
/-
fact.eq_def :
  ∀ (x : Nat),
    fact x =
      match x with
      | 0 => 1
      | Nat.succ n => (n + 1) * fact n
-/

The coercion from String to Name was removed. Previously, it was Name.mkSimple, which does not separate strings at dots, but experience showed that this is not always the desired coercion. For the previous behavior, manually insert a call to Name.mkSimple.
The Subarray fields as, h₁ and h₂ have been renamed to array, start_le_stop, and stop_le_array_size, respectively. This more closely follows standard Lean conventions. Deprecated aliases for the field projections were added; these will be removed in a future release.
The change to the instance name algorithm (described above) can break projects that made use of the auto-generated names.
Option.toMonad has been renamed to Option.getM and the unneeded [Monad m] instance argument has been removed.

v4.7.0

simp and rw now use instance arguments found by unification, rather than always resynthesizing. For backwards compatibility, the original behaviour is available via set_option tactic.skipAssignedInstances false. #3507 and #3509.
When the pp.proofs is false, now omitted proofs use ⋯ rather than _, which gives a more helpful error message when copied from the Infoview. The pp.proofs.threshold option lets small proofs always be pretty printed. #3241.
pp.proofs.withType is now set to false by default to reduce noise in the info view.
The pretty printer for applications now handles the case of over-application itself when applying app unexpanders. In particular, the | `($_ $a $b $xs*) => `(($a + $b) $xs*) case of an app_unexpander is no longer necessary. #3495.

New simp (and dsimp) configuration option: zetaDelta. It is false by default. The zeta option is still true by default, but their meaning has changed.

When zeta := true, simp and dsimp reduce terms of the form let x := val; e[x] into e[val].
When zetaDelta := true, simp and dsimp will expand let-variables in the context. For example, suppose the context contains x := val. Then, any occurrence of x is replaced with val.

See issue #2682 for additional details. Here are some examples:

example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
  intro x
  simp
  /-
  New goal:
  h : z = 9; x := 5 |- x + 4 = z
  -/
  rw [h]

example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
  intro x
  -- Using both `zeta` and `zetaDelta`.
  simp (config := { zetaDelta := true })
  /-
  New goal:
  h : z = 9; x := 5 |- 9 = z
  -/
  rw [h]

example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
  intro x
  simp [x] -- asks `simp` to unfold `x`
  /-
  New goal:
  h : z = 9; x := 5 |- 9 = z
  -/
  rw [h]

example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
  intro x
  simp (config := { zetaDelta := true, zeta := false })
  /-
  New goal:
  h : z = 9; x := 5 |- let y := 4; 5 + y = z
  -/
  rw [h]

When adding new local theorems to simp, the system assumes that the function application arguments have been annotated with no_index. This modification, which addresses issue #2670, restores the Lean 3 behavior that users expect. With this modification, the following examples are now operational:
```
example {α β : Type} {f : α × β → β → β} (h : ∀ p : α × β, f p p.2 = p.2)
  (a : α) (b : β) : f (a, b) b = b := by
  simp [h]

example {α β : Type} {f : α × β → β → β}
  (a : α) (b : β) (h : f (a,b) (a,b).2 = (a,b).2) : f (a, b) b = b := by
  simp [h]
```
In both cases, h is applicable because simp does not index f-arguments anymore when adding h to the simp-set. It's important to note, however, that global theorems continue to be indexed in the usual manner.
Improved the error messages produced by the decide tactic. #3422
Improved auto-completion performance. #3460
Improved initial language server startup performance. #3552
Changed call hierarchy to sort entries and strip private header from names displayed in the call hierarchy. #3482
There is now a low-level error recovery combinator in the parsing framework, primarily intended for DSLs. #3413
You can now write termination_by? after a declaration to see the automatically inferred termination argument, and turn it into a termination_by … clause using the “Try this” widget or a code action. #3514
A large fraction of Std has been moved into the Lean repository. This was motivated by:
1. Making universally useful tactics such as ext, by_cases, change at, norm_cast, rcases, simpa, simp?, omega, and exact? available to all users of Lean, without imports.
2. Minimizing the syntactic changes between plain Lean and Lean with import Std.
3. Simplifying the development process for the basic data types Nat, Int, Fin (and variants such as UInt64), List, Array, and BitVec as we begin making the APIs and simp normal forms for these types more complete and consistent.
4. Laying the groundwork for the Std roadmap, as a library focused on essential datatypes not provided by the core langauge (e.g. RBMap) and utilities such as basic IO. While we have achieved most of our initial aims in v4.7.0-rc1, some upstreaming will continue over the coming months.
The / and % notations in Int now use Int.ediv and Int.emod (i.e. the rounding conventions have changed). Previously Std overrode these notations, so this is no change for users of Std. There is now kernel support for these functions. #3376.
omega, our integer linear arithmetic tactic, is now availabe in the core langauge.
- It is supplemented by a preprocessing tactic bv_omega which can solve goals about BitVec which naturally translate into linear arithmetic problems. #3435.
- omega now has support for Fin #3427, the <<< operator #3433.
- During the port omega was modified to no longer identify atoms up to definitional equality (so in particular it can no longer prove id x ≤ x). #3525. This may cause some regressions. We plan to provide a general purpose preprocessing tactic later, or an omega! mode.
- omega is now invoked in Lean's automation for termination proofs #3503 as well as in array indexing proofs #3515. This automation will be substantially revised in the medium term, and while omega does help automate some proofs, we plan to make this much more robust.
The library search tactics exact? and apply? that were originally in Mathlib are now available in Lean itself. These use the implementation using lazy discrimination trees from Std, and thus do not require a disk cache but have a slightly longer startup time. The order used for selection lemmas has changed as well to favor goals purely based on how many terms in the head pattern match the current goal.
The solve_by_elim tactic has been ported from Std to Lean so that library search can use it.
New #check_tactic and #check_simp commands have been added. These are useful for checking tactics (particularly simp) behave as expected in test suites.
Previously, app unexpanders would only be applied to entire applications. However, some notations produce functions, and these functions can be given additional arguments. The solution so far has been to write app unexpanders so that they can take an arbitrary number of additional arguments. However this leads to misleading hover information in the Infoview. For example, while HAdd.hAdd f g 1 pretty prints as (f + g) 1, hovering over f + g shows f. There is no way to fix the situation from within an app unexpander; the expression position for HAdd.hAdd f g is absent, and app unexpanders cannot register TermInfo.

This commit changes the app delaborator to try running app unexpanders on every prefix of an application, from longest to shortest prefix. For efficiency, it is careful to only try this when app delaborators do in fact exist for the head constant, and it also ensures arguments are only delaborated once. Then, in (f + g) 1, the f + g gets TermInfo registered for that subexpression, making it properly hoverable.

#3375

Breaking changes:

Lean.withTraceNode and variants got a stronger MonadAlwaysExcept assumption to fix trace trees not being built on elaboration runtime exceptions. Instances for most elaboration monads built on EIO Exception should be synthesized automatically.
The match ... with. and fun. notations previously in Std have been replaced by nomatch ... and nofun. #3279 and #3286

Other improvements:

several bug fixes for simp:
- we should not crash when simp loops #3269
- simp gets stuck on autoParam #3315
- simp fails when custom discharger makes no progress #3317
- simp fails to discharge autoParam premises even when it can reduce them to True #3314
- simp? suggests generated equations lemma names, fixes #3547 #3573
fixes for match expressions:
- fix regression with builtin literals #3521
- accept match when patterns cover all cases of a BitVec finite type #3538
- fix matching Int literals #3504
- patterns containing int values and constructors #3496
improve termination_by error messages #3255
fix rename_i in macros, fixes #3553 #3581
fix excessive resource usage in generalize, fixes #3524 #3575
an equation lemma with autoParam arguments fails to rewrite, fixing #2243 #3316
add_decl_doc should check that declarations are local #3311
instantiate the types of inductives with the right parameters, closing #3242 #3246
New simprocs for many basic types. #3407

Lake fixes:

Warn on fetch cloud release failure #3401
Cloud release trace & lake build :release errors #3248

v4.6.1

Backport of #3552 fixing a performance regression in server startup.

v4.6.0

Add custom simplification procedures (aka simprocs) to simp. Simprocs can be triggered by the simplifier on a specified term-pattern. Here is an small example:

import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat

def foo (x : Nat) : Nat :=
  x + 10

/--
The `simproc` `reduceFoo` is invoked on terms that match the pattern `foo _`.
-/
simproc reduceFoo (foo _) :=
  /- A term of type `Expr → SimpM Step -/
  fun e => do
    /-
    The `Step` type has three constructors: `.done`, `.visit`, `.continue`.
    * The constructor `.done` instructs `simp` that the result does
      not need to be simplied further.
    * The constructor `.visit` instructs `simp` to visit the resulting expression.
    * The constructor `.continue` instructs `simp` to try other simplification procedures.

    All three constructors take a `Result`. The `.continue` contructor may also take `none`.
    `Result` has two fields `expr` (the new expression), and `proof?` (an optional proof).
     If the new expression is definitionally equal to the input one, then `proof?` can be omitted or set to `none`.
    -/
    /- `simp` uses matching modulo reducibility. So, we ensure the term is a `foo`-application. -/
    unless e.isAppOfArity ``foo 1 do
      return .continue
    /- `Nat.fromExpr?` tries to convert an expression into a `Nat` value -/
    let some n ← Nat.fromExpr? e.appArg!
      | return .continue
    return .done { expr := Lean.mkNatLit (n+10) }

We disable simprocs support by using the command set_option simprocs false. This command is particularly useful when porting files to v4.6.0. Simprocs can be scoped, manually added to simp commands, and suppressed using -. They are also supported by simp?. simp only does not execute any simproc. Here are some examples for the simproc defined above.

example : x + foo 2 = 12 + x := by
  set_option simprocs false in
    /- This `simp` command does not make progress since `simproc`s are disabled. -/
    fail_if_success simp
  simp_arith

example : x + foo 2 = 12 + x := by
  /- `simp only` must not use the default simproc set. -/
  fail_if_success simp only
  simp_arith

example : x + foo 2 = 12 + x := by
  /-
  `simp only` does not use the default simproc set,
  but we can provide simprocs as arguments. -/
  simp only [reduceFoo]
  simp_arith

example : x + foo 2 = 12 + x := by
  /- We can use `-` to disable `simproc`s. -/
  fail_if_success simp [-reduceFoo]
  simp_arith

The command register_simp_attr <id> now creates a simp and a simproc set with the name <id>. The following command instructs Lean to insert the reduceFoo simplification procedure into the set my_simp. If no set is specified, Lean uses the default simp set.

simproc [my_simp] reduceFoo (foo _) := ...

The syntax of the termination_by and decreasing_by termination hints is overhauled:
- They are now placed directly after the function they apply to, instead of after the whole mutual block.
- Therefore, the function name no longer has to be mentioned in the hint.
- If the function has a where clause, the termination_by and decreasing_by for that function come before the where. The functions in the where clause can have their own termination hints, each following the corresponding definition.
- The termination_by clause can only bind “extra parameters”, that are not already bound by the function header, but are bound in a lambda (:= fun x y z =>) or in patterns (| x, n + 1 => …). These extra parameters used to be understood as a suffix of the function parameters; now it is a prefix.
Migration guide: In simple cases just remove the function name, and any variables already bound at the header.
```
 def foo : Nat → Nat → Nat := …
-termination_by foo a b => a - b
+termination_by a b => a - b
```
or
```
 def foo : Nat → Nat → Nat := …
-termination_by _ a b => a - b
+termination_by a b => a - b
```
If the parameters are bound in the function header (before the :), remove them as well:
```
 def foo (a b : Nat) : Nat := …
-termination_by foo a b => a - b
+termination_by a - b
```
Else, if there are multiple extra parameters, make sure to refer to the right ones; the bound variables are interpreted from left to right, no longer from right to left:
```
 def foo : Nat → Nat → Nat → Nat
   | a, b, c => …
-termination_by foo b c => b
+termination_by a b => b
```
In the case of a mutual block, place the termination arguments (without the function name) next to the function definition:
```
-mutual
-def foo : Nat → Nat → Nat := …
-def bar : Nat → Nat := …
-end
-termination_by
-  foo a b => a - b
-  bar a => a
+mutual
+def foo : Nat → Nat → Nat := …
+termination_by a b => a - b
+def bar : Nat → Nat := …
+termination_by a => a
+end
```
Similarly, if you have (mutual) recursion through where or let rec, the termination hints are now placed directly after the function they apply to:
```
-def foo (a b : Nat) : Nat := …
-  where bar (x : Nat) : Nat := …
-termination_by
-  foo a b => a - b
-  bar x => x
+def foo (a b : Nat) : Nat := …
+termination_by a - b
+  where
+    bar (x : Nat) : Nat := …
+    termination_by x

-def foo (a b : Nat) : Nat :=
-  let rec bar (x : Nat) :  Nat := …
-  …
-termination_by
-  foo a b => a - b
-  bar x => x
+def foo (a b : Nat) : Nat :=
+  let rec bar (x : Nat) : Nat := …
+    termination_by x
+  …
+termination_by a - b
```
In cases where a single decreasing_by clause applied to multiple mutually recursive functions before, the tactic now has to be duplicated.
The semantics of decreasing_by changed; the tactic is applied to all termination proof goals together, not individually.

This helps when writing termination proofs interactively, as one can focus each subgoal individually, for example using ·. Previously, the given tactic script had to work for all goals, and one had to resort to tactic combinators like first:
```
 def foo (n : Nat) := … foo e1 … foo e2 …
-decreasing_by
-simp_wf
-first | apply something_about_e1; …
-      | apply something_about_e2; …
+decreasing_by
+all_goals simp_wf
+· apply something_about_e1; …
+· apply something_about_e2; …
```
To obtain the old behaviour of applying a tactic to each goal individually, use all_goals:
```
 def foo (n : Nat) := …
-decreasing_by some_tactic
+decreasing_by all_goals some_tactic
```
In the case of mutual recursion each decreasing_by now applies to just its function. If some functions in a recursive group do not have their own decreasing_by, the default decreasing_tactic is used. If the same tactic ought to be applied to multiple functions, the decreasing_by clause has to be repeated at each of these functions.
Modify InfoTree.context to facilitate augmenting it with partial contexts while elaborating a command. This breaks backwards compatibility with all downstream projects that traverse the InfoTree manually instead of going through the functions in InfoUtils.lean, as well as those manually creating and saving InfoTrees. See PR #3159 for how to migrate your code.
Add language server support for call hierarchy requests (PR #3082). The change to the .ilean format in this PR means that projects must be fully rebuilt once in order to generate .ilean files with the new format before features like "find references" work correctly again.
Structure instances with multiple sources (for example {a, b, c with x := 0}) now have their fields filled from these sources in strict left-to-right order. Furthermore, the structure instance elaborator now aggressively use sources to fill in subobject fields, which prevents unnecessary eta expansion of the sources, and hence greatly reduces the reliance on costly structure eta reduction. This has a large impact on mathlib, reducing total CPU instructions by 3% and enabling impactful refactors like leanprover-community/mathlib4#8386 which reduces the build time by almost 20%. See PR #2478 and RFC #2451.
Add pretty printer settings to omit deeply nested terms (pp.deepTerms false and pp.deepTerms.threshold) (PR #3201)
Add pretty printer options pp.numeralTypes and pp.natLit. When pp.numeralTypes is true, then natural number literals, integer literals, and rational number literals are pretty printed with type ascriptions, such as (2 : Rat), (-2 : Rat), and (-2 / 3 : Rat). When pp.natLit is true, then raw natural number literals are pretty printed as nat_lit 2. PR #2933 and RFC #3021.

Lake updates:

improved platform information & control #3226
lake update from unsupported manifest versions #3149

Other improvements:

make intro be aware of let_fun #3115
produce simpler proof terms in rw #3121
fuse nested mkCongrArg calls in proofs generated by simp #3203
induction using followed by a general term #3188
allow generalization in let #3060, fixing #3065
reducing out-of-bounds swap! should return a, not `default`` #3197, fixing #3196
derive BEq on structure with Prop-fields #3191, fixing #3140
refine through more casesOnApp/matcherApp #3176, fixing #3175
do not strip dotted components from lean module names #2994, fixing #2999
fix deriving only deriving the first declaration for some handlers #3058, fixing #3057
do not instantiate metavariables in kabstract/rw for disallowed occurrences #2539, fixing #2538
hover info for cases h : ... #3084

v4.5.0

Modify the lexical syntax of string literals to have string gaps, which are escape sequences of the form "\" newline whitespace*. These have the interpetation of an empty string and allow a string to flow across multiple lines without introducing additional whitespace. The following is equivalent to "this is a string".
```
"this is \
   a string"
```
PR #2821 and RFC #2838.
Add raw string literal syntax. For example, r"\n" is equivalent to "\\n", with no escape processing. To include double quote characters in a raw string one can add sufficiently many # characters before and after the bounding "s, as in r#"the "the" is in quotes"# for "the \"the\" is in quotes". PR #2929 and issue #1422.
The low-level termination_by' clause is no longer supported.

Migration guide: Use termination_by instead, e.g.:
```
-termination_by' measure (fun ⟨i, _⟩ => as.size - i)
+termination_by i _ => as.size - i
```
If the well-founded relation you want to use is not the one that the WellFoundedRelation type class would infer for your termination argument, you can use WellFounded.wrap from the std libarary to explicitly give one:
```
-termination_by' ⟨r, hwf⟩
+termination_by x => hwf.wrap x
```
Support snippet edits in LSP TextEdits. See Lean.Lsp.SnippetString for more details.
Deprecations and changes in the widget API.
- Widget.UserWidgetDefinition is deprecated in favour of Widget.Module. The annotation @[widget] is deprecated in favour of @[widget_module]. To migrate a definition of type UserWidgetDefinition, remove the name field and replace the type with Widget.Module. Removing the name results in a title bar no longer being drawn above your panel widget. To add it back, draw it as part of the component using <details open=true><summary class='mv2 pointer'>{name}</summary>{rest_of_widget}</details>. See an example migration here.
- The new command show_panel_widgets allows displaying always-on and locally-on panel widgets.
- RpcEncodable widget props can now be stored in the infotree.
- See RFC 2963 for more details and motivation.
If no usable lexicographic order can be found automatically for a termination proof, explain why. See feat: GuessLex: if no measure is found, explain why.
Option to print inferred termination argument. With set_option showInferredTerminationBy true you will get messages like
```
Inferred termination argument:
termination_by
ackermann n m => (sizeOf n, sizeOf m)
```
for automatically generated termination_by clauses.
More detailed error messages for invalid mutual blocks.
Multiple improvements to the output of simp? and simp_all?.
Tactics with withLocation * no longer fail if they close the main goal.
Implementation of a test_extern command for writing tests for @[extern] and @[implemented_by] functions. Usage is
```
import Lean.Util.TestExtern

test_extern Nat.add 17 37
```
The head symbol must be the constant with the @[extern] or @[implemented_by] attribute. The return type must have a DecidableEq instance.

Bug fixes for #2853, #2953, #2966, #2971, #2990, #3094.

Bug fix for eager evaluation of default value in Option.getD. Avoid panic in leanPosToLspPos when file source is unavailable. Improve short-circuiting behavior for List.all and List.any.

Several Lake bug fixes: #3036, #3064, #3069.

v4.4.0

Lake and the language server now support per-package server options using the moreServerOptions config field, as well as options that apply to both the language server and lean using the leanOptions config field. Setting either of these fields instead of moreServerArgs ensures that viewing files from a dependency uses the options for that dependency. Additionally, moreServerArgs is being deprecated in favor of the moreGlobalServerArgs field. See PR #2858.

A Lakefile with the following deprecated package declaration:
```
def moreServerArgs := #[
  "-Dpp.unicode.fun=true"
]
def moreLeanArgs := moreServerArgs

package SomePackage where
  moreServerArgs := moreServerArgs
  moreLeanArgs := moreLeanArgs
```
... can be updated to the following package declaration to use per-package options:
```
package SomePackage where
  leanOptions := #[⟨`pp.unicode.fun, true⟩]
```
Rename request handler.
Import auto-completion.
`pp.beta`` to apply beta reduction when pretty printing.
Embed and check githash in .olean.
Guess lexicographic order for well-founded recursion.
Allow trailing comma in tuples, lists, and tactics.

Bug fixes for #2628, #2883, #2810, #2925, and #2914.

Lake:

lake init . and a bare lake init and will now use the current directory as the package name. #2890
lake new and lake init will now produce errors on invalid package names such as .., foo/bar, Init, Lean, Lake, and Main. See issue #2637 and PR #2890.
lean_lib no longer converts its name to upper camel case (e.g., lean_lib bar will include modules named bar.* rather than Bar.*). See issue #2567 and PR #2889.
Lean and Lake now properly support non-identifier library names (e.g., lake new 123-hello and import «123Hello» now work correctly). See issue #2865 and PR #2889.
Lake now filters the environment extensions loaded from a compiled configuration (lakefile.olean) to include only those relevant to Lake's workspace loading process. This resolves segmentation faults caused by environment extension type mismatches (e.g., when defining custom elaborators via elab in configurations). See issue #2632 and PR #2896.
Cloud releases will now properly be re-unpacked if the build directory is removed. See PR #2928.
Lake's math template has been simplified. See PR #2930.
lake exe <target> now parses target like a build target (as the help text states it should) rather than as a basic name. For example, lake exe @mathlib/runLinter should now work. See PR #2932.
lake new foo.bar [std] now generates executables named foo-bar and lake new foo.bar exe properly creates foo/bar.lean. See PR #2932.
Later packages and libraries in the dependency tree are now preferred over earlier ones. That is, the later ones "shadow" the earlier ones. Such an ordering is more consistent with how declarations generally work in programming languages. This will break any package that relied on the previous ordering. See issue #2548 and PR #2937.
Executable roots are no longer mistakenly treated as importable. They will no longer be picked up by findModule?. See PR #2937.

v4.3.0

simp [f] does not unfold partial applications of f anymore. See issue #2042. To fix proofs affected by this change, use unfold f or simp (config := { unfoldPartialApp := true }) [f].
By default, simp will no longer try to use Decidable instances to rewrite terms. In particular, not all decidable goals will be closed by simp, and the decide tactic may be useful in such cases. The decide simp configuration option can be used to locally restore the old simp behavior, as in simp (config := {decide := true}); this includes using Decidable instances to verify side goals such as numeric inequalities.
Many bug fixes:
Cancel outstanding tasks on document edit in the language server.
Remove unnecessary % operations in Fin.mod and Fin.div
Avoid DecidableEq in Array.mem
Ensure USize.size unifies with ?m + 1
Improve compatibility with emacs eglot client

Lake:

Sensible defaults for lake new MyProject math
Changed postUpdate? configuration option to a post_update declaration. See the post_update syntax docstring for more information on the new syntax.
A manifest is automatically created on workspace load if one does not exists..
The := syntax for configuration declarations (i.e., package, lean_lib, and lean_exe) has been deprecated. For example, package foo := {...} is deprecated.
support for overriding package URLs via LAKE_PKG_URL_MAP
Moved the default build directory (e.g., build), default packages directory (e.g., lake-packages), and the compiled configuration (e.g., lakefile.olean) into a new dedicated directory for Lake outputs, .lake. The cloud release build archives are also stored here, fixing #2713.
Update manifest format to version 7 (see lean4#2801 for details on the changes).
Deprecate the manifestFile field of a package configuration.
There is now a more rigorous check on lakefile.olean compatibility (see #2842 for more details).

v4.2.0

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).

v4.1.0

The error positioning on missing tokens has been improved. In particular, this should make it easier to spot errors in incomplete tactic proofs.
After elaborating a configuration file, Lake will now cache the configuration to a lakefile.olean. Subsequent runs of Lake will import this OLean instead of elaborating the configuration file. This provides a significant performance improvement (benchmarks indicate that using the OLean cuts Lake's startup time in half), but there are some important details to keep in mind:
- Lake will regenerate this OLean after each modification to the lakefile.lean or lean-toolchain. You can also force a reconfigure by passing the new --reconfigure / -R option to lake.
- Lake configuration options (i.e., -K) will be fixed at the moment of elaboration. Setting these options when lake is using the cached configuration will have no effect. To change options, run lake with -R / --reconfigure.
- The lakefile.olean is a local configuration and should not be committed to Git. Therefore, existing Lake packages need to add it to their .gitignore.
The signature of Lake.buildO has changed, args has been split into weakArgs and traceArgs. traceArgs are included in the input trace and weakArgs are not. See Lake's FFI example for a demonstration of how to adapt to this change.
The signatures of Lean.importModules, Lean.Elab.headerToImports, and Lean.Elab.parseImports have changed from taking List Import to Array Import.
There is now an occs field in the configuration object for the rewrite tactic, allowing control of which occurrences of a pattern should be rewritten. This was previously a separate argument for Lean.MVarId.rewrite, and this has been removed in favour of an additional field of Rewrite.Config. It was not previously accessible from user tactics.

v4.0.0

Lean.Meta.getConst? has been renamed. We have renamed getConst? to getUnfoldableConst? (and getConstNoEx? to getUnfoldableConstNoEx?). These were not intended to be part of the public API, but downstream projects had been using them (sometimes expecting different behaviour) incorrectly instead of Lean.getConstInfo.
dsimp / simp / simp_all now fail by default if they make no progress.

This can be overridden with the (config := { failIfUnchanged := false }) option. This change was made to ease manual use of simp (with complicated goals it can be hard to tell if it was effective) and to allow easier flow control in tactics internally using simp. See the summary discussion on zulip for more details.
simp_all now preserves order of hypotheses.

In order to support the failIfUnchanged configuration option for dsimp / simp / simp_all the way simp_all replaces hypotheses has changed. In particular it is now more likely to preserve the order of hypotheses. See simp_all reorders hypotheses unnecessarily. (Previously all non-dependent propositional hypotheses were reverted and reintroduced. Now only such hypotheses which were changed, or which come after a changed hypothesis, are reverted and reintroduced. This has the effect of preserving the ordering amongst the non-dependent propositional hypotheses, but now any dependent or non-propositional hypotheses retain their position amongst the unchanged non-dependent propositional hypotheses.) This may affect proofs that use rename_i, case ... =>, or next ... =>.
New have this implementation.

this is now a regular identifier again that is implicitly introduced by anonymous have := for the remainder of the tactic block. It used to be a keyword that was visible in all scopes and led to unexpected behavior when explicitly used as a binder name.
Show typeclass and tactic names in profile output.

Make calc require the sequence of relation/proof-s to have the same indentation, and add calc alternative syntax allowing underscores _ in the first relation.

The flexible indentation in calc was often used to align the relation symbols:

example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
  calc
      (x + y) * (x + y) = (x + y) * x + (x + y) * y       := by rw [Nat.mul_add]
                      -- improper indentation
                      _ = x * x + y * x + (x + y) * y     := by rw [Nat.add_mul]
                      _ = x * x + y * x + (x * y + y * y) := by rw [Nat.add_mul]
                      _ = x * x + y * x + x * y + y * y   := by rw [←Nat.add_assoc]

This is no longer legal. The new syntax puts the first term right after the calc and each step has the same indentation:

example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
  calc (x + y) * (x + y)
    _ = (x + y) * x + (x + y) * y       := by rw [Nat.mul_add]
    _ = x * x + y * x + (x + y) * y     := by rw [Nat.add_mul]
    _ = x * x + y * x + (x * y + y * y) := by rw [Nat.add_mul]
    _ = x * x + y * x + x * y + y * y   := by rw [←Nat.add_assoc]

Update Lake to latest prerelease.
Make go-to-definition on a typeclass projection application go to the instance(s).
Include timings in trace messages when profiler is true.
Pretty-print signatures in hover and #check <ident>.
Introduce parser memoization to avoid exponential behavior.
feat: allow doSeq in let x <- e | seq.
Add hover/go-to-def/refs for options.
Add empty type ascription syntax (e :).
Make tokens in <|> relevant to syntax match.
Add linter.deprecated option to silence deprecation warnings.
Improve fuzzy-matching heuristics.
Implementation-detail hypotheses.
Hover information for cases/induction case names.
Prefer longer parse even if unsuccessful.
Show declaration module in hover.
New conv mode structuring tactics.
simp can track information and can print an equivalent simp only. PR #1626.
Enforce uniform indentation in tactic blocks / do blocks. See issue #1606.
Moved AssocList, HashMap, HashSet, RBMap, RBSet, PersistentArray, PersistentHashMap, PersistentHashSet to the Lean package. The standard library contains versions that will evolve independently to simplify bootstrapping process.
Standard library moved to the std4 GitHub repository.
InteractiveGoals now has information that a client infoview can use to show what parts of the goal have changed after applying a tactic. PR #1610.
Add [inheritDoc] attribute. PR #1480.
Expose that panic = default. PR #1614.
New code generator project has started.
Remove description argument from register_simp_attr. PR #1566.
Additional concurrency primitives.
Collapsible traces with messages.
Hygienic resolution of namespaces.
New Float functions.
Many new doc strings have been added to declarations at Init.

v4.0.0-m5 (07 August 2022)

Update Lake to v4.0.0. See the v4.0.0 release notes for detailed changes.

Mutual declarations in different namespaces are now supported. Example:

mutual
  def Foo.boo (x : Nat) :=
    match x with
    | 0 => 1
    | x + 1 => 2*Boo.bla x

  def Boo.bla (x : Nat) :=
    match x with
    | 0 => 2
    | x+1 => 3*Foo.boo x
end

A namespace is automatically created for the common prefix. Example:

mutual
  def Tst.Foo.boo (x : Nat) := ...
  def Tst.Boo.bla (x : Nat) := ...
end

expands to

namespace Tst
mutual
  def Foo.boo (x : Nat) := ...
  def Boo.bla (x : Nat) := ...
end
end Tst

Allow users to install their own deriving handlers for existing type classes. See example at Simple.lean.
Add tactic congr (num)?. See doc string for additional details.
Missing doc linter
match-syntax notation now checks for unused alternatives. See issue #1371.
Auto-completion for structure instance fields. Example:
```
example : Nat × Nat := {
  f -- HERE
}
```
fst now appears in the list of auto-completion suggestions.
Auto-completion for dotted identifier notation. Example:
```
example : Nat :=
  .su -- HERE
```
succ now appears in the list of auto-completion suggestions.

nat_lit is not needed anymore when declaring OfNat instances. See issues #1389 and #875. Example:

inductive Bit where
  | zero
  | one

instance inst0 : OfNat Bit 0 where
  ofNat := Bit.zero

instance : OfNat Bit 1 where
  ofNat := Bit.one

example : Bit := 0
example : Bit := 1

Add [elabAsElim] attribute (it is called elab_as_eliminator in Lean 3). Motivation: simplify the Mathlib port to Lean 4.
Trans type class now accepts relations in Type u. See this Zulip issue.
Accept unescaped keywords as inductive constructor names. Escaping can often be avoided at use sites via dot notation.
```
inductive MyExpr
  | let : ...

def f : MyExpr → MyExpr
  | .let ... => .let ...
```
Throw an error message at parametric local instances such as [Nat -> Decidable p]. The type class resolution procedure cannot use this kind of local instance because the parameter does not have a forward dependency. This check can be disabled using set_option checkBinderAnnotations false.
Add option pp.showLetValues. When set to false, the info view hides the value of let-variables in a goal. By default, it is true when visualizing tactic goals, and false otherwise. See issue #1345 for additional details.
Add option warningAsError. When set to true, warning messages are treated as errors.

Support dotted notation and named arguments in patterns. Example:

def getForallBinderType (e : Expr) : Expr :=
  match e with
  | .forallE (binderType := type) .. => type
  | _ => panic! "forall expected"

"jump-to-definition" now works for function names embedded in the following attributes @[implementedBy funName], @[tactic parserName], @[termElab parserName], @[commandElab parserName], @[builtinTactic parserName], @[builtinTermElab parserName], and @[builtinCommandElab parserName]. See issue #1350.
Improve MVarId methods discoverability. See issue #1346. We still have to add similar methods for FVarId, LVarId, Expr, and other objects. Many existing methods have been marked as deprecated.

Add attribute [deprecated] for marking deprecated declarations. Examples:

def g (x : Nat) := x + 1

-- Whenever `f` is used, a warning message is generated suggesting to use `g` instead.
@[deprecated g]
def f (x : Nat) := x + 1

#check f 0 -- warning: `f` has been deprecated, use `g` instead

-- Whenever `h` is used, a warning message is generated.
@[deprecated]
def h (x : Nat) := x + 1

#check h 0 -- warning: `h` has been deprecated

Add type LevelMVarId (and abbreviation LMVarId) for universe level metavariable ids. Motivation: prevent meta-programmers from mixing up universe and expression metavariable ids.
Improve calc term and tactic. See issue #1342.
Relaxed antiquotation parsing further reduces the need for explicit $x:p antiquotation kind annotations.
Add support for computed fields in inductives. Example:
```
inductive Exp
  | var (i : Nat)
  | app (a b : Exp)
with
  @[computedField] hash : Exp → Nat
    | .var i => i
    | .app a b => a.hash * b.hash + 1
```
The result of the Exp.hash function is then stored as an extra "computed" field in the .var and .app constructors; Exp.hash accesses this field and thus runs in constant time (even on dag-like values).

Update a[i] notation. It is now based on the typeclass

class GetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) where
  getElem (xs : cont) (i : idx) (h : dom xs i) : Elem

The notation a[i] is now defined as follows

macro:max x:term noWs "[" i:term "]" : term => `(getElem $x $i (by get_elem_tactic))

The proof that i is a valid index is synthesized using the tactic get_elem_tactic. For example, the type Array α has the following instances

instance : GetElem (Array α) Nat α fun xs i => LT.lt i xs.size where ...
instance : GetElem (Array α) USize α fun xs i => LT.lt i.toNat xs.size where ...

You can use the notation a[i]'h to provide the proof manually. Two other notations were introduced: a[i]! and a[i]?, For a[i]!, a panic error message is produced at runtime if i is not a valid index. a[i]? has type Option α, and a[i]? evaluates to none if the index i is not valid. The three new notations are defined as follows:

@[inline] def getElem' [GetElem cont idx elem dom] (xs : cont) (i : idx) (h : dom xs i) : elem :=
getElem xs i h

@[inline] def getElem! [GetElem cont idx elem dom] [Inhabited elem] (xs : cont) (i : idx) [Decidable (dom xs i)] : elem :=
  if h : _ then getElem xs i h else panic! "index out of bounds"

@[inline] def getElem? [GetElem cont idx elem dom] (xs : cont) (i : idx) [Decidable (dom xs i)] : Option elem :=
  if h : _ then some (getElem xs i h) else none

macro:max x:term noWs "[" i:term "]" noWs "?" : term => `(getElem? $x $i)
macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
macro x:term noWs "[" i:term "]'" h:term:max : term => `(getElem' $x $i $h)

See discussion on Zulip. Examples:

example (a : Array Int) (i : Nat) : Int :=
  a[i] -- Error: failed to prove index is valid ...

example (a : Array Int) (i : Nat) (h : i < a.size) : Int :=
  a[i] -- Ok

example (a : Array Int) (i : Nat) : Int :=
  a[i]! -- Ok

example (a : Array Int) (i : Nat) : Option Int :=
  a[i]? -- Ok

example (a : Array Int) (h : a.size = 2) : Int :=
  a[0]'(by rw [h]; decide) -- Ok

example (a : Array Int) (h : a.size = 2) : Int :=
  have : 0 < a.size := by rw [h]; decide
  have : 1 < a.size := by rw [h]; decide
  a[0] + a[1] -- Ok

example (a : Array Int) (i : USize) (h : i.toNat < a.size) : Int :=
  a[i] -- Ok

The get_elem_tactic is defined as

macro "get_elem_tactic" : tactic =>
  `(first
    | get_elem_tactic_trivial
    | fail "failed to prove index is valid, ..."
   )

The get_elem_tactic_trivial auxiliary tactic can be extended using macro_rules. By default, it tries trivial, simp_arith, and a special case for Fin. In the future, it will also try linarith. You can extend get_elem_tactic_trivial using my_tactic as follows

macro_rules
| `(tactic| get_elem_tactic_trivial) => `(tactic| my_tactic)

Note that Idx's type in GetElem does not depend on Cont. So, you cannot write the instance instance : GetElem (Array α) (Fin ??) α fun xs i => ..., but the Lean library comes equipped with the following auxiliary instance:

instance [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
  getElem xs i h := getElem xs i.1 h

and helper tactic

macro_rules
| `(tactic| get_elem_tactic_trivial) => `(tactic| apply Fin.val_lt_of_le; get_elem_tactic_trivial; done)

Example:

example (a : Array Nat) (i : Fin a.size) :=
  a[i] -- Ok

example (a : Array Nat) (h : n ≤ a.size) (i : Fin n) :=
  a[i] -- Ok

Better support for qualified names in recursive declarations. The following is now supported:

namespace Nat
  def fact : Nat → Nat
  | 0 => 1
  | n+1 => (n+1) * Nat.fact n
end Nat

Add support for CommandElabM monad at #eval. Example:

import Lean

open Lean Elab Command

#eval do
  let id := mkIdent `foo
  elabCommand (← `(def $id := 10))

#eval foo -- 10

Try to elaborate do notation even if the expected type is not available. We still delay elaboration when the expected type is not available. This change is particularly useful when writing examples such as
```
#eval do
  IO.println "hello"
  IO.println "world"
```
That is, we don't have to use the idiom #eval show IO _ from do ... anymore. Note that auto monadic lifting is less effective when the expected type is not available. Monadic polymorphic functions (e.g., ST.Ref.get) also require the expected type.
On Linux, panics now print a backtrace by default, which can be disabled by setting the environment variable LEAN_BACKTRACE to 0. Other platforms are TBD.
The group(·) syntax combinator is now introduced automatically where necessary, such as when using multiple parsers inside (...)+.
Add "Typed Macros": syntax trees produced and accepted by syntax antiquotations now remember their syntax kinds, preventing accidental production of ill-formed syntax trees and reducing the need for explicit :kind antiquotation annotations. See PR for details.

Aliases of protected definitions are protected too. Example:

protected def Nat.double (x : Nat) := 2*x

namespace Ex
export Nat (double) -- Add alias Ex.double for Nat.double
end Ex

open Ex
#check Ex.double -- Ok
#check double -- Error, `Ex.double` is alias for `Nat.double` which is protected

Use IO.getRandomBytes to initialize random seed for IO.rand. See discussion at this PR.

Improve dot notation and aliases interaction. See discussion on Zulip for additional details. Example:

def Set (α : Type) := α → Prop
def Set.union (s₁ s₂ : Set α) : Set α := fun a => s₁ a ∨ s₂ a
def FinSet (n : Nat) := Fin n → Prop

namespace FinSet
  export Set (union) -- FinSet.union is now an alias for `Set.union`
end FinSet

example (x y : FinSet 10) : FinSet 10 :=
  x.union y -- Works

ext and enter conv tactics can now go inside let-declarations. Example:

example (g : Nat → Nat) (y : Nat) (h : let x := y + 1; g (0+x) = x) : g (y + 1) = y + 1 := by
  conv at h => enter [x, 1, 1]; rw [Nat.zero_add]
  /-
    g : Nat → Nat
    y : Nat
    h : let x := y + 1;
        g x = x
    ⊢ g (y + 1) = y + 1
  -/
  exact h

Add zeta conv tactic to expand let-declarations. Example:

example (h : let x := y + 1; 0 + x = y) : False := by
  conv at h => zeta; rw [Nat.zero_add]
  /-
    y : Nat
    h : y + 1 = y
    ⊢ False
  -/
  simp_arith at h

Improve namespace resolution. See issue #1224. Example:

import Lean
open Lean Parser Elab
open Tactic -- now opens both `Lean.Parser.Tactic` and `Lean.Elab.Tactic`

Rename constant command to opaque. See discussion at Zulip.

Extend induction and cases syntax: multiple left-hand-sides in a single alternative. This extension is very similar to the one implemented for match expressions. Examples:

inductive Foo where
  | mk1 (x : Nat) | mk2 (x : Nat) | mk3

def f (v : Foo) :=
  match v with
  | .mk1 x => x + 1
  | .mk2 x => 2*x + 1
  | .mk3   => 1

theorem f_gt_zero : f v > 0 := by
  cases v with
  | mk1 x | mk2 x => simp_arith!  -- New feature used here!
  | mk3 => decide

let/if indentation in do blocks in now supported.
Add unnamed antiquotation $_ for use in syntax quotation patterns.
Add unused variables linter. Feedback welcome!

Lean now generates an error if the body of a declaration body contains a universe parameter that does not occur in the declaration type, nor is an explicit parameter. Examples:

/-
The following declaration now produces an error because `PUnit` is universe polymorphic,
but the universe parameter does not occur in the function type `Nat → Nat`
-/
def f (n : Nat) : Nat :=
  let aux (_ : PUnit) : Nat := n + 1
  aux ⟨⟩

/-
The following declaration is accepted because the universe parameter was explicitly provided in the
function signature.
-/
def g.{u} (n : Nat) : Nat :=
  let aux (_ : PUnit.{u}) : Nat := n + 1
  aux ⟨⟩

Add subst_vars tactic.
Fix autoParam in structure fields lost in multiple inheritance..

Add [eliminator] attribute. It allows users to specify default recursor/eliminators for the induction and cases tactics. It is an alternative for the using notation. Example:

@[eliminator] protected def recDiag {motive : Nat → Nat → Sort u}
    (zero_zero : motive 0 0)
    (succ_zero : (x : Nat) → motive x 0 → motive (x + 1) 0)
    (zero_succ : (y : Nat) → motive 0 y → motive 0 (y + 1))
    (succ_succ : (x y : Nat) → motive x y → motive (x + 1) (y + 1))
    (x y : Nat) :  motive x y :=
  let rec go : (x y : Nat) → motive x y
    | 0,     0 => zero_zero
    | x+1, 0   => succ_zero x (go x 0)
    | 0,   y+1 => zero_succ y (go 0 y)
    | x+1, y+1 => succ_succ x y (go x y)
  go x y
termination_by go x y => (x, y)

def f (x y : Nat) :=
  match x, y with
  | 0,   0   => 1
  | x+1, 0   => f x 0
  | 0,   y+1 => f 0 y
  | x+1, y+1 => f x y
termination_by f x y => (x, y)

example (x y : Nat) : f x y > 0 := by
  induction x, y <;> simp [f, *]

Add support for casesOn applications to structural and well-founded recursion modules. This feature is useful when writing definitions using tactics. Example:

inductive Foo where
  | a | b | c
  | pair: Foo × Foo → Foo

def Foo.deq (a b : Foo) : Decidable (a = b) := by
  cases a <;> cases b
  any_goals apply isFalse Foo.noConfusion
  any_goals apply isTrue rfl
  case pair a b =>
    let (a₁, a₂) := a
    let (b₁, b₂) := b
    exact match deq a₁ b₁, deq a₂ b₂ with
    | isTrue h₁, isTrue h₂ => isTrue (by rw [h₁,h₂])
    | isFalse h₁, _ => isFalse (fun h => by cases h; cases (h₁ rfl))
    | _, isFalse h₂ => isFalse (fun h => by cases h; cases (h₂ rfl))

Option is again a monad. The auxiliary type OptionM has been removed. See Zulip thread.
Improve split tactic. It used to fail on match expressions of the form match h : e with ... where e is not a free variable. The failure used to occur during generalization.

New encoding for match-expressions that use the h : notation for discriminants. The information is not lost during delaboration, and it is the foundation for a better split tactic. at delaboration time. Example:

#print Nat.decEq
/-
protected def Nat.decEq : (n m : Nat) → Decidable (n = m) :=
fun n m =>
  match h : Nat.beq n m with
  | true => isTrue (_ : n = m)
  | false => isFalse (_ : ¬n = m)
-/

exists tactic is now takes a comma separated list of terms.
Add dsimp and dsimp! tactics. They guarantee the result term is definitionally equal, and only apply rfl-theorems.
Fix binder information for match patterns that use definitions tagged with [matchPattern] (e.g., Nat.add). We now have proper binder information for the variable y in the following example.
```
def f (x : Nat) : Nat :=
  match x with
  | 0 => 1
  | y + 1 => y
```

(Fix) the default value for structure fields may now depend on the structure parameters. Example:

structure Something (i: Nat) where
n1: Nat := 1
n2: Nat := 1 + i

def s : Something 10 := {}
example : s.n2 = 11 := rfl

Apply rfl theorems at the dsimp auxiliary method used by simp. dsimp can be used anywhere in an expression because it preserves definitional equality.
Refine auto bound implicit feature. It does not consider anymore unbound variables that have the same name of a declaration being defined. Example:
```
def f : f → Bool := -- Error at second `f`
  fun _ => true

inductive Foo : List Foo → Type -- Error at second `Foo`
  | x : Foo []
```
Before this refinement, the declarations above would be accepted and the second f and Foo would be treated as auto implicit variables. That is, f : {f : Sort u} → f → Bool, and Foo : {Foo : Type u} → List Foo → Type.

Fix syntax highlighting for recursive declarations. Example

inductive List (α : Type u) where
  | nil : List α  -- `List` is not highlighted as a variable anymore
  | cons (head : α) (tail : List α) : List α

def List.map (f : α → β) : List α → List β
  | []    => []
  | a::as => f a :: map f as -- `map` is not highlighted as a variable anymore

Add autoUnfold option to Lean.Meta.Simp.Config, and the following macros
- simp! for simp (config := { autoUnfold := true })
- simp_arith! for simp (config := { autoUnfold := true, arith := true })
- simp_all! for simp_all (config := { autoUnfold := true })
- simp_all_arith! for simp_all (config := { autoUnfold := true, arith := true })
When the autoUnfold is set to true, simp tries to unfold the following kinds of definition
- Recursive definitions defined by structural recursion.
- Non-recursive definitions where the body is a match-expression. This kind of definition is only unfolded if the match can be reduced. Example:
```
def append (as bs : List α) : List α :=
  match as with
  | [] => bs
  | a :: as => a :: append as bs

theorem append_nil (as : List α) : append as [] = as := by
  induction as <;> simp_all!

theorem append_assoc (as bs cs : List α) : append (append as bs) cs = append as (append bs cs) := by
  induction as <;> simp_all!
```

Add save tactic for creating checkpoints more conveniently. Example:

example : <some-proposition> := by
  tac_1
  tac_2
  save
  tac_3
  ...

is equivalent to

example : <some-proposition> := by
  checkpoint
    tac_1
    tac_2
  tac_3
  ...

Remove support for {} annotation from inductive datatype constructors. This annotation was barely used, and we can control the binder information for parameter bindings using the new inductive family indices to parameter promotion. Example: the following declaration using {}
```
inductive LE' (n : Nat) : Nat → Prop where
  | refl {} : LE' n n -- Want `n` to be explicit
  | succ  : LE' n m → LE' n (m+1)
```
can now be written as
```
inductive LE' : Nat → Nat → Prop where
  | refl (n : Nat) : LE' n n
  | succ : LE' n m → LE' n (m+1)
```
In both cases, the inductive family has one parameter and one index. Recall that the actual number of parameters can be retrieved using the command #print.
Remove support for {} annotation in the structure command.
Several improvements to LSP server. Examples: "jump to definition" in mutually recursive sections, fixed incorrect hover information in "match"-expression patterns, "jump to definition" for pattern variables, fixed auto-completion in function headers, etc.
In macro ... xs:p* ... and similar macro bindings of combinators, xs now has the correct type Array Syntax
Identifiers in syntax patterns now ignore macro scopes during matching.

Improve binder names for constructor auto implicit parameters. Example, given the inductive datatype

inductive Member : α → List α → Type u
  | head : Member a (a::as)
  | tail : Member a bs → Member a (b::bs)

before:

#check @Member.head
-- @Member.head : {x : Type u_1} → {a : x} → {as : List x} → Member a (a :: as)

now:

#check @Member.head
-- @Member.head : {α : Type u_1} → {a : α} → {as : List α} → Member a (a :: as)

Improve error message when constructor parameter universe level is too big.

Add support for for h : i in [start:stop] do .. where h : i ∈ [start:stop]. This feature is useful for proving termination of functions such as:

inductive Expr where
  | app (f : String) (args : Array Expr)

def Expr.size (e : Expr) : Nat := Id.run do
  match e with
  | app f args =>
    let mut sz := 1
    for h : i in [: args.size] do
      -- h.upper : i < args.size
      sz := sz + size (args.get ⟨i, h.upper⟩)
    return sz

Add tactic case'. It is similar to case, but does not admit the goal on failure. For example, the new tactic is useful when writing tactic scripts where we need to use case' at first | ... | ..., and we want to take the next alternative when case' fails.

Add tactic macro

macro "stop" s:tacticSeq : tactic => `(repeat sorry)

See discussion on Zulip.

When displaying goals, we do not display inaccessible proposition names if they do not have forward dependencies. We still display their types. For example, the goal

case node.inl.node
β : Type u_1
b : BinTree β
k : Nat
v : β
left : Tree β
key : Nat
value : β
right : Tree β
ihl : BST left → Tree.find? (Tree.insert left k v) k = some v
ihr : BST right → Tree.find? (Tree.insert right k v) k = some v
h✝ : k < key
a✝³ : BST left
a✝² : ForallTree (fun k v => k < key) left
a✝¹ : BST right
a✝ : ForallTree (fun k v => key < k) right
⊢ BST left

is now displayed as

case node.inl.node
β : Type u_1
b : BinTree β
k : Nat
v : β
left : Tree β
key : Nat
value : β
right : Tree β
ihl : BST left → Tree.find? (Tree.insert left k v) k = some v
ihr : BST right → Tree.find? (Tree.insert right k v) k = some v
 : k < key
 : BST left
 : ForallTree (fun k v => k < key) left
 : BST right
 : ForallTree (fun k v => key < k) right
⊢ BST left

The hypothesis name is now optional in the by_cases tactic.
Fix inconsistency between syntax and kind names. The node kinds numLit, charLit, nameLit, strLit, and scientificLit are now called num, char, name, str, and scientific respectively. Example: we now write
```
macro_rules | `($n:num) => `("hello")
```
instead of
```
macro_rules | `($n:numLit) => `("hello")
```
(Experimental) New checkpoint <tactic-seq> tactic for big interactive proofs.
Rename tactic nativeDecide => native_decide.
Antiquotations are now accepted in any syntax. The incQuotDepth syntax parser is therefore obsolete and has been removed.
Renamed tactic nativeDecide => native_decide.

"Cleanup" local context before elaborating a match alternative right-hand-side. Examples:

example (x : Nat) : Nat :=
  match g x with
  | (a, b) => _ -- Local context does not contain the auxiliary `_discr := g x` anymore

example (x : Nat × Nat) (h : x.1 > 0) : f x > 0 := by
  match x with
  | (a, b) => _ -- Local context does not contain the `h✝ : x.fst > 0` anymore

Improve let-pattern (and have-pattern) macro expansion. In the following example,
```
example (x : Nat × Nat) : f x > 0 := by
  let (a, b) := x
  done
```
The resulting goal is now ... |- f (a, b) > 0 instead of ... |- f x > 0.
Add cross-compiled aarch64 Linux and aarch64 macOS releases.
Add tutorial-like examples to our documentation, rendered using LeanInk+Alectryon.

v4.0.0-m4 (23 March 2022)

simp now takes user-defined simp-attributes. You can define a new simp attribute by creating a file (e.g., MySimp.lean) containing

import Lean
open Lean.Meta

initialize my_ext : SimpExtension ← registerSimpAttr `my_simp "my own simp attribute"

If you don't need to access my_ext, you can also use the macro

import Lean

register_simp_attr my_simp "my own simp attribute"

Recall that the new simp attribute is not active in the Lean file where it was defined. Here is a small example using the new feature.

import MySimp

def f (x : Nat) := x + 2
def g (x : Nat) := x + 1

@[my_simp] theorem f_eq : f x = x + 2 := rfl
@[my_simp] theorem g_eq : g x = x + 1 := rfl

example : f x + g x = 2*x + 3 := by
  simp_arith [my_simp]

Extend match syntax: multiple left-hand-sides in a single alternative. Example:

def fib : Nat → Nat
| 0 | 1 => 1
| n+2 => fib n + fib (n+1)

This feature was discussed at issue 371. It was implemented as a macro expansion. Thus, the following is accepted.

inductive StrOrNum where
  | S (s : String)
  | I (i : Int)

def StrOrNum.asString (x : StrOrNum) :=
  match x with
  | I a | S a => toString a

Improve #eval command. Now, when it fails to synthesize a Lean.MetaEval instance for the result type, it reduces the type and tries again. The following example now works without additional annotations
```
def Foo := List Nat

def test (x : Nat) : Foo :=
  [x, x+1, x+2]

#eval test 4
```

rw tactic can now apply auto-generated equation theorems for a given definition. Example:

example (a : Nat) (h : n = 1) : [a].length = n := by
  rw [List.length]
  trace_state -- .. |- [].length + 1 = n
  rw [List.length]
  trace_state -- .. |- 0 + 1 = n
  rw [h]

Fuzzy matching for auto completion
Extend dot-notation x.field for arrow types. If type of x is an arrow, we look up for Function.field. For example, given f : Nat → Nat and g : Nat → Nat, f.comp g is now notation for Function.comp f g.

The new .<identifier> notation is now also accepted where a function type is expected.

example (xs : List Nat) : List Nat := .map .succ xs
example (xs : List α) : Std.RBTree α ord := xs.foldl .insert ∅

Add code folding support to the language server.
Support notation let <pattern> := <expr> | <else-case> in do blocks.
Remove support for "auto" pure. In the Zulip thread, the consensus seemed to be that "auto" pure is more confusing than it's worth.

Remove restriction in congr theorems that all function arguments on the left-hand-side must be free variables. For example, the following theorem is now a valid congr theorem.

@[congr]
theorem dep_congr [DecidableEq ι] {p : ι → Set α} [∀ i, Inhabited (p i)] :
                  ∀ {i j} (h : i = j) (x : p i) (y : α) (hx : x = y), Pi.single (f := (p ·)) i x = Pi.single (f := (p ·)) j ⟨y, hx ▸ h ▸ x.2⟩ :=

Partially applied congruence theorems.
Improve elaboration postponement heuristic when expected type is a metavariable. Lean now reduces the expected type before performing the test.
Remove deprecated leanpkg in favor of Lake now bundled with Lean.
Various improvements to go-to-definition & find-all-references accuracy.
Auto generated congruence lemmas with support for casts on proofs and Decidable instances (see wishlist).
Rename option autoBoundImplicitLocal => autoImplicit.
Relax auto-implicit restrictions. The command set_option relaxedAutoImplicit false disables the relaxations.
contradiction tactic now closes the goal if there is a False.elim application in the target.
Renamed tatic byCases => by_cases (motivation: enforcing naming convention).

Local instances occurring in patterns are now considered by the type class resolution procedure. Example:

def concat : List ((α : Type) × ToString α × α) → String
  | [] => ""
  | ⟨_, _, a⟩ :: as => toString a ++ concat as

Notation for providing the motive for match expressions has changed. before:

match x, rfl : (y : Nat) → x = y → Nat with
| 0,   h => ...
| x+1, h => ...

now:

match (motive := (y : Nat) → x = y → Nat) x, rfl with
| 0,   h => ...
| x+1, h => ...

With this change, the notation for giving names to equality proofs in match-expressions is not whitespace sensitive anymore. That is, we can now write

match h : sort.swap a b with
| (r₁, r₂) => ... -- `h : sort.swap a b = (r₁, r₂)`

(generalizing := true) is the default behavior for match expressions even if the expected type is not a proposition. In the following example, we used to have to include (generalizing := true) manually.

inductive Fam : Type → Type 1 where
  | any : Fam α
  | nat : Nat → Fam Nat

example (a : α) (x : Fam α) : α :=
  match x with
  | Fam.any   => a
  | Fam.nat n => n

We now use PSum (instead of Sum) when compiling mutually recursive definitions using well-founded recursion.
Better support for parametric well-founded relations. See issue #1017. This change affects the low-level termination_by' hint because the fixed prefix of the function parameters in not "packed" anymore when constructing the well-founded relation type. For example, in the following definition, as is part of the fixed prefix, and is not packed anymore. In previous versions, the termination_by' term would be written as measure fun ⟨as, i, _⟩ => as.size - i
```
def sum (as : Array Nat) (i : Nat) (s : Nat) : Nat :=
  if h : i < as.size then
    sum as (i+1) (s + as.get ⟨i, h⟩)
  else
    s
termination_by' measure fun ⟨i, _⟩ => as.size - i
```
Add while <cond> do <do-block>, repeat <do-block>, and repeat <do-block> until <cond> macros for do-block. These macros are based on partial definitions, and consequently are useful only for writing programs we don't want to prove anything about.
Add arith option to Simp.Config, the macro simp_arith expands to simp (config := { arith := true }). Only Nat and linear arithmetic is currently supported. Example:
```
example : 0 < 1 + x ∧ x + y + 2 ≥ y + 1 := by
  simp_arith
```
Add fail <string>? tactic that always fail.
Add support for acyclicity at dependent elimination. See issue #1022.
Add trace <string> tactic for debugging purposes.
Add nontrivial SizeOf instance for types Unit → α, and add support for them in the auto-generated SizeOf instances for user-defined inductive types. For example, given the inductive datatype
```
inductive LazyList (α : Type u) where
  | nil                               : LazyList α
  | cons (hd : α) (tl : LazyList α)   : LazyList α
  | delayed (t : Thunk (LazyList α))  : LazyList α
```
we now have sizeOf (LazyList.delayed t) = 1 + sizeOf t instead of sizeOf (LazyList.delayed t) = 2.

Add support for guessing (very) simple well-founded relations when proving termination. For example, the following function does not require a termination_by annotation anymore.

def Array.insertAtAux (i : Nat) (as : Array α) (j : Nat) : Array α :=
  if h : i < j then
    let as := as.swap! (j-1) j;
    insertAtAux i as (j-1)
  else
    as

Add support for for h : x in xs do ... notation where h : x ∈ xs. This is mainly useful for showing termination.
Auto implicit behavior changed for inductive families. An auto implicit argument occurring in inductive family index is also treated as an index (IF it is not fixed, see next item). For example
```
inductive HasType : Index n → Vector Ty n → Ty → Type where
```
is now interpreted as
```
inductive HasType : {n : Nat} → Index n → Vector Ty n → Ty → Type where
```

To make the previous feature more convenient to use, we promote a fixed prefix of inductive family indices to parameters. For example, the following declaration is now accepted by Lean

inductive Lst : Type u → Type u
  | nil  : Lst α
  | cons : α → Lst α → Lst α

and α in Lst α is a parameter. The actual number of parameters can be inspected using the command #print Lst. This feature also makes sure we still accept the declaration

inductive Sublist : List α → List α → Prop
  | slnil : Sublist [] []
  | cons l₁ l₂ a : Sublist l₁ l₂ → Sublist l₁ (a :: l₂)
  | cons2 l₁ l₂ a : Sublist l₁ l₂ → Sublist (a :: l₁) (a :: l₂)

Added auto implicit "chaining". Unassigned metavariables occurring in the auto implicit types now become new auto implicit locals. Consider the following example:

inductive HasType : Fin n → Vector Ty n → Ty → Type where
  | stop : HasType 0 (ty :: ctx) ty
  | pop  : HasType k ctx ty → HasType k.succ (u :: ctx) ty

ctx is an auto implicit local in the two constructors, and it has type ctx : Vector Ty ?m. Without auto implicit "chaining", the metavariable ?m will remain unassigned. The new feature creates yet another implicit local n : Nat and assigns n to ?m. So, the declaration above is shorthand for

inductive HasType : {n : Nat} → Fin n → Vector Ty n → Ty → Type where
  | stop : {ty : Ty} → {n : Nat} → {ctx : Vector Ty n} → HasType 0 (ty :: ctx) ty
  | pop  : {n : Nat} → {k : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType k ctx ty → HasType k.succ (u :: ctx) ty

Eliminate auxiliary type annotations (e.g, autoParam and optParam) from recursor minor premises and projection declarations. Consider the following example

structure A :=
  x : Nat
  h : x = 1 := by trivial

example (a : A) : a.x = 1 := by
  have aux := a.h
  -- `aux` has now type `a.x = 1` instead of `autoParam (a.x = 1) auto✝`
  exact aux

example (a : A) : a.x = 1 := by
  cases a with
  | mk x h =>
    -- `h` has now type `x = 1` instead of `autoParam (x = 1) auto✝`
    assumption

We now accept overloaded notation in patterns, but we require the set of pattern variables in each alternative to be the same. Example:

inductive Vector (α : Type u) : Nat → Type u
  | nil : Vector α 0
  | cons : α → Vector α n → Vector α (n+1)

infix:67 " :: " => Vector.cons -- Overloading the `::` notation

def head1 (x : List α) (h : x ≠ []) : α :=
  match x with
  | a :: as => a -- `::` is `List.cons` here

def head2 (x : Vector α (n+1)) : α :=
  match x with
  | a :: as => a -- `::` is `Vector.cons` here

New notation .<identifier> based on Swift. The namespace is inferred from the expected type. See issue #944. Examples:

def f (x : Nat) : Except String Nat :=
  if x > 0 then
    .ok x
  else
    .error "x is zero"

namespace Lean.Elab
open Lsp

def identOf : Info → Option (RefIdent × Bool)
  | .ofTermInfo ti => match ti.expr with
    | .const n .. => some (.const n, ti.isBinder)
    | .fvar id .. => some (.fvar id, ti.isBinder)
    | _ => none
  | .ofFieldInfo fi => some (.const fi.projName, false)
  | _ => none

def isImplicit (bi : BinderInfo) : Bool :=
  bi matches .implicit

end Lean.Elab

152 KiB Raw Blame History Unescape Escape

Lean 4 releases

v4.11.0

v4.10.0

v4.9.0

Language features, tactics, and metaprograms

Language server, widgets, and IDE extensions

Library

Lean internals

Compiler, runtime, and FFI

Lake

DevOps

Breaking changes

v4.8.0

Language features, tactics, and metaprograms

Language server and IDE extensions

Pretty printing

Library

Lean internals

Compiler, runtime, and FFI

Lake

DevOps

Breaking changes

v4.7.0

v4.6.1

v4.6.0

v4.5.0

v4.4.0

v4.3.0

v4.2.0

v4.1.0

v4.0.0

v4.0.0-m5 (07 August 2022)

v4.0.0-m4 (23 March 2022)

152 KiB

Raw Blame History