From 72f714440367f7ea68a8746072a9622ccdd9c616 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 6 Nov 2023 11:57:10 +0000
Subject: [PATCH] doc: mention the proof-binding syntax in match

This comes up over and over again in the zulip; let's document it!
---
 src/Lean/Parser/Term.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 7c5c28e443..479a13f4d4 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -351,6 +351,9 @@ 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.