Add RELEASES entry

leanprover · Jan 31, 2024 · 469be42 · 469be42
1 parent c5d6d51
commit 469be42
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/RELEASES.md b/RELEASES.md
@@ -196,6 +196,11 @@ example : x + foo 2 = 12 + x := by
 
 * Add language server support for [call hierarchy requests](https://www.youtube.com/watch?v=r5LA7ivUb2c) ([PR #3082](https://github.com/leanprover/lean4/pull/3082)). The change to the .ilean format in this PR means that projects must be fully rebuilt once in order to generate .ilean files with the new format before features like "find references" work correctly again.
 
+* Add pretty printer options `pp.numeralTypes` and `pp.natLit`.
+  When `pp.numeralTypes` is true, then natural number literals, integer literals, and rational number literals
+  are pretty printed with type ascriptions, such as `(2 : Rat)`, `(-2 : Rat)`, and `(-2 / 3 : Rat)`.
+  When `pp.natLit` is true, then raw natural number literals are pretty printed as `nat_lit 2`.
+  [PR #2933](https://github.com/leanprover/lean4/pull/2933) and [RFC #3021](https://github.com/leanprover/lean4/issues/3021).
 
 v4.5.0
 ---------