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

chore: cherry-pick release notes from releases/v4.15.0 and releases/v4.16.0 (#6520)

Browse source 
These release notes were automatically generated by the script in #6519.
This commit is contained in:
Kim Morrison 2025-01-04 12:25:33 +11:00 • committed by GitHub
parent 58d178e68f
commit d991feddad
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 1185 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1187
RELEASES.md
View file

File diff suppressed because it is too large Load diff

16
releases_drafts/list_lex.md
View file

@ -1,16 +0,0 @@
We replace the inductive predicate `List.lt` with an upstreamed version of `List.Lex` from Mathlib.
(Previously `Lex.lt` was defined in terms of `<`; now it is generalized to take an arbitrary relation.)
This subtely changes the notion of ordering on `List α`.
`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.