From d569ed4e5f796bbabbe17302a7c5a7060a4c7de7 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 17 Feb 2024 17:53:37 -0800 Subject: [PATCH] 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 | 14 +++++++------- tests/lean/474.lean.expected.out | 2 +- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index e92249e2f3..305bad4e8c 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/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] diff --git a/tests/lean/474.lean.expected.out b/tests/lean/474.lean.expected.out index 168f78c4a4..bf8a88bbf7 100644 --- a/tests/lean/474.lean.expected.out +++ b/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