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