feat: make loose fvars pretty print as _fvar.123 instead of `_uniq.…

…123` (#3380)

Loose fvars are never supposed to be pretty printed, but having them
print with "fvar" in the name can help with debugging broken tactics and
elaborators.

Metaprogramming users often do not realize at first that `_uniq.???` in
pretty printing output refers to fvars not in the current local context.

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -24,13 +24,13 @@ def unfoldMDatas : Expr → Expr
 
 @[builtin_delab fvar]
 def delabFVar : Delab := do
-let Expr.fvar fvarId ← getExpr | unreachable!
-try
-  let l ← fvarId.getDecl
-  maybeAddBlockImplicit (mkIdent l.userName)
-catch _ =>
-  -- loose free variable, use internal name
-  maybeAddBlockImplicit <| mkIdent fvarId.name
+  let Expr.fvar fvarId ← getExpr | unreachable!
+  try
+    let l ← fvarId.getDecl
+    maybeAddBlockImplicit (mkIdent l.userName)
+  catch _ =>
+    -- loose free variable, use internal name
+    maybeAddBlockImplicit <| mkIdent (fvarId.name.replacePrefix `_uniq `_fvar)
 
 -- loose bound variable, use pseudo syntax
 @[builtin_delab bvar]

tests/lean/474.lean.expected.out

@@ -1,7 +1,7 @@
 let y := Nat.zero;
 Nat.add y y
 fun y_1 => Nat.add y y_1
-fun y => Nat.add _uniq.1 y
+fun y => Nat.add _fvar.1 y
 fun (y : Nat) => Nat.add y y
 Nat.add ?m y
 Nat.add (?m #0) #0