From 44ef6c64908454403486a8548ce1901bf51239f1 Mon Sep 17 00:00:00 2001
From: ia0 <git@ia0.eu>
Date: Wed, 15 Jul 2026 15:11:13 +0200
Subject: [PATCH] doc: fix string literal mismatch in generalized field
 notation example

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

diff --git a/Manual/Terms.lean b/Manual/Terms.lean
index b838643a9..0a5e41ed9 100644
--- a/Manual/Terms.lean
+++ b/Manual/Terms.lean
@@ -767,7 +767,7 @@ where
 def adminUser : Username := "admin"
 ```
 
-However, {lean}`Username.validate` can't be called on {lean}`"root"` using field notation, because {lean}`String` does not unfold to {lean}`Username`.
+However, {lean}`Username.validate` can't be called on {lean}`"admin"` using field notation, because {lean}`String` does not unfold to {lean}`Username`.
 ```lean +error (name := notString)
 #eval "admin".validate
 ```