doc: document match h:e with syntax

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