.

releases_drafts/list_lex.md

@@ -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.

src/CMakeLists.txt

@@ -10,7 +10,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 16)
+set(LEAN_VERSION_MINOR 17)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")