feat: pp.numeralTypes option for printing number literals with type…

… ascriptions

This was a pretty printer option in the Lean 3 community edition, and it was useful for debugging how arithmetic expressions elaborated or have been otherwise transformed. For example, the real numbers have two exponentiation operations (Real -> Real -> Real and Real -> Nat -> Real) and it is helpful knowing at a glance which of these is `x ^ 2`.

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -600,7 +600,11 @@ def delabLit : Delab := do
 @[builtin_delab app.OfNat.ofNat]
 def delabOfNat : Delab := whenPPOption getPPCoercions do
   let .app (.app _ (.lit (.natVal n))) _ ← getExpr | failure
-  return quote n
+  if ← getPPOption getPPNumeralTypes then
+    let ty ← SubExpr.withNaryArg 0 delab
+    `(($(quote n) : $ty))
+  else
+    return quote n
 
 -- `@OfDecimal.ofDecimal _ _ m s e` ~> `m*10^(sign * e)` where `sign == 1` if `s = false` and `sign = -1` if `s = true`
 @[builtin_delab app.OfScientific.ofScientific]

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -63,6 +63,11 @@ register_builtin_option pp.letVarTypes : Bool := {
   group    := "pp"
   descr    := "(pretty printer) display types of let-bound variables"
 }
+register_builtin_option pp.numeralTypes : Bool := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) display types of numeric literals"
+}
 register_builtin_option pp.instantiateMVars : Bool := {
   defValue := false -- TODO: default to true?
   group    := "pp"
@@ -183,6 +188,7 @@ def getPPAll (o : Options) : Bool := o.get pp.all.name false
 def getPPFunBinderTypes (o : Options) : Bool := o.get pp.funBinderTypes.name (getPPAll o)
 def getPPPiBinderTypes (o : Options) : Bool := o.get pp.piBinderTypes.name pp.piBinderTypes.defValue
 def getPPLetVarTypes (o : Options) : Bool := o.get pp.letVarTypes.name (getPPAll o)
+def getPPNumeralTypes (o : Options) : Bool := o.get pp.numeralTypes.name pp.numeralTypes.defValue
 def getPPCoercions (o : Options) : Bool := o.get pp.coercions.name (!getPPAll o)
 def getPPExplicit (o : Options) : Bool := o.get pp.explicit.name (getPPAll o)
 def getPPNotation (o : Options) : Bool := o.get pp.notation.name (!getPPAll o)

tests/lean/ppNumeralTypes.lean

@@ -0,0 +1,14 @@
+set_option pp.numeralTypes true
+
+#check (17 : Fin 22)
+
+-- Doesn't apply to nat literals
+#check nat_lit 2
+
+#check 2
+
+#check 2 + 1 = 3
+
+set_option pp.all true
+
+#check 2

tests/lean/ppNumeralTypes.lean.expected.out

@@ -0,0 +1,5 @@
+(17 : Fin (22 : Nat)) : Fin (22 : Nat)
+2 : Nat
+(2 : Nat) : Nat
+(2 : Nat) + (1 : Nat) = (3 : Nat) : Prop
+@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2) : Nat