diff --git a/src/items/functions.md b/src/items/functions.md
index 325588a53..5b4ac7af6 100644
--- a/src/items/functions.md
+++ b/src/items/functions.md
@@ -59,8 +59,8 @@ fn answer_to_life_the_universe_and_everything() -> i32 {
## Function parameters
-As with `let` bindings, function parameters are irrefutable [patterns], so any
-pattern that is valid in a let binding is also valid as a parameter:
+Function parameters are irrefutable [patterns], so any pattern that is valid in
+an else-less `let` binding is also valid as a parameter:
```rust
fn first((value, _): (i32, i32)) -> i32 { value }
diff --git a/src/statements.md b/src/statements.md
index 8d9c21d7d..7acb0dc25 100644
--- a/src/statements.md
+++ b/src/statements.md
@@ -54,17 +54,38 @@ fn outer() {
> **Syntax**\
> _LetStatement_ :\
> [_OuterAttribute_]\* `let` [_PatternNoTopAlt_]
-> ( `:` [_Type_] )? (`=` [_Expression_] )? `;`
-
-A *`let` statement* introduces a new set of [variables], given by an
-irrefutable [pattern]. The pattern is followed optionally by a type
-annotation and then optionally by an initializer expression. When no
-type annotation is given, the compiler will infer the type, or signal
+> ( `:` [_Type_] )? (`=` [_Expression_] [†](#let-else-restriction)
+> ( `else` [_BlockExpression_]) ? ) ? `;`
+>
+> † When an `else` block is specified, the
+> _Expression_ must not be a [_LazyBooleanExpression_], or end with a `}`.
+
+A *`let` statement* introduces a new set of [variables], given by a [pattern].
+The pattern is followed optionally by a type annotation and then either ends,
+or is followed by an initializer expression plus an optional `else` block.
+When no type annotation is given, the compiler will infer the type, or signal
an error if insufficient type information is available for definite
inference. Any variables introduced by a variable declaration are visible
from the point of declaration until the end of the enclosing block scope,
except when they are shadowed by another variable declaration.
+If an `else` block is not present, the pattern must be irrefutable.
+If an `else` block is present, the pattern may be refutable.
+If the pattern does not match (this requires it to be refutable), the `else`
+block is executed.
+The `else` block must always diverge (evaluate to the [never type]).
+
+```rust
+let (mut v, w) = (vec![1, 2, 3], 42); // The bindings may be mut or const
+let Some(t) = v.pop() else { // Refutable patterns require an else block
+ panic!(); // The else block must diverge
+};
+let [u, v] = [v[0], v[1]] else { // This pattern is irrefutable, so the compiler
+ // will lint as the else block is redundant.
+ panic!();
+};
+```
+
## Expression statements
> **Syntax**\
@@ -121,6 +142,7 @@ statement are [`cfg`], and [the lint check attributes].
[function]: items/functions.md
[item]: items.md
[module]: items/modules.md
+[never type]: types/never.md
[canonical path]: paths.md#canonical-paths
[implementations]: items/implementations.md
[variables]: variables.md
@@ -128,9 +150,11 @@ statement are [`cfg`], and [the lint check attributes].
[`cfg`]: conditional-compilation.md
[the lint check attributes]: attributes/diagnostics.md#lint-check-attributes
[pattern]: patterns.md
+[_BlockExpression_]: expressions/block-expr.md
[_ExpressionStatement_]: #expression-statements
[_Expression_]: expressions.md
[_Item_]: items.md
+[_LazyBooleanExpression_]: expressions/operator-expr.md#lazy-boolean-operators
[_LetStatement_]: #let-statements
[_MacroInvocationSemi_]: macros.md#macro-invocation
[_OuterAttribute_]: attributes.md