fix

src/Init/Data/Float.lean

@@ -47,25 +47,6 @@ def Float.lt : Float → Float → Prop := fun a b =>
 def Float.le : Float → Float → Prop := fun a b =>
   floatSpec.le a.val b.val
 
-/--
-Raw transmutation from `UInt64`.
-
-Floats and UInts have the same endianness on all supported platforms.
-IEEE 754 very precisely specifies the bit layout of floats.
--/
-@[extern "lean_float_from_bits"] opaque Float.fromBits : UInt64 → Float
-
-/--
-Raw transmutation to `UInt64`.
-
-Floats and UInts have the same endianness on all supported platforms.
-IEEE 754 very precisely specifies the bit layout of floats.
-
-Note that this function is distinct from `Float.toUInt64`, which attempts
-to preserve the numeric value, and not the bitwise value.
--/
-@[extern "lean_float_to_bits"] opaque Float.toBits : Float → UInt64
-
 instance : Add Float := ⟨Float.add⟩
 instance : Sub Float := ⟨Float.sub⟩
 instance : Mul Float := ⟨Float.mul⟩

src/Init/Data/List/Basic.lean

@@ -551,7 +551,7 @@ theorem reverseAux_eq_append (as bs : List α) : reverseAux as bs = reverseAux a
 /-! ### flatten -/
 
 /--
-`O(|flatten L|)`. `flatten L` concatenates all the lists in `L` into one list.
+`O(|flatten L|)`. `join L` concatenates all the lists in `L` into one list.
 * `flatten [[a], [], [b, c], [d, e, f]] = [a, b, c, d, e, f]`
 -/
 def flatten : List (List α) → List α

src/Lean/Compiler/ConstFolding.lean

@@ -133,8 +133,8 @@ def foldNatBinBoolPred (fn : Nat → Nat → Bool) (a₁ a₂ : Expr) : Option E
     return mkConst ``Bool.false
 
 def foldNatBeq := fun _ : Bool => foldNatBinBoolPred (fun a b => a == b)
