From 3de18ceb55ae31410752d390e776bbc65e7c0238 Mon Sep 17 00:00:00 2001
From: ammkrn <46387933+ammkrn@users.noreply.github.com>
Date: Mon, 14 Feb 2022 08:53:37 -0600
Subject: [PATCH] doc: document match h:e with syntax

---
 doc/declarations.md | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/doc/declarations.md b/doc/declarations.md
index 2b9752ed9d..ddb15d8f00 100644
--- a/doc/declarations.md
+++ b/doc/declarations.md
@@ -675,6 +675,20 @@ When a ``match`` has only one line, the vertical bar may be left out. In that ca
     def bar₄ (p : Nat × Nat) : Nat :=
     let ⟨m, n⟩ := p in m + n
 
+Information about the term being matched can be preserved in each branch using the syntax `match h:t with` (with no whitespace between the name of the hypothesis, the colon, and the term). For example, a user may want to match a term `ns : List Nat`, while tracking the hypothesis `ns = []` or `ns = h :: t` in the respective match arm:
+
+```lean
+def foo (ns : List Nat) (h1 : ns ≠ []) (k : Nat -> Char) : Char :=
+  match h2:ns with
+  -- in this arm, we have the hypothesis `h2 : ns = []`
+  | [] => absurd h2 h1
+  -- in this arm, we have the hypothesis `h2 : ns = h :: t`
+  | h :: t => k h
+
+-- '7'
+#eval foo [7, 8, 9] (by decide) Nat.digitChar
+```
+
 .. _structures_and_records:
 
 Structures and Records