From f4ffebf01cabc9c7965026df23f2163e3d979a58 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 14 Oct 2020 18:38:59 +0200
Subject: [PATCH] feat: delaborator: use nicer binder name for `[anonymous]`

Fixes #193
---
 src/Lean/Delaborator.lean           | 12 ++++++++----
 tests/lean/ppExpr.lean              |  1 +
 tests/lean/ppExpr.lean.expected.out |  1 +
 3 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index a2bb33f1ae..8bda9e2fb7 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -416,14 +416,19 @@ match e with
 | Expr.forallE _ _ e'@(Expr.forallE _ _ _ _) _ => go e'
 | _ => pure false
 
+private def getUnusedName (suggestion : Name) : DelabM Name := do
+-- Use a nicer binder name than `[anonymous]`. We probably shouldn't do this in all LocalContext use cases, so do it here.
+let suggestion := if suggestion.isAnonymous then `a else suggestion;
+lctx ← getLCtx;
+pure $ lctx.getUnusedName suggestion
+
 private partial def delabBinders (delabGroup : Array Syntax → Syntax → Delab) : optParam (Array Syntax) #[] → Delab
 -- Accumulate names (`Syntax.ident`s with position information) of the current, unfinished
 -- binder group `(d e ...)` as determined by `shouldGroupWithNext`. We cannot do grouping
 -- inside-out, on the Syntax level, because it depends on comparing the Expr binder types.
 | curNames => do
-  lctx ← liftMetaM $ getLCtx;
   e ← getExpr;
-  let n := lctx.getUnusedName e.bindingName!;
+  n ← getUnusedName e.bindingName!;
   stxN ← annotateCurPos (mkIdent n);
   let curNames := curNames.push stxN;
   condM shouldGroupWithNext
@@ -486,8 +491,7 @@ delabBinders $ fun curNames stxBody => do
 @[builtinDelab letE]
 def delabLetE : Delab := do
 Expr.letE n t v b _ ← getExpr | unreachable!;
-lctx ← getLCtx;
-let n := lctx.getUnusedName n;
+n ← getUnusedName n;
 stxT ← descend t 0 delab;
 stxV ← descend v 1 delab;
 stxB ← withLetDecl n t v (fun fvar =>
diff --git a/tests/lean/ppExpr.lean b/tests/lean/ppExpr.lean
index be193c5ac7..48ee93061c 100644
--- a/tests/lean/ppExpr.lean
+++ b/tests/lean/ppExpr.lean
@@ -9,3 +9,4 @@ def test (e : Expr) : MetaM Unit :=
 PrettyPrinter.ppExpr Name.anonymous [] e >>= IO.println
 
 #eval test (mkBVar 0)
+#eval test (mkLambda Name.anonymous BinderInfo.default (mkSort levelZero) (mkBVar 0))
diff --git a/tests/lean/ppExpr.lean.expected.out b/tests/lean/ppExpr.lean.expected.out
index a0a4a0eb17..de4792f533 100644
--- a/tests/lean/ppExpr.lean.expected.out
+++ b/tests/lean/ppExpr.lean.expected.out
@@ -1 +1,2 @@
 #0
+fun (a : Prop) => a