Merge branch 'main' into derive-toExpr

CODEOWNERS

@@ -4,7 +4,7 @@
 # Listed persons will automatically be asked by GitHub to review a PR touching these paths.
 # If multiple names are listed, a review by any of them is considered sufficient by default.
 
-/.github/ @Kha @kim-em
+/.github/ @kim-em
 /RELEASES.md @kim-em
 /src/kernel/ @leodemoura
 /src/lake/ @tydeu
@@ -14,9 +14,7 @@
 /src/Lean/Elab/Tactic/ @kim-em
 /src/Lean/Language/ @Kha
 /src/Lean/Meta/Tactic/ @leodemoura
-/src/Lean/Parser/ @Kha
-/src/Lean/PrettyPrinter/ @Kha
-/src/Lean/PrettyPrinter/Delaborator/ @kmill
+/src/Lean/PrettyPrinter/ @kmill
 /src/Lean/Server/ @mhuisi
 /src/Lean/Widget/ @Vtec234
 /src/Init/Data/ @kim-em

doc/lexical_structure.md

@@ -128,16 +128,16 @@ Numeric literals can be specified in various bases.
 
 ```
    numeral    : numeral10 | numeral2 | numeral8 | numeral16
-   numeral10  : [0-9]+
-   numeral2   : "0" [bB] [0-1]+
-   numeral8   : "0" [oO] [0-7]+
-   numeral16  : "0" [xX] hex_char+
+   numeral10  : [0-9]+ ("_"+ [0-9]+)*
+   numeral2   : "0" [bB] ("_"* [0-1]+)+
+   numeral8   : "0" [oO] ("_"* [0-7]+)+
+   numeral16  : "0" [xX] ("_"* hex_char+)+
 ```
 
 Floating point literals are also possible with optional exponent:
 
 ```
-   float    : [0-9]+ "." [0-9]+ [[eE[+-][0-9]+]
+   float    : numeral10 "." numeral10? [eE[+-]numeral10]
 ```
 
 For example:
@@ -147,6 +147,7 @@ constant w : Int := 55
 constant x : Nat := 26085
 constant y : Nat := 0x65E5
 constant z : Float := 2.548123e-05
+constant b : Bool := 0b_11_01_10_00
 ```
 
 Note: that negative numbers are created by applying the "-" negation prefix operator to the number, for example:

doc/monads/readers.lean

@@ -139,7 +139,7 @@ You might be wondering, how does the context actually move through the `ReaderM`
 add an input argument to a function by modifying its return type?  There is a special command in
 Lean that will show you the reduced types:
 -/
-#reduce ReaderM Environment String   -- Environment → String
+#reduce (types := true) ReaderM Environment String   -- Environment → String
 /-!
 And you can see here that this type is actually a function!  It's a function that takes an
 `Environment` as input and returns a `String`.
@@ -196,4 +196,4 @@ entirely.
 
 Now it's time to move on to [StateM Monad](states.lean.md) which is like a `ReaderM` that is
 also updatable.
--/
+-/

src/Init/Data.lean

@@ -21,6 +21,7 @@ import Init.Data.Fin
 import Init.Data.UInt
 import Init.Data.SInt
 import Init.Data.Float
+import Init.Data.Float32
 import Init.Data.Option
 import Init.Data.Ord
 import Init.Data.Random

src/Init/Data/Array/Basic.lean

@@ -11,7 +11,7 @@ import Init.Data.UInt.BasicAux
 import Init.Data.Repr
 import Init.Data.ToString.Basic
 import Init.GetElem
-import Init.Data.List.ToArray
+import Init.Data.List.ToArrayImpl
 import Init.Data.Array.Set
 
 universe u v w
@@ -85,6 +85,8 @@ theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
 
 @[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
 
+@[simp] theorem getElem?_toList {a : Array α} {i : Nat} : a.toList[i]? = a[i]? := rfl
+
 /-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
 -- NB: This is defined as a structure rather than a plain def so that a lemma
 -- like `sizeOf_lt_of_mem` will not apply with no actual arrays around.
@@ -97,6 +99,9 @@ instance : Membership α (Array α) where
 theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
   ⟨fun | .mk h => h, Array.Mem.mk⟩
 
+@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
+  simp [mem_def]
+
 @[simp] theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
   rw [Array.mem_def, ← getElem_toList]
   apply List.getElem_mem
@@ -242,7 +247,7 @@ def singleton (v : α) : Array α :=
   mkArray 1 v
 
 def back! [Inhabited α] (a : Array α) : α :=
-  a.get! (a.size - 1)
+  a[a.size - 1]!
 
 @[deprecated back! (since := "2024-10-31")] abbrev back := @back!
 
@@ -658,7 +663,7 @@ def all (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool
   Id.run <| as.allM p start stop
 
 def contains [BEq α] (as : Array α) (a : α) : Bool :=
-  as.any (· == a)
+  as.any (a == ·)
 
 def elem [BEq α] (a : α) (as : Array α) : Bool :=
   as.contains a

src/Init/Data/Array/Find.lean

@@ -81,7 +81,7 @@ theorem getElem_zero_flatten.proof {L : Array (Array α)} (h : 0 < L.flatten.siz
     (L.findSome? fun l => l[0]?).isSome := by
   cases L using array_array_induction
   simp only [List.findSome?_toArray, List.findSome?_map, Function.comp_def, List.getElem?_toArray,
-    List.findSome?_isSome_iff, List.isSome_getElem?]
+    List.findSome?_isSome_iff, isSome_getElem?]
   simp only [flatten_toArray_map_toArray, size_toArray, List.length_flatten,
     Nat.sum_pos_iff_exists_pos, List.mem_map] at h
   obtain ⟨_, ⟨xs, m, rfl⟩, h⟩ := h