fix: use _fvar._ instead of _ for anonymous fvars (#12745)

This PR fixes `pp.fvars.anonymous` to display loose free variables as
`_fvar._` instead of `_` when the option is set to `false`. This was the
intended behavior in https://github.com/leanprover/lean4/pull/12688 but
the fix was committed locally and not pushed before that PR was merged.

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

src/Init/Notation.lean

@@ -911,7 +911,7 @@ differ between runs or Lean versions. Use `set_option pp.mvars.anonymous false`
 anonymous metavariables with `?_` while preserving user-named metavariables like `?a`.
 Alternatively, `set_option pp.mvars false` replaces all metavariables with `?_`.
 Similarly, `set_option pp.fvars.anonymous false` replaces loose free variable names like
-`_fvar.22` with `_`.
+`_fvar.22` with `_fvar._`.
 
 For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop
 everything else.

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -51,7 +51,7 @@ def delabFVar : Delab := do
       -- use internal name like `_fvar.22`
       maybeAddBlockImplicit <| mkIdent (fvarId.name.replacePrefix `_uniq `_fvar)
     else
-      maybeAddBlockImplicit <| mkIdent `_
+      maybeAddBlockImplicit <| mkIdent `_fvar._
 
 -- loose bound variable, use pseudo syntax
 @[builtin_delab bvar]

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -133,7 +133,7 @@ register_builtin_option pp.mvars.delayed : Bool := {
 register_builtin_option pp.fvars.anonymous : Bool := {
   defValue := true
   descr    := "(pretty printer) display names for loose free variables (not in the local context) such as `_fvar.22` when true, \
-    and otherwise display them as '_'. Useful for stabilizing output in `#guard_msgs`."
+    and otherwise display them as `_fvar._`. Useful for stabilizing output in `#guard_msgs`."
 }
 register_builtin_option pp.beta : Bool := {
   defValue := false

tests/lean/run/ppFVarsAnonymous.lean

@@ -6,7 +6,7 @@ import Lean
 When a free variable is not in the local context (a "loose" fvar),
 the pretty printer renders it with an internal name like `_fvar.42`.
 The `pp.fvars.anonymous` option (default `true`) controls this behavior:
-when set to `false`, loose fvars are displayed as `_`.
+when set to `false`, loose fvars are displayed as `_fvar._`.
 -/
 
 open Lean Elab Command in
@@ -24,4 +24,4 @@ run_cmd liftTermElabM do
   let fvarId : FVarId := { name := .num `_uniq 42 }
   let e := Expr.fvar fvarId
   let fmt ← Meta.ppExpr e
-  guard <| s!"{fmt}" == "_"
+  guard <| s!"{fmt}" == "_fvar._"