v4.5.0-rc1
Pre-releaseChanges since v4.4.0
(from RELEASE.md):
-
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 go 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.
Withset_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.
Full Changelog: v4.4.0...v4.5.0-rc1