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.
-
Executables configured with
supportInterpreter := true
on Windows should now be run vialake exe
to function properly.The way Lean is built on Windows has changed (see PR #3601). As a result, Lake now dynamically links executables with
supportInterpreter := true
on Windows tolibleanshared.dll
andlibInit_shared.dll
. Therefore, such executables will not run unless those shared libraries are co-located with the executables or part ofPATH
. Running the executable vialake exe
will ensure these libraries are part ofPATH
.In a related change, the signature of the
nativeFacets
Lake configuration options has changed from a staticArray
to a function(shouldExport : Bool) → Array
. See its docstring or Lake's README for further details on the changed option. -
Lean now generates an error if the type of a theorem is not a proposition.
-
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).
-
Funcitonal induction principles.
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 theusing
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 indef 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
. -
Attribute
@[pp_using_anonymous_constructor]
to make structures pretty print like⟨x, y, z⟩
rather than{a := x, b := y, c := z}
. This attribute is applied toSigma
,PSigma
,PProd
,Subtype
,And
, andFin
. -
Now structure instances pretty print with parent structures' fields inlined. That is, if
B
extendsA
, then{ toA := { x := 1 }, y := 2 }
now pretty prints as{ x := 1, y := 2 }
. Setting optionpp.structureInstances.flatten
to false turns this off. -
Option
pp.structureProjections
is renamed topp.fieldNotation
, and there is now a suboptionpp.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. -
Added
@[induction_eliminator]
and@[cases_eliminator]
attributes to be able to define custom eliminators for theinduction
andcases
tactics, replacing the@[eliminator]
attribute. Gives custom eliminators forNat
so thatinduction
andcases
put goal states into terms of0
andn + 1
rather thanNat.zero
andNat.succ n
. Added optiontactic.customEliminators
to control whether to use custom eliminators. #3629 and #3655.
Breaking changes:
- Automatically generated equational theorems are now named using suffix
.eq_<idx>
instead of._eq_<idx>
, and.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.def
/-
fact.def :
∀ (x : Nat),
fact x =
match x with
| 0 => 1
| Nat.succ n => (n + 1) * fact n
-/
- The coercion from
String
toName
was removed. Previously, it wasName.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 toName.mkSimple
.
-
simp
andrw
now use instance arguments found by unification, rather than always resynthesizing. For backwards compatibility, the original behaviour is available viaset_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. Thepp.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 anapp_unexpander
is no longer necessary. #3495. -
New
simp
(anddsimp
) configuration option:zetaDelta
. It isfalse
by default. Thezeta
option is stilltrue
by default, but their meaning has changed.- When
zeta := true
,simp
anddsimp
reduce terms of the formlet x := val; e[x]
intoe[val]
. - When
zetaDelta := true
,simp
anddsimp
will expand let-variables in the context. For example, suppose the context containsx := val
. Then, any occurrence ofx
is replaced withval
.
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
-
When adding new local theorems to
simp
, the system assumes that the function application arguments have been annotated withno_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 becausesimp
does not index f-arguments anymore when addingh
to thesimp
-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 atermination_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:- Making universally useful tactics such as
ext
,by_cases
,change at
,norm_cast
,rcases
,simpa
,simp?
,omega
, andexact?
available to all users of Lean, without imports. - Minimizing the syntactic changes between plain Lean and Lean with
import Std
. - Simplifying the development process for the basic data types
Nat
,Int
,Fin
(and variants such asUInt64
),List
,Array
, andBitVec
as we begin making the APIs and simp normal forms for these types more complete and consistent. - 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 inv4.7.0-rc1
, some upstreaming will continue over the coming months.
- Making universally useful tactics such as
-
The
/
and%
notations inInt
now useInt.ediv
andInt.emod
(i.e. the rounding conventions have changed). PreviouslyStd
overrode these notations, so this is no change for users ofStd
. 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 aboutBitVec
which naturally translate into linear arithmetic problems. #3435. omega
now has support forFin
#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 proveid x ≤ x
). #3525. This may cause some regressions. We plan to provide a general purpose preprocessing tactic later, or anomega!
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 whileomega
does help automate some proofs, we plan to make this much more robust.
- It is supplemented by a preprocessing tactic
-
The library search tactics
exact?
andapply?
that were originally in Mathlib are now available in Lean itself. These use the implementation using lazy discrimination trees fromStd
, 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 fromStd
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 (particularlysimp
) 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 overf + g
showsf
. There is no way to fix the situation from within an app unexpander; the expression position forHAdd.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
, thef + g
gets TermInfo registered for that subexpression, making it properly hoverable.
Breaking changes:
Lean.withTraceNode
and variants got a strongerMonadAlwaysExcept
assumption to fix trace trees not being built on elaboration runtime exceptions. Instances for most elaboration monads built onEIO Exception
should be synthesized automatically.- The
match ... with.
andfun.
notations previously in Std have been replaced bynomatch ...
andnofun
. #3279 and #3286
Other improvements:
- several bug fixes for
simp
: - fixes for
match
expressions: - 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:
- Backport of #3552 fixing a performance regression in server startup.
-
Add custom simplification procedures (aka
simproc
s) tosimp
. 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 tosimp
commands, and suppressed using-
. They are also supported bysimp?
.simp only
does not execute anysimproc
. Here are some examples for thesimproc
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 asimp
and asimproc
set with the name<id>
. The following command instructs Lean to insert thereduceFoo
simplification procedure into the setmy_simp
. If no set is specified, Lean uses the defaultsimp
set.simproc [my_simp] reduceFoo (foo _) := ...
-
The syntax of the
termination_by
anddecreasing_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, thetermination_by
anddecreasing_by
for that function come before thewhere
. The functions in thewhere
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
orlet 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. - They are now placed directly after the function they apply to, instead of
after the whole
-
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 likefirst
: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 owndecreasing_by
, the defaultdecreasing_tactic
is used. If the same tactic ought to be applied to multiple functions, thedecreasing_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 theInfoTree
manually instead of going through the functions inInfoUtils.lean
, as well as those manually creating and savingInfoTree
s. 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
andpp.deepTerms.threshold
) (PR #3201) -
Add pretty printer options
pp.numeralTypes
andpp.natLit
. Whenpp.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)
. Whenpp.natLit
is true, then raw natural number literals are pretty printed asnat_lit 2
. PR #2933 and RFC #3021.
Lake updates:
Other improvements:
- make
intro
be aware oflet_fun
#3115 - produce simpler proof terms in
rw
#3121 - fuse nested
mkCongrArg
calls in proofs generated bysimp
#3203 induction using
followed by a general term #3188- allow generalization in
let
#3060, fixing #3065 - reducing out-of-bounds
swap!
should returna
, not `default`` #3197, fixing #3196 - derive
BEq
on structure withProp
-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
-
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"
-
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 inr#"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 useWellFounded.wrap
from the std libarary to explicitly give one:-termination_by' ⟨r, hwf⟩ +termination_by x => hwf.wrap x
-
Support snippet edits in LSP
TextEdit
s. SeeLean.Lsp.SnippetString
for more details. -
Deprecations and changes in the widget API.
Widget.UserWidgetDefinition
is deprecated in favour ofWidget.Module
. The annotation@[widget]
is deprecated in favour of@[widget_module]
. To migrate a definition of typeUserWidgetDefinition
, remove thename
field and replace the type withWidget.Module
. Removing thename
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 likeInferred 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?
andsimp_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 isimport 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 aDecidableEq
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.
-
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 andlean
using theleanOptions
config field. Setting either of these fields instead ofmoreServerArgs
ensures that viewing files from a dependency uses the options for that dependency. Additionally,moreServerArgs
is being deprecated in favor of themoreGlobalServerArgs
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⟩]
Bug fixes for #2628, #2883, #2810, #2925, and #2914.
Lake:
lake init .
and a barelake init
and will now use the current directory as the package name. #2890lake new
andlake init
will now produce errors on invalid package names such as..
,foo/bar
,Init
,Lean
,Lake
, andMain
. 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 namedbar.*
rather thanBar.*
). See issue #2567 and PR #2889.- Lean and Lake now properly support non-identifier library names (e.g.,
lake new 123-hello
andimport «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 viaelab
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 parsestarget
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 namedfoo-bar
andlake new foo.bar exe
properly createsfoo/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.
-
simp [f]
does not unfold partial applications off
anymore. See issue #2042. To fix proofs affected by this change, useunfold f
orsimp (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 bysimp
, and thedecide
tactic may be useful in such cases. Thedecide
simp configuration option can be used to locally restore the oldsimp
behavior, as insimp (config := {decide := true})
; this includes using Decidable instances to verify side goals such as numeric inequalities. -
Many bug fixes:
- Add left/right actions to term tree coercion elaborator and make `^`` a right action
- Fix for #2775, don't catch max recursion depth errors
- Reduction of
Decidable
instances very slow when usingcases
tactic simp
not rewriting in bindersimp
unfoldinglet
even withzeta := false
optionsimp
(with beta/zeta disabled) and discrimination trees- unknown free variable introduced by
rw ... at h
dsimp
doesn't userfl
theorems which consist of an unapplied constantdsimp
does not close reflexive equality goals if they are wrapped in metadatarw [h]
usesh
from the environment in preference toh
from the local context- missing
withAssignableSyntheticOpaque
forassumption
tactic - ignoring default value for field warning
-
Cancel outstanding tasks on document edit in the language server.
Lake:
- Sensible defaults for
lake new MyProject math
- Changed
postUpdate?
configuration option to apost_update
declaration. See thepost_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
, andlean_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).
- isDefEq cache for terms not containing metavariables..
- Make
Environment.mk
andEnvironment.add
private, and addreplay
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 successfullake 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 ofe
and no longer captures pre-existing metavariables that occur ine
(#2502).- This is accomplished via changes to
withCollectingNewGoalsFrom
, which also affectselabTermWithHoles
,refine'
,calc
(tactic), andspecialize
. 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 torefine e
capturing previously-created goals appearing unexpectedly ine
(no issue; see PR).
- This is accomplished via changes to
-
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
orlean-toolchain
. You can also force a reconfigure by passing the new--reconfigure
/-R
option tolake
. - Lake configuration options (i.e.,
-K
) will be fixed at the moment of elaboration. Setting these options whenlake
is using the cached configuration will have no effect. To change options, runlake
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
.
- Lake will regenerate this OLean after each modification to the
-
The signature of
Lake.buildO
has changed,args
has been split intoweakArgs
andtraceArgs
.traceArgs
are included in the input trace andweakArgs
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
, andLean.Elab.parseImports
have changed from takingList Import
toArray Import
. -
There is now an
occs
field in the configuration object for therewrite
tactic, allowing control of which occurrences of a pattern should be rewritten. This was previously a separate argument forLean.MVarId.rewrite
, and this has been removed in favour of an additional field ofRewrite.Config
. It was not previously accessible from user tactics.
-
Lean.Meta.getConst?
has been renamed. We have renamedgetConst?
togetUnfoldableConst?
(andgetConstNoEx?
togetUnfoldableConstNoEx?
). These were not intended to be part of the public API, but downstream projects had been using them (sometimes expecting different behaviour) incorrectly instead ofLean.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 ofsimp
(with complicated goals it can be hard to tell if it was effective) and to allow easier flow control in tactics internally usingsimp
. See the summary discussion on zulip for more details. -
simp_all
now preserves order of hypotheses.In order to support the
failIfUnchanged
configuration option fordsimp
/simp
/simp_all
the waysimp_all
replaces hypotheses has changed. In particular it is now more likely to preserve the order of hypotheses. Seesimp_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 userename_i
,case ... =>
, ornext ... =>
. -
this
is now a regular identifier again that is implicitly introduced by anonymoushave :=
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. -
Make
calc
require the sequence of relation/proof-s to have the same indentation, and addcalc
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).
-
Add
linter.deprecated
option to silence deprecation warnings. -
simp
can track information and can print an equivalentsimp 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. -
Many new doc strings have been added to declarations at
Init
.
-
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. -
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 declaringOfNat
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 calledelab_as_eliminator
in Lean 3). Motivation: simplify the Mathlib port to Lean 4. -
Trans
type class now accepts relations inType 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 usingset_option checkBinderAnnotations false
. -
Add option
pp.showLetValues
. When set tofalse
, the info view hides the value oflet
-variables in a goal. By default, it istrue
when visualizing tactic goals, andfalse
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 forFVarId
,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 abbreviationLMVarId
) 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 typeclassclass 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 followsmacro: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 tacticget_elem_tactic
. For example, the typeArray α
has the following instancesinstance : 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]!
anda[i]?
, Fora[i]!
, a panic error message is produced at runtime ifi
is not a valid index.a[i]?
has typeOption α
, anda[i]?
evaluates tonone
if the indexi
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 asmacro "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 usingmacro_rules
. By default, it triestrivial
,simp_arith
, and a special case forFin
. In the future, it will also trylinarith
. You can extendget_elem_tactic_trivial
usingmy_tactic
as followsmacro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| my_tactic)
Note that
Idx
's type inGetElem
does not depend onCont
. So, you cannot write the instanceinstance : 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
to0
. 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 forIO.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
andenter
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 toopaque
. See discussion at Zulip. -
Extend
induction
andcases
syntax: multiple left-hand-sides in a single alternative. This extension is very similar to the one implemented formatch
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
-
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 theinduction
andcases
tactics. It is an alternative for theusing
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 typeOptionM
has been removed. See Zulip thread. -
Improve
split
tactic. It used to fail onmatch
expressions of the formmatch h : e with ...
wheree
is not a free variable. The failure used to occur during generalization. -
New encoding for
match
-expressions that use theh :
notation for discriminants. The information is not lost during delaboration, and it is the foundation for a bettersplit
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
anddsimp!
tactics. They guarantee the result term is definitionally equal, and only applyrfl
-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 variabley
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 thedsimp
auxiliary method used bysimp
.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
andFoo
would be treated as auto implicit variables. That is,f : {f : Sort u} → f → Bool
, andFoo : {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 toLean.Meta.Simp.Config
, and the following macrossimp!
forsimp (config := { autoUnfold := true })
simp_arith!
forsimp (config := { autoUnfold := true, arith := true })
simp_all!
forsimp_all (config := { autoUnfold := true })
simp_all_arith!
forsimp_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 thematch
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 thestructure
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 typeArray 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 ..
whereh : 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 tocase
, but does not admit the goal on failure. For example, the new tactic is useful when writing tactic scripts where we need to usecase'
atfirst | ... | ...
, and we want to take the next alternative whencase'
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 kindsnumLit
,charLit
,nameLit
,strLit
, andscientificLit
are now callednum
,char
,name
,str
, andscientific
respectively. Example: we now writemacro_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 (andhave
-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.
-
simp
now takes user-defined simp-attributes. You can define a newsimp
attribute by creating a file (e.g.,MySimp.lean
) containingimport 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 macroimport 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 aLean.MetaEval
instance for the result type, it reduces the type and tries again. The following example now works without additional annotationsdef 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]
-
Extend dot-notation
x.field
for arrow types. If type ofx
is an arrow, we look up forFunction.field
. For example, givenf : Nat → Nat
andg : Nat → Nat
,f.comp g
is now notation forFunction.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 ∅
-
Support notation
let <pattern> := <expr> | <else-case>
indo
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 validcongr
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⟩ :=
-
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 aFalse.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 writematch h : sort.swap a b with | (r₁, r₂) => ... -- `h : sort.swap a b = (r₁, r₂)`
-
(generalizing := true)
is the default behavior formatch
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 ofSum
) 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, thetermination_by'
term would be written asmeasure 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>
, andrepeat <do-block> until <cond>
macros fordo
-block. These macros are based onpartial
definitions, and consequently are useful only for writing programs we don't want to prove anything about. -
Add
arith
option toSimp.Config
, the macrosimp_arith
expands tosimp (config := { arith := true })
. OnlyNat
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 typesUnit → α
, and add support for them in the auto-generatedSizeOf
instances for user-defined inductive types. For example, given the inductive datatypeinductive 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 ofsizeOf (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 whereh : 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
α
inLst α
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 declarationinductive 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 typectx : Vector Ty ?m
. Without auto implicit "chaining", the metavariable?m
will remain unassigned. The new feature creates yet another implicit localn : Nat
and assignsn
to?m
. So, the declaration above is shorthand forinductive 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
andoptParam
) from recursor minor premises and projection declarations. Consider the following examplestructure 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