chore: change pp.natLit to be enabled by default

leanprover · Dec 24, 2024 · 65b00c9 · 65b00c9
1 parent b18f3a3
commit 65b00c9
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean
@@ -85,7 +85,7 @@ register_builtin_option pp.letVarTypes : Bool := {
   descr    := "(pretty printer) display types of let-bound variables"
 }
 register_builtin_option pp.natLit : Bool := {
-  defValue := false
+  defValue := true
   group    := "pp"
   descr    := "(pretty printer) display raw natural number literals with `nat_lit` prefix"
 }