From 1919386ec81ad8326f43371a28db85eb7fdca581 Mon Sep 17 00:00:00 2001
From: ia0 <git@ia0.eu>
Date: Tue, 11 Aug 2026 15:33:42 +0200
Subject: [PATCH] doc: fix typo in example for using local variables in
 elab_rules

---
 Manual/NotationsMacros/Elab.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Manual/NotationsMacros/Elab.lean b/Manual/NotationsMacros/Elab.lean
index e345cfb4e..4f9566cdf 100644
--- a/Manual/NotationsMacros/Elab.lean
+++ b/Manual/NotationsMacros/Elab.lean
@@ -252,7 +252,7 @@ It chooses the most recent suitable variable, as desired:
 #eval
   let x := "x"
   let y := "y"
-  "It was " ++ y
+  "It was " ++ anything!
 ```
 ```leanOutput lets
 "It was y"