max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: move release notes about MessageData to v4.9.0 (#4222)

Browse source
This commit is contained in:
Kim Morrison 2024-05-20 11:42:30 +10:00 • committed by GitHub
parent 239ade80dc
commit 7c5249278e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
RELEASES.md
View file

@ -22,6 +22,18 @@ v4.9.0 (development in progress)
definition itself can be marked as `@[semireducible]` to get the previous
behavor.
* The `MessageData.ofPPFormat` constructor has been removed.
Its functionality has been split into two:
- for lazy structured messages, please use `MessageData.lazy`;
- for embedding `Format` or `FormatWithInfos`, use `MessageData.ofFormatWithInfos`.
An example migration can be found in [#3929](https://github.com/leanprover/lean4/pull/3929/files#diff-5910592ab7452a0e1b2616c62d22202d2291a9ebb463145f198685aed6299867L109).
* The `MessageData.ofFormat` constructor has been turned into a function.
If you need to inspect `MessageData`,
you can pattern-match on `MessageData.ofFormatWithInfos`.
v4.8.0
---------
@ -155,18 +167,6 @@ fact.def :
* `Option.toMonad` has been renamed to `Option.getM` and the unneeded `[Monad m]` instance argument has been removed.
* The `MessageData.ofPPFormat` constructor has been removed.
Its functionality has been split into two:
- for lazy structured messages, please use `MessageData.lazy`;
- for embedding `Format` or `FormatWithInfos`, use `MessageData.ofFormatWithInfos`.
An example migration can be found in [#3929](https://github.com/leanprover/lean4/pull/3929/files#diff-5910592ab7452a0e1b2616c62d22202d2291a9ebb463145f198685aed6299867L109).
* The `MessageData.ofFormat` constructor has been turned into a function.
If you need to inspect `MessageData`,
you can pattern-match on `MessageData.ofFormatWithInfos`.
v4.7.0
---------