feat: delaborator for Char literals

src/Init/Meta.lean

@@ -587,6 +587,9 @@ def mkLit (kind : SyntaxNodeKind) (val : String) (info := SourceInfo.none) : TSy
   let atom : Syntax := Syntax.atom info val
   mkNode kind #[atom]
 
+def mkCharLit (val : Char) (info := SourceInfo.none) : CharLit :=
+  mkLit charLitKind (Char.quote val) info
+
 def mkStrLit (val : String) (info := SourceInfo.none) : StrLit :=
   mkLit strLitKind (String.quote val) info
 
@@ -1004,6 +1007,7 @@ instance [Quote α k] [CoeHTCT (TSyntax k) (TSyntax [k'])] : Quote α k' := ⟨f
 
 instance : Quote Term := ⟨id⟩
 instance : Quote Bool := ⟨fun | true => mkCIdent ``Bool.true | false => mkCIdent ``Bool.false⟩
+instance : Quote Char charLitKind := ⟨Syntax.mkCharLit⟩
 instance : Quote String strLitKind := ⟨Syntax.mkStrLit⟩
 instance : Quote Nat numLitKind := ⟨fun n => Syntax.mkNumLit <| toString n⟩
 instance : Quote Substring := ⟨fun s => Syntax.mkCApp ``String.toSubstring' #[quote s.toString]⟩

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -681,6 +681,13 @@ def delabLetE : Delab := do
     `(let $(mkIdent n) : $stxT := $stxV; $stxB)
   else `(let $(mkIdent n) := $stxV; $stxB)
 
+@[builtin_delab app.Char.ofNat]
+def delabChar : Delab := do
+  let e ← getExpr
+  guard <| e.getAppNumArgs == 1
+  let .lit (.natVal n) := e.appArg! | failure
+  return quote (Char.ofNat n)
+
 @[builtin_delab lit]
 def delabLit : Delab := do
   let Expr.lit l ← getExpr | unreachable!

src/Lean/ToExpr.lean

@@ -39,7 +39,7 @@ instance : ToExpr Bool where
   toTypeExpr := mkConst ``Bool
 
 instance : ToExpr Char where
-  toExpr     := fun c => mkApp (mkConst ``Char.ofNat) (toExpr c.toNat)
+  toExpr     := fun c => mkApp (mkConst ``Char.ofNat) (mkRawNatLit c.toNat)
   toTypeExpr := mkConst ``Char
 
 instance : ToExpr String where