-def foldNatBlt := fun _ : Bool => foldNatBinBoolPred (fun a b => a < b)
-def foldNatBle := fun _ : Bool => foldNatBinBoolPred (fun a b => a ≤ b)
+def foldNatBle := fun _ : Bool => foldNatBinBoolPred (fun a b => a < b)
+def foldNatBlt := fun _ : Bool => foldNatBinBoolPred (fun a b => a ≤ b)
 
 def natFoldFns : List (Name × BinFoldFn) :=
   [(``Nat.add, foldNatAdd),

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1092,29 +1092,19 @@ def coeDelaborator : Delab := whenPPOption getPPCoercions do
   let e ← getExpr
   let .const declName _ := e.getAppFn | failure
   let some info ← Meta.getCoeFnInfo? declName | failure
-  let n := e.getAppNumArgs
-  guard <| n ≥ info.numArgs
   if (← getPPOption getPPExplicit) && info.coercee != 0 then
     -- Approximation: the only implicit arguments come before the coercee
     failure
-  if n == info.numArgs then
-    delabHead info 0 false
-  else
-    let nargs := n - info.numArgs
-    delabAppCore nargs (delabHead info nargs) (unexpand := false)
-where
-  delabHead (info : CoeFnInfo) (nargs : Nat) (insertExplicit : Bool) : Delab := do
-    guard <| !insertExplicit
-    if info.type == .coeFun && nargs > 0 then
-      -- In the CoeFun case, annotate with the coercee itself.
-      -- We can still see the whole coercion expression by hovering over the whitespace between the arguments.
-      withNaryArg info.coercee <| withAnnotateTermInfo delab
-    else
-      withAnnotateTermInfo do
-        match info.type with
-        | .coe     => `(↑$(← withNaryArg info.coercee delab))
-        | .coeFun  => `(⇑$(← withNaryArg info.coercee delab))
-        | .coeSort => `(↥$(← withNaryArg info.coercee delab))
+  let n := e.getAppNumArgs
+  withOverApp info.numArgs do
+    match info.type with
+    | .coe => `(↑$(← withNaryArg info.coercee delab))
+    | .coeFun =>
+      if n = info.numArgs then
+        `(⇑$(← withNaryArg info.coercee delab))
+      else
+        withNaryArg info.coercee delab
+    | .coeSort => `(↥$(← withNaryArg info.coercee delab))
 
 @[builtin_delab app.dite]
 def delabDIte : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 5 do

src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean

@@ -99,5 +99,17 @@ attribute [bv_normalize] BitVec.mul_eq
 attribute [bv_normalize] BitVec.udiv_eq
 attribute [bv_normalize] BitVec.umod_eq
 
+@[bv_normalize]
+theorem Bool.and_eq_and (x y : Bool) : x.and y = (x && y) := by
+  rfl
+
+@[bv_normalize]
+theorem Bool.or_eq_or (x y : Bool) : x.or y = (x || y) := by
+  rfl
+
+@[bv_normalize]
+theorem Bool.no_eq_not (x : Bool) : x.not = !x := by
+  rfl
+
 end Normalize
 end Std.Tactic.BVDecide

src/include/lean/lean.h

@@ -1259,8 +1259,6 @@ static inline lean_obj_res lean_nat_mod(b_lean_obj_arg a1, b_lean_obj_arg a2) {
 
 static inline bool lean_nat_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
-        // This comparison is UB according to the standard but allowed as per the
-        // GCC documentation and the address sanitizer does not complain about it.
         return a1 == a2;
     } else {
         return lean_nat_big_eq(a1, a2);
@@ -1277,8 +1275,6 @@ static inline bool lean_nat_ne(b_lean_obj_arg a1, b_lean_obj_arg a2) {
 
 static inline bool lean_nat_le(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
-        // This comparison is UB according to the standard but allowed as per the
-        // GCC documentation and the address sanitizer does not complain about it.
         return a1 <= a2;
     } else {
         return lean_nat_big_le(a1, a2);
@@ -1291,8 +1287,6 @@ static inline uint8_t lean_nat_dec_le(b_lean_obj_arg a1, b_lean_obj_arg a2) {
 
 static inline bool lean_nat_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
-        // This comparison is UB according to the standard but allowed as per the
-        // GCC documentation and the address sanitizer does not complain about it.
         return a1 < a2;
     } else {
         return lean_nat_big_lt(a1, a2);
@@ -2691,8 +2685,6 @@ static inline size_t lean_float_to_usize(double a) {
     else
         return (size_t) lean_float_to_uint32(a); // NOLINT
 }
-LEAN_EXPORT double lean_float_from_bits(uint64_t u);
-LEAN_EXPORT uint64_t lean_float_to_bits(double d);
 static inline double lean_float_add(double a, double b) { return a + b; }
 static inline double lean_float_sub(double a, double b) { return a - b; }
 static inline double lean_float_mul(double a, double b) { return a * b; }

src/runtime/object.cpp

@@ -1620,21 +1620,6 @@ extern "C" LEAN_EXPORT obj_res lean_float_frexp(double a) {
     return r;
 }
 
-extern "C" LEAN_EXPORT double lean_float_from_bits(uint64_t u)
-{
-    static_assert(sizeof(double) == sizeof(u), "`double` unexpected size.");
-    double ret;
-    std::memcpy(&ret, &u, sizeof(double));
-    return ret;
-}
-
-extern "C" LEAN_EXPORT uint64_t lean_float_to_bits(double d)
-{
-    uint64_t ret;
-    std::memcpy(&ret, &d, sizeof(double));
-    return ret;
-}
-
 // =======================================
 // Strings
 

tests/lean/run/6086.lean

@@ -1,3 +0,0 @@
-/-- info: [true, true, false, true, false, false, true, true, false, true, false, false] -/
-#guard_msgs in
-#eval [Nat.ble 36 37, Nat.ble 37 37, Nat.ble 38 37, Nat.blt 36 37, Nat.blt 37 37, Nat.blt 38 37, 36 ≤ 37, 37 ≤ 37, 38 ≤ 37 ,36 < 37, 37 < 37, 38 < 37]

tests/lean/run/floatBits.lean

@@ -1,13 +0,0 @@
-def d : Float := 1.245
-
-/--
-info: 4608285800708723180
--/
-#guard_msgs in
-#eval d.toBits
-
-/--
-info: true
--/
-#guard_msgs in
-#eval Float.fromBits d.toBits == d