chore: clear releases_drafts for start of 4.10.0 (#4377)
This commit is contained in:
parent
a99007ac75
commit
63739a42f3
2 changed files with 0 additions and 25 deletions
|
|
@ -1,13 +0,0 @@
|
|||
* 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`.
|
||||
|
||||
part of #3929
|
||||
|
|
@ -1,12 +0,0 @@
|
|||
Functions defined by well-founded recursion are now marked as
|
||||
`@[irreducible]`, which should prevent expensive and often unfruitful
|
||||
unfolding of such definitions.
|
||||
|
||||
Existing proofs that hold by definitional equality (e.g. `rfl`) can be
|
||||
rewritten to explictly unfold the function definition (using `simp`,
|
||||
`unfold`, `rw`), or the recursive function can be temporariliy made
|
||||
semireducible (using `unseal f in` before the command) or the function
|
||||
definition itself can be marked as `@[semireducible]` to get the previous
|
||||
behavor.
|
||||
|
||||
#4061
|
||||
Loading…
Add table
Reference in a new issue