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

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.

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