# Lean 4.5.0

Lean version 4.5.0 has been released! This release contains a number of quality-of-life improvements.

Please see the detailed release notes for a complete list of changes.

## String Literals

Taking inspiration from Rust and Python, Lean's string literals are now more flexible. *String gaps* make it easier to write long strings on multiple lines without introducing newlines into the string, and *raw strings* allow string literals to include characters that would otherwise be escaped.

String gaps are indicated with a backslash right before a newline, which causes the newline and the spaces at the beginning of the next line to be ignored:

#eval "this string \ is only one line \ long."`"this string is only one line long." : String`

"this string is only one line long."

Gaps also work with interpolation:

#eval s!"this string \ contains {Nat.pred2} newline with two spaces."`Nat.pred (a✝ : Nat) : Nat`

The predecessor function on natural numbers. This definition is overridden in the compiler to use `n - 1` instead. The definition provided here is the logical model.

"this string contains 1\n newline with two spaces."

Raw strings don't process backslash escapes. This is primarily useful when representing escape sequences in a string literal, as they would otherwise need to be double-escaped. Raw literals begin with a lowercase `r`

:

#eval r"This is a backslash: \"`"This is a backslash: \\" : String`

"This is a backslash: \\"

To include a double-quote character in a raw literal, surround the opening and closing double-quotes with hash marks:

#eval r#"I said "hello""#`"I said \"hello\"" : String`

"I said \"hello\""

More hash marks can be used to enable the inclusion of hash-marked strings without escaping:

#eval r##"I said #"hello"#"##`"I said #\"hello\"#" : String`

"I said #\"hello\"#"

## Error Message Improvements

Many error messages have been made more friendly and actionable.

### Mutual Blocks

Instead of reporting `invalid mutual block`

when mixing inductive types and definitions in the same block, Lean now provides more guidance:

mutual inductiveA | mkA : String → A def a : A := .mkA "a"In Lean, every concrete type other than the universes and every type constructor other than dependent arrows is an instance of a general family of type constructions known as inductive types. It is remarkable that it is possible to construct a substantial edifice of mathematics based on nothing more than the type universes, dependent arrow types, and inductive types; everything else follows from those. Intuitively, an inductive type is built up from a specified list of constructor. For example, `List α` is the list of elements of type `α`, and is defined as follows: ``` inductive List (α : Type u) where | nil | cons (head : α) (tail : List α) ``` A list of elements of type `α` is either the empty list, `nil`, or an element `head : α` followed by a list `tail : List α`. For more information about [inductive types](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html).end`"a" : String`

invalid mutual block: either all elements of the block must be inductive declarations, or they must all be definitions/theorems/abbrevs

### Lexicographic Termination Arguments

When checking recursive functions, Lean tries to justify that the function always terminates with two techniques: structural recursion, in which all recursive calls are passed syntactic sub-terms of one of the arguments, and well-founded recursion, in which termination is justfied by appeal to some other notion of size. Joachim Breitner's blog post describes these techniques in detail. Crucially, well-founded recursion can combine size changes of multiple arguments, and it can often discover these combinations automatically.

Starting in version 4.5.0, Lean now provides a table that describes why it can't combine decreasing sizes. For this definition:

def f(j`Nat → Nat → Nat → Nat`

k`Nat`

n`Nat`

: Nat`Nat`

) : Nat`Nat : Type`

The type of natural numbers, starting at zero. It is defined as an inductive type freely generated by "zero is a natural number" and "the successor of a natural number is a natural number". You can prove a theorem `P n` about `n : Nat` by `induction n`, which will expect a proof of the theorem for `P 0`, and a proof of `P (succ i)` assuming a proof of `P i`. The same method also works to define functions by recursion on natural numbers: induction and recursion are two expressions of the same operation from lean's point of view. ``` open Nat example (n : Nat) : n < succ n := by induction n with | zero => show 0 < 1 decide | succ i ih => -- ih : i < succ i show succ i < succ (succ i) exact Nat.succ_lt_succ ih ``` This type is special-cased by both the kernel and the compiler: * The type of expressions contains "`Nat` literals" as a primitive constructor, and the kernel knows how to reduce zero/succ expressions to nat literals. * If implemented naively, this type would represent a numeral `n` in unary as a linked list with `n` links, which is horribly inefficient. Instead, the runtime itself has a special representation for `Nat` which stores numbers up to 2^63 directly and larger numbers use an arbitrary precision "bignum" library (usually [GMP](https://gmplib.org/)).:= match`Nat : Type`

The type of natural numbers, starting at zero. It is defined as an inductive type freely generated by "zero is a natural number" and "the successor of a natural number is a natural number". You can prove a theorem `P n` about `n : Nat` by `induction n`, which will expect a proof of the theorem for `P 0`, and a proof of `P (succ i)` assuming a proof of `P i`. The same method also works to define functions by recursion on natural numbers: induction and recursion are two expressions of the same operation from lean's point of view. ``` open Nat example (n : Nat) : n < succ n := by induction n with | zero => show 0 < 1 decide | succ i ih => -- ih : i < succ i show succ i < succ (succ i) exact Nat.succ_lt_succ ih ``` This type is special-cased by both the kernel and the compiler: * The type of expressions contains "`Nat` literals" as a primitive constructor, and the kernel knows how to reduce zero/succ expressions to nat literals. * If implemented naively, this type would represent a numeral `n` in unary as a linked list with `n` links, which is horribly inefficient. Instead, the runtime itself has a special representation for `Nat` which stores numbers up to 2^63 directly and larger numbers use an arbitrary precision "bignum" library (usually [GMP](https://gmplib.org/)).jPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not., k`Nat`

, n`Nat`

with`Nat`

| 0, 0, 0 => 0 | jPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not., k`Nat`

+ 1, n`Nat`

=> f`Nat`

j`Nat → Nat → Nat → Nat`

k`Nat`

(n`Nat`

+ 1) | 0, 0, n`Nat`

+ 1 => f`Nat`

0 1 n`Nat → Nat → Nat → Nat`

| _, 0, _ => 3`Nat`

Lean reports the following error:

fail to show termination for f with errors argument #1 was not used for structural recursion failed to eliminate recursive application _root_.f j k (n + 1) argument #2 was not used for structural recursion failed to eliminate recursive application _root_.f 0 1 n argument #3 was not used for structural recursion failed to eliminate recursive application _root_.f j k (n + 1) structural recursion cannot be used Could not find a decreasing measure. The arguments relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) j k n 1) 122:19-32 = < ? 2) 123:19-26 = ? _ Please use `termination_by` to specify a decreasing measure.

The last part of the message describes the relationship of each recursive call to their argument values that Lean found. In particular, in the first case with a recursive call (`| j, k + 1, n => f j k (n + 1)`

), the value for `j`

remains the same, the value for `k`

decreases, and the relationship between the input value for `n`

and its value in the recursive call is unknown. In the second recursive case (`| 0, 0, n + 1 => f 0 1 n`

), `n`

remained equal, and because Lean did not conclude anything about `k`

, it gave up searching for a lexicographic order.

##
Changes to `termination_by`

In Lean 4.6.0, the syntax for indicating termination measures for recursive functions will be revamped, making it more consistent and removing many confusing corner cases. To prepare for this change, Lean 4.5.0 no longer supports the little-used `termination_by'`

syntax, which is largely a relic of Lean 4's early history. This feature allowed well-founded relations to be specified directly as expressions rather than using the `WellFoundedRelation`

class. To migrate code that uses `termination_by'`

to `termination_by`

in 4.5.0, replace calls to `measure`

with their arguments as follows:

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`

to provide the appropriate relation explicitly:

termination_by' ⟨r, hwf⟩

termination_by x => hwf.wrap x

## Further Improvements

Further improvements were made to the widget system, support for snippet text edits were added to Lean's LSP implementation, and many bugs were fixed. The complete details are available in the detailed release notes.