diff --git a/RELEASES.md b/RELEASES.md index 2b75b7ab7f9b5..bdb234f00eb3b 100644 --- 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 ---------