6893913683
This PR replaces `List.lt` with `List.Lex`, from Mathlib, and adds the new `Bool` valued lexicographic comparatory function `List.lex`. This subtly changes the definition of `<` on Lists in some situations. `List.lt` was a weaker relation: in particular if `l₁ < l₂`, then `a :: l₁ < b :: l₂` may hold according to `List.lt` even if `a` and `b` are merely incomparable (either neither `a < b` nor `b < a`), whereas according to `List.Lex` this would require `a = b`. When `<` is total, in the sense that `¬ · < ·` is antisymmetric, then the two relations coincide. Mathlib was already overriding the order instances for `List α`, so this change should not be noticed by anyone already using Mathlib. We simultaneously add the boolean valued `List.lex` function, parameterised by a `BEq` typeclass and an arbitrary `lt` function. This will support the flexibility previously provided for `List.lt`, via a `==` function which is weaker than strict equality. |
||
|---|---|---|
| .. | ||
| list_lex.md | ||
| README.md | ||
Draft release notes
This folder contains drafts of release notes for inclusion in RELEASES.md.
During the process to create a release candidate, we look through all the commits that make up the release
to prepare the release notes, and in that process we take these drafts into account.
Guidelines:
- You should prefer adding release notes to commit messages over adding anything to this folder. A release note should briefly explain the impact of a change from a user's point of view. Please mark these parts out with words such as release notes and/or breaking changes.
- It is not necessary to add anything to this folder. It is meant for larger features that span multiple PRs, or for anything that would be helpful when preparing the release notes that might be missed by someone reading through the change log.
- If the PR that adds a feature simultaneously adds a draft release note, including the PR number is not required since it can be obtained from the git history for the file.
When release notes are prepared, all the draft release notes are deleted from this folder.
For release candidates beyond the first one, you can either update RELEASE.md directly
or continue to add drafts.
When a release is finalized, we will copy the completed release notes from RELEASE.md to the master branch.