feat: add pp.fvars.anonymous option (#12688)

This PR adds a `pp.fvars.anonymous` option (default `true`) that
controls the display of loose free variables (fvars not in the local
context).

- When `true` (default), loose fvars display their internal name like
`_fvar.42`
- When `false`, they display as `_fvar._`

This is analogous to `pp.mvars.anonymous` for metavariables. It's useful
for stabilizing output in `#guard_msgs` when messages contain fvar IDs
that vary between runs — for example, in diagnostic tools that report
`isDefEq` failures from trace output where the local context is not
available.

🤖 Prepared with Claude Code

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

src/Init/Notation.lean

@@ -910,6 +910,8 @@ When messages contain autogenerated names (e.g., metavariables like `?m.47`), th
 differ between runs or Lean versions. Use `set_option pp.mvars.anonymous false` to replace
 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 `_`.
 
 For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop
 everything else.

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -46,8 +46,12 @@ def delabFVar : Delab := do
     let l ← fvarId.getDecl
     maybeAddBlockImplicit (mkIdent l.userName)
   catch _ =>
-    -- loose free variable, use internal name
-    maybeAddBlockImplicit <| mkIdent (fvarId.name.replacePrefix `_uniq `_fvar)
+    -- loose free variable
+    if ← getPPOption getPPFVarsAnonymous then
+      -- use internal name like `_fvar.22`
+      maybeAddBlockImplicit <| mkIdent (fvarId.name.replacePrefix `_uniq `_fvar)
+    else
+      maybeAddBlockImplicit <| mkIdent `_
 
 -- loose bound variable, use pseudo syntax
 @[builtin_delab bvar]

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -130,6 +130,11 @@ register_builtin_option pp.mvars.delayed : Bool := {
   defValue := false
   descr    := "(pretty printer) display delayed assigned metavariables when true, otherwise display what they are assigned to"
 }
+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`."
+}
 register_builtin_option pp.beta : Bool := {
   defValue := false
   descr    := "(pretty printer) apply beta-reduction when pretty printing"
@@ -271,6 +276,7 @@ def getPPMVarsAnonymous (o : Options) : Bool := o.get pp.mvars.anonymous.name (p
 def getPPMVarsLevels (o : Options) : Bool := o.get pp.mvars.levels.name (pp.mvars.levels.defValue && getPPMVarsAnonymous o)
 def getPPMVarsWithType (o : Options) : Bool := o.get pp.mvars.withType.name pp.mvars.withType.defValue
 def getPPMVarsDelayed (o : Options) : Bool := o.get pp.mvars.delayed.name (pp.mvars.delayed.defValue || getPPAll o)
+def getPPFVarsAnonymous (o : Options) : Bool := o.get pp.fvars.anonymous.name pp.fvars.anonymous.defValue
 def getPPBeta (o : Options) : Bool := o.get pp.beta.name pp.beta.defValue
 def getPPSafeShadowing (o : Options) : Bool := o.get pp.safeShadowing.name pp.safeShadowing.defValue
 def getPPProofs (o : Options) : Bool := o.get pp.proofs.name (pp.proofs.defValue || getPPAll o)

tests/lean/run/ppFVarsAnonymous.lean

@@ -0,0 +1,27 @@
+import Lean
+
+/-!
+# Tests for `pp.fvars.anonymous`
+
+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 `_`.
+-/
+
+open Lean Elab Command in
+#guard_msgs in
+run_cmd liftTermElabM do
+  let fvarId : FVarId := { name := .num `_uniq 42 }
+  let e := Expr.fvar fvarId
+  let fmt ← Meta.ppExpr e
+  guard <| s!"{fmt}" == "_fvar.42"
+
+set_option pp.fvars.anonymous false in
+open Lean Elab Command in
+#guard_msgs in
+run_cmd liftTermElabM do
+  let fvarId : FVarId := { name := .num `_uniq 42 }
+  let e := Expr.fvar fvarId
+  let fmt ← Meta.ppExpr e
+  guard <| s!"{fmt}" == "_"