fix: pretty printing loose bvars

Fixes #192

src/Lean/Delaborator.lean

@@ -261,7 +261,7 @@ catch
 @[builtinDelab bvar]
 def delabBVar : Delab := do
 Expr.bvar idx _ ← getExpr | unreachable!;
-pure $ mkIdent $ "#" ++ toString idx
+pure $ mkIdent $ mkNameSimple $ "#" ++ toString idx
 
 @[builtinDelab mvar]
 def delabMVar : Delab := do

src/Lean/PrettyPrinter/Formatter.lean

@@ -289,7 +289,9 @@ let id := id.simpMacroScopes;
 let s := id.toString;
 if id.isAnonymous then
   pushToken "[anonymous]"
-else if LocalContext.isInaccessibleUserName id || id.components.any Name.isNum then
+else if LocalContext.isInaccessibleUserName id || id.components.any Name.isNum ||
+  -- loose bvar
+  "#".isPrefixOf s then
   -- not parsable anyway, output as-is
   pushToken s
 else do {

tests/lean/ppExpr.lean

@@ -0,0 +1,11 @@
+import Lean
+new_frontend
+
+/-! Pretty printing tests for `Expr`s that cannot be generated by parsing+elaborating. -/
+
+open Lean
+
+def test (e : Expr) : MetaM Unit :=
+PrettyPrinter.ppExpr Name.anonymous [] e >>= IO.println
+
+#eval test (mkBVar 0)

tests/lean/ppExpr.lean.expected.out

@@ -0,0 +1 @@
+#0