From 40936d52bd71853e8317d6f4045ae31210c15d83 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 Jul 2022 12:32:15 -0700 Subject: [PATCH] chore: improve `[deprecated]` example at release notes --- RELEASES.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/RELEASES.md b/RELEASES.md index fd98b691e6..b02cff5e04 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -14,13 +14,17 @@ Unreleased ```lean def g (x : Nat) := x + 1 - -- Whenever `f` is used, a warning message is generated suggestiong to use `g` instead. + -- Whenever `f` is used, a warning message is generated suggesting to use `g` instead. @[deprecated g] def f (x : Nat) := x + 1 + #check f 0 -- warning: `f` has been deprecated, use `g` instead + -- Whenever `h` is used, a warning message is generated. @[deprecated] def h (x : Nat) := x + 1 + + #check h 0 -- warning: `h` has been deprecated ``` * Add type `LevelMVarId` (and abbreviation `LMVarId`) for universe level metavariable ids.