feat: add Context.setConfig

src/Init/Core.lean

@@ -1922,12 +1922,12 @@ represents an element of `Squash α` the same as `α` itself
 `Squash.lift` will extract a value in any subsingleton `β` from a function on `α`,
 while `Nonempty.rec` can only do the same when `β` is a proposition.
 -/
-def Squash (α : Sort u) := Quot (fun (_ _ : α) => True)
+def Squash (α : Type u) := Quot (fun (_ _ : α) => True)
 
 /-- The canonical quotient map into `Squash α`. -/
-def Squash.mk {α : Sort u} (x : α) : Squash α := Quot.mk _ x
+def Squash.mk {α : Type u} (x : α) : Squash α := Quot.mk _ x
 
-theorem Squash.ind {α : Sort u} {motive : Squash α → Prop} (h : ∀ (a : α), motive (Squash.mk a)) : ∀ (q : Squash α), motive q :=
+theorem Squash.ind {α : Type u} {motive : Squash α → Prop} (h : ∀ (a : α), motive (Squash.mk a)) : ∀ (q : Squash α), motive q :=
   Quot.ind h
 
 /-- If `β` is a subsingleton, then a function `α → β` lifts to `Squash α → β`. -/

src/Init/Data/Array.lean

@@ -18,4 +18,3 @@ import Init.Data.Array.Bootstrap
 import Init.Data.Array.GetLit
 import Init.Data.Array.MapIdx
 import Init.Data.Array.Set
-import Init.Data.Array.Monadic

src/Init/Data/Array/Attach.lean

@@ -43,13 +43,6 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
     l.attach.toList = l.toList.attachWith (· ∈ l) (by simp [mem_toList]) := by
   simp [attach]
 
-@[simp] theorem _root_.List.attachWith_mem_toArray {l : List α} :
-    l.attachWith (fun x => x ∈ l.toArray) (fun x h => by simpa using h) =
-      l.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
-  simp only [List.attachWith, List.attach, List.map_pmap]
-  apply List.pmap_congr_left
-  simp
-
 /-! ## unattach
 
 `Array.unattach` is the (one-sided) inverse of `Array.attach`. It is a synonym for `Array.map Subtype.val`.
@@ -90,7 +83,7 @@ def unattach {α : Type _} {p : α → Prop} (l : Array { x // p x }) := l.map (
 
 @[simp] theorem unattach_attach {l : Array α} : l.attach.unattach = l := by
   cases l
-  simp only [List.attach_toArray, List.unattach_toArray, List.unattach_attachWith]
+  simp
 
 @[simp] theorem unattach_attachWith {p : α → Prop} {l : Array α}
     {H : ∀ a ∈ l, p a} :

src/Init/Data/Array/Bootstrap.lean

@@ -15,26 +15,26 @@ This file contains some theorems about `Array` and `List` needed for `Init.Data.
 
 namespace Array
 
-theorem foldlM_toList.aux [Monad m]
+theorem foldlM_eq_foldlM_toList.aux [Monad m]
     (f : β → α → m β) (arr : Array α) (i j) (H : arr.size ≤ i + j) (b) :
     foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.toList.drop j).foldlM f b := by
   unfold foldlM.loop
   split; split
   · cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
   · rename_i i; rw [Nat.succ_add] at H
-    simp [foldlM_toList.aux f arr i (j+1) H]
+    simp [foldlM_eq_foldlM_toList.aux f arr i (j+1) H]
     rw (occs := .pos [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
     rfl
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
 
-@[simp] theorem foldlM_toList [Monad m]
+theorem foldlM_eq_foldlM_toList [Monad m]
     (f : β → α → m β) (init : β) (arr : Array α) :
-    arr.toList.foldlM f init = arr.foldlM f init := by
-  simp [foldlM, foldlM_toList.aux]
+    arr.foldlM f init = arr.toList.foldlM f init := by
+  simp [foldlM, foldlM_eq_foldlM_toList.aux]
 
-@[simp] theorem foldl_toList (f : β → α → β) (init : β) (arr : Array α) :
-    arr.toList.foldl f init = arr.foldl f init :=
-  List.foldl_eq_foldlM .. ▸ foldlM_toList ..
+theorem foldl_eq_foldl_toList (f : β → α → β) (init : β) (arr : Array α) :
+    arr.foldl f init = arr.toList.foldl f init :=
+  List.foldl_eq_foldlM .. ▸ foldlM_eq_foldlM_toList ..
 
 theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
     (f : α → β → m β) (arr : Array α) (init : β) (i h) :
@@ -51,23 +51,23 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init
   match arr, this with | _, .inl rfl => rfl | arr, .inr h => ?_
   simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]
 
-@[simp] theorem foldrM_toList [Monad m]
+theorem foldrM_eq_foldrM_toList [Monad m]
     (f : α → β → m β) (init : β) (arr : Array α) :
-    arr.toList.foldrM f init = arr.foldrM f init := by
+    arr.foldrM f init = arr.toList.foldrM f init := by
   rw [foldrM_eq_reverse_foldlM_toList, List.foldlM_reverse]
 
-@[simp] theorem foldr_toList (f : α → β → β) (init : β) (arr : Array α) :
-    arr.toList.foldr f init = arr.foldr f init :=
-  List.foldr_eq_foldrM .. ▸ foldrM_toList ..
+theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α) :
+    arr.foldr f init = arr.toList.foldr f init :=
+  List.foldr_eq_foldrM .. ▸ foldrM_eq_foldrM_toList ..
 
 @[simp] theorem push_toList (arr : Array α) (a : α) : (arr.push a).toList = arr.toList ++ [a] := by
   simp [push, List.concat_eq_append]
 
 @[simp] theorem toListAppend_eq (arr : Array α) (l) : arr.toListAppend l = arr.toList ++ l := by
-  simp [toListAppend, ← foldr_toList]
+  simp [toListAppend, foldr_eq_foldr_toList]
 
 @[simp] theorem toListImpl_eq (arr : Array α) : arr.toListImpl = arr.toList := by
-  simp [toListImpl, ← foldr_toList]
+  simp [toListImpl, foldr_eq_foldr_toList]
 
 @[simp] theorem pop_toList (arr : Array α) : arr.pop.toList = arr.toList.dropLast := rfl
 
@@ -76,7 +76,7 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init
 @[simp] theorem toList_append (arr arr' : Array α) :
     (arr ++ arr').toList = arr.toList ++ arr'.toList := by
   rw [← append_eq_append]; unfold Array.append
-  rw [← foldl_toList]
+  rw [foldl_eq_foldl_toList]
   induction arr'.toList generalizing arr <;> simp [*]
 
 @[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
@@ -98,44 +98,20 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init
   rw [← appendList_eq_append]; unfold Array.appendList
   induction l generalizing arr <;> simp [*]
 
-@[deprecated "Use the reverse direction of `foldrM_toList`." (since := "2024-11-13")]
-theorem foldrM_eq_foldrM_toList [Monad m]
-    (f : α → β → m β) (init : β) (arr : Array α) :
-    arr.foldrM f init = arr.toList.foldrM f init := by
-  simp
+@[deprecated foldlM_eq_foldlM_toList (since := "2024-09-09")]
+abbrev foldlM_eq_foldlM_data := @foldlM_eq_foldlM_toList
 
-@[deprecated "Use the reverse direction of `foldlM_toList`." (since := "2024-11-13")]
-theorem foldlM_eq_foldlM_toList [Monad m]
-    (f : β → α → m β) (init : β) (arr : Array α) :
-    arr.foldlM f init = arr.toList.foldlM f init:= by
-  simp
-
-@[deprecated "Use the reverse direction of `foldr_toList`." (since := "2024-11-13")]
-theorem foldr_eq_foldr_toList
-    (f : α → β → β) (init : β) (arr : Array α) :
-    arr.foldr f init = arr.toList.foldr f init := by
-  simp
-
-@[deprecated "Use the reverse direction of `foldl_toList`." (since := "2024-11-13")]
-theorem foldl_eq_foldl_toList
-    (f : β → α → β) (init : β) (arr : Array α) :
-    arr.foldl f init = arr.toList.foldl f init:= by
-  simp
-
-@[deprecated foldlM_toList (since := "2024-09-09")]
-abbrev foldlM_eq_foldlM_data := @foldlM_toList
-
-@[deprecated foldl_toList (since := "2024-09-09")]
-abbrev foldl_eq_foldl_data := @foldl_toList
+@[deprecated foldl_eq_foldl_toList (since := "2024-09-09")]
+abbrev foldl_eq_foldl_data := @foldl_eq_foldl_toList
 
 @[deprecated foldrM_eq_reverse_foldlM_toList (since := "2024-09-09")]
 abbrev foldrM_eq_reverse_foldlM_data := @foldrM_eq_reverse_foldlM_toList
 
-@[deprecated foldrM_toList (since := "2024-09-09")]
-abbrev foldrM_eq_foldrM_data := @foldrM_toList
+@[deprecated foldrM_eq_foldrM_toList (since := "2024-09-09")]
+abbrev foldrM_eq_foldrM_data := @foldrM_eq_foldrM_toList
 
-@[deprecated foldr_toList (since := "2024-09-09")]
-abbrev foldr_eq_foldr_data := @foldr_toList
+@[deprecated foldr_eq_foldr_toList (since := "2024-09-09")]
+abbrev foldr_eq_foldr_data := @foldr_eq_foldr_toList
 
 @[deprecated push_toList (since := "2024-09-09")]
 abbrev push_data := @push_toList

src/Init/Data/Array/Lemmas.lean

@@ -151,15 +151,15 @@ theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List
 
 theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
     l.toArray.foldlM f init = l.foldlM f init := by
-  rw [foldlM_toList]
+  rw [foldlM_eq_foldlM_toList]
 
 theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
     l.toArray.foldr f init = l.foldr f init := by
-  rw [foldr_toList]
+  rw [foldr_eq_foldr_toList]
 
 theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
     l.toArray.foldl f init = l.foldl f init := by
-  rw [foldl_toList]
+  rw [foldl_eq_foldl_toList]
 
 /-- Variant of `foldrM_toArray` with a side condition for the `start` argument. -/
 @[simp] theorem foldrM_toArray' [Monad m] (f : α → β → m β) (init : β) (l : List α)
@@ -174,21 +174,21 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
     (h : stop = l.toArray.size) :
     l.toArray.foldlM f init 0 stop = l.foldlM f init := by
   subst h
-  rw [foldlM_toList]
+  rw [foldlM_eq_foldlM_toList]
 
 /-- Variant of `foldr_toArray` with a side condition for the `start` argument. -/
 @[simp] theorem foldr_toArray' (f : α → β → β) (init : β) (l : List α)
     (h : start = l.toArray.size) :
     l.toArray.foldr f init start 0 = l.foldr f init := by
   subst h
-  rw [foldr_toList]
+  rw [foldr_eq_foldr_toList]
 
 /-- Variant of `foldl_toArray` with a side condition for the `stop` argument. -/
 @[simp] theorem foldl_toArray' (f : β → α → β) (init : β) (l : List α)
     (h : stop = l.toArray.size) :
     l.toArray.foldl f init 0 stop = l.foldl f init := by
   subst h
-  rw [foldl_toList]
+  rw [foldl_eq_foldl_toList]
 
 @[simp] theorem append_toArray (l₁ l₂ : List α) :
     l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
@@ -202,9 +202,6 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
 @[simp] theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by
   induction l generalizing as <;> simp [*]
 
-@[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a b => push b a) as = as ++ l.reverse.toArray := by
-  rw [foldr_eq_foldl_reverse, foldl_push]
-
 @[simp] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
     l.toArray.findSomeM? f = l.findSomeM? f := by
   rw [Array.findSomeM?]
@@ -365,8 +362,7 @@ namespace Array
 
 theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
     (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
-  simp only [foldrM_eq_reverse_foldlM_toList, push_toList, List.reverse_append, List.reverse_cons,
-    List.reverse_nil, List.nil_append, List.singleton_append, List.foldlM_cons, List.foldlM_reverse]
+  simp [foldrM_eq_reverse_foldlM_toList, -size_push]
 
 /--
 Variant of `foldrM_push` with `h : start = arr.size + 1`
@@ -392,11 +388,11 @@ rather than `(arr.push a).size` as the argument.
 @[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
 
 @[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse := by
-  rw [toListRev, ← foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]
+  rw [toListRev, foldl_eq_foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]
 
 theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
     arr.mapM f = arr.foldlM (fun bs a => bs.push <$> f a) #[] := by
-  rw [mapM, aux, ← foldlM_toList]; rfl
+  rw [mapM, aux, foldlM_eq_foldlM_toList]; rfl
 where
   aux (i r) :
       mapM.map f arr i r = (arr.toList.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
@@ -411,7 +407,7 @@ where
 
 @[simp] theorem toList_map (f : α → β) (arr : Array α) : (arr.map f).toList = arr.toList.map f := by
   rw [map, mapM_eq_foldlM]
-  apply congrArg toList (foldl_toList (fun bs a => push bs (f a)) #[] arr).symm |>.trans
+  apply congrArg toList (foldl_eq_foldl_toList (fun bs a => push bs (f a)) #[] arr) |>.trans
   have H (l arr) : List.foldl (fun bs a => push bs (f a)) arr l = ⟨arr.toList ++ l.map f⟩ := by
     induction l generalizing arr <;> simp [*]
   simp [H]
@@ -1027,7 +1023,7 @@ theorem foldr_congr {as bs : Array α} (h₀ : as = bs) {f g : α → β → β}
 
 theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
     arr.mapM f = List.toArray <$> (arr.toList.mapM f) := by
-  rw [mapM_eq_foldlM, ← foldlM_toList, ← List.foldrM_reverse]
+  rw [mapM_eq_foldlM, foldlM_eq_foldlM_toList, ← List.foldrM_reverse]
   conv => rhs; rw [← List.reverse_reverse arr.toList]
   induction arr.toList.reverse with
   | nil => simp
@@ -1152,7 +1148,7 @@ theorem getElem?_modify {as : Array α} {i : Nat} {f : α → α} {j : Nat} :
 @[simp] theorem toList_filter (p : α → Bool) (l : Array α) :
     (l.filter p).toList = l.toList.filter p := by
   dsimp only [filter]
-  rw [← foldl_toList]
+  rw [foldl_eq_foldl_toList]
   generalize l.toList = l
   suffices ∀ a, (List.foldl (fun r a => if p a = true then push r a else r) a l).toList =
       a.toList ++ List.filter p l by
@@ -1183,7 +1179,7 @@ theorem filter_congr {as bs : Array α} (h : as = bs)
 @[simp] theorem toList_filterMap (f : α → Option β) (l : Array α) :
     (l.filterMap f).toList = l.toList.filterMap f := by
   dsimp only [filterMap, filterMapM]
-  rw [← foldlM_toList]
+  rw [foldlM_eq_foldlM_toList]
   generalize l.toList = l
   have this : ∀ a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).toList =
     a.toList ++ List.filterMap f l := ?_
@@ -1262,7 +1258,7 @@ theorem getElem?_append {as bs : Array α} {n : Nat} :
 @[simp] theorem toList_flatten {l : Array (Array α)} :
     l.flatten.toList = (l.toList.map toList).flatten := by
   dsimp [flatten]
-  simp only [← foldl_toList]
+  simp only [foldl_eq_foldl_toList]
   generalize l.toList = l
   have : ∀ a : Array α, (List.foldl ?_ a l).toList = a.toList ++ ?_ := ?_
   exact this #[]

src/Init/Data/Array/Monadic.lean

@@ -1,159 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-prelude
-import Init.Data.Array.Lemmas
-import Init.Data.Array.Attach
-import Init.Data.List.Monadic
-
-/-!
-# Lemmas about `Array.forIn'` and `Array.forIn`.
--/
-
-namespace Array
-
-open Nat
-
-/-! ## Monadic operations -/
-
-/-! ### mapM -/
-
-theorem mapM_eq_foldlM_push [Monad m] [LawfulMonad m] (f : α → m β) (l : Array α) :
-    mapM f l = l.foldlM (fun acc a => return (acc.push (← f a))) #[] := by
-  rcases l with ⟨l⟩
-  simp only [List.mapM_toArray, bind_pure_comp, size_toArray, List.foldlM_toArray']
-  rw [List.mapM_eq_reverse_foldlM_cons]
-  simp only [bind_pure_comp, Functor.map_map]
-  suffices ∀ (k), (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) k l =
-      List.foldlM (fun acc a => acc.push <$> f a) k.reverse.toArray l by
-    exact this []
-  intro k
-  induction l generalizing k with
-  | nil => simp
-  | cons a as ih =>
-    simp [ih, List.foldlM_cons]
-
-/-! ### foldlM and foldrM -/
-
-theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : Array β₁) (init : α) :
-    (l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
-  cases l
-  rw [List.map_toArray] -- Why doesn't this fire via `simp`?
-  simp [List.foldlM_map]
-
-theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : Array β₁)
-    (init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
-  cases l
-  rw [List.map_toArray] -- Why doesn't this fire via `simp`?
-  simp [List.foldrM_map]
-
-theorem foldlM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : γ → β → m γ) (l : Array α) (init : γ) :
-    (l.filterMap f).foldlM g init =
-      l.foldlM (fun x y => match f y with | some b => g x b | none => pure x) init := by
-  cases l
-  rw [List.filterMap_toArray] -- Why doesn't this fire via `simp`?
-  simp [List.foldlM_filterMap]
-  rfl
-
-theorem foldrM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : β → γ → m γ) (l : Array α) (init : γ) :
-    (l.filterMap f).foldrM g init =
-      l.foldrM (fun x y => match f x with | some b => g b y | none => pure y) init := by
-  cases l
-  rw [List.filterMap_toArray] -- Why doesn't this fire via `simp`?
-  simp [List.foldrM_filterMap]
-  rfl
-
-theorem foldlM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : β → α → m β) (l : Array α) (init : β) :
-    (l.filter p).foldlM g init =
-      l.foldlM (fun x y => if p y then g x y else pure x) init := by
-  cases l
-  rw [List.filter_toArray] -- Why doesn't this fire via `simp`?
-  simp [List.foldlM_filter]
-
-theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β → m β) (l : Array α) (init : β) :
-    (l.filter p).foldrM g init =
-      l.foldrM (fun x y => if p x then g x y else pure y) init := by
-  cases l
-  rw [List.filter_toArray] -- Why doesn't this fire via `simp`?
-  simp [List.foldrM_filter]
-
-/-! ### forIn' -/
-
-/--
-We can express a for loop over an array as a fold,
-in which whenever we reach `.done b` we keep that value through the rest of the fold.
--/
-theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
-    (l : Array α) (f : (a : α) → a ∈ l → β → m (ForInStep β)) (init : β) :
-    forIn' l init f = ForInStep.value <$>
-      l.attach.foldlM (fun b ⟨a, m⟩ => match b with
-        | .yield b => f a m b
-        | .done b => pure (.done b)) (ForInStep.yield init) := by
-  cases l
-  rw [List.attach_toArray] -- Why doesn't this fire via `simp`?
-  simp only [List.forIn'_toArray, List.forIn'_eq_foldlM, List.attachWith_mem_toArray, size_toArray,
-    List.length_map, List.length_attach, List.foldlM_toArray', List.foldlM_map]
-  congr
-
-/-- We can express a for loop over an array which always yields as a fold. -/
-@[simp] theorem forIn'_yield_eq_foldlM [Monad m] [LawfulMonad m]
-    (l : Array α) (f : (a : α) → a ∈ l → β → m γ) (g : (a : α) → a ∈ l → β → γ → β) (init : β) :
-    forIn' l init (fun a m b => (fun c => .yield (g a m b c)) <$> f a m b) =
-      l.attach.foldlM (fun b ⟨a, m⟩ => g a m b <$> f a m b) init := by
-  cases l
-  rw [List.attach_toArray] -- Why doesn't this fire via `simp`?
-  simp [List.foldlM_map]
-
-theorem forIn'_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
-    (l : Array α) (f : (a : α) → a ∈ l → β → β) (init : β) :
-    forIn' l init (fun a m b => pure (.yield (f a m b))) =
-      pure (f := m) (l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init) := by
-  cases l
-  simp [List.forIn'_pure_yield_eq_foldl, List.foldl_map]
-
-@[simp] theorem forIn'_yield_eq_foldl
-    (l : Array α) (f : (a : α) → a ∈ l → β → β) (init : β) :
-    forIn' (m := Id) l init (fun a m b => .yield (f a m b)) =
-      l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by
-  cases l
-  simp [List.foldl_map]
-
-/--
-We can express a for loop over an array as a fold,
-in which whenever we reach `.done b` we keep that value through the rest of the fold.
--/
-theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
-    (f : α → β → m (ForInStep β)) (init : β) (l : Array α) :
-    forIn l init f = ForInStep.value <$>
-      l.foldlM (fun b a => match b with
-        | .yield b => f a b
-        | .done b => pure (.done b)) (ForInStep.yield init) := by
-  cases l
-  simp only [List.forIn_toArray, List.forIn_eq_foldlM, size_toArray, List.foldlM_toArray']
-  congr
-
-/-- We can express a for loop over an array which always yields as a fold. -/
-@[simp] theorem forIn_yield_eq_foldlM [Monad m] [LawfulMonad m]
-    (l : Array α) (f : α → β → m γ) (g : α → β → γ → β) (init : β) :
-    forIn l init (fun a b => (fun c => .yield (g a b c)) <$> f a b) =
-      l.foldlM (fun b a => g a b <$> f a b) init := by
-  cases l
-  simp [List.foldlM_map]
-
-theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
-    (l : Array α) (f : α → β → β) (init : β) :
-    forIn l init (fun a b => pure (.yield (f a b))) =
-      pure (f := m) (l.foldl (fun b a => f a b) init) := by
-  cases l
-  simp [List.forIn_pure_yield_eq_foldl, List.foldl_map]
-
-@[simp] theorem forIn_yield_eq_foldl
-    (l : Array α) (f : α → β → β) (init : β) :
-    forIn (m := Id) l init (fun a b => .yield (f a b)) =
-      l.foldl (fun b a => f a b) init := by
-  cases l
-  simp [List.foldl_map]
-
-end Array

src/Init/Data/Array/Subarray.lean

@@ -15,6 +15,15 @@ structure Subarray (α : Type u)  where
   start_le_stop : start ≤ stop
   stop_le_array_size : stop ≤ array.size
 
+@[deprecated Subarray.array (since := "2024-04-13")]
+abbrev Subarray.as (s : Subarray α) : Array α := s.array
+
+@[deprecated Subarray.start_le_stop (since := "2024-04-13")]
+theorem Subarray.h₁ (s : Subarray α) : s.start ≤ s.stop := s.start_le_stop
+
+@[deprecated Subarray.stop_le_array_size (since := "2024-04-13")]
+theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.array.size := s.stop_le_array_size
+
 namespace Subarray
 
 def size (s : Subarray α) : Nat :=

src/Init/Data/BitVec/Basic.lean

@@ -29,6 +29,9 @@ section Nat
 
 instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
 
+@[deprecated isLt (since := "2024-03-12")]
+theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
+
 /-- Theorem for normalizing the bit vector literal representation. -/
 -- TODO: This needs more usage data to assess which direction the simp should go.
 @[simp, bv_toNat] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = .ofNat n i := rfl

src/Init/Data/List/Impl.lean

@@ -91,7 +91,7 @@ The following operations are given `@[csimp]` replacements below:
 @[specialize] def foldrTR (f : α → β → β) (init : β) (l : List α) : β := l.toArray.foldr f init
 
 @[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by
-  funext α β f init l; simp [foldrTR, ← Array.foldr_toList, -Array.size_toArray]
+  funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_toList, -Array.size_toArray]
 
 /-! ### flatMap  -/
 
@@ -331,7 +331,7 @@ def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
     | a::as, n => by
       rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
       simp [enumFrom, f]
-  rw [← Array.foldr_toList]
+  rw [Array.foldr_eq_foldr_toList]
   simp [go]
 
 /-! ## Other list operations -/

src/Init/Data/Option/Basic.lean

@@ -16,6 +16,10 @@ def getM [Alternative m] : Option α → m α
   | none     => failure
   | some a   => pure a
 
+@[deprecated getM (since := "2024-04-17")]
+-- `[Monad m]` is not needed here.
+def toMonad [Monad m] [Alternative m] : Option α → m α := getM
+
 /-- Returns `true` on `some x` and `false` on `none`. -/
 @[inline] def isSome : Option α → Bool
   | some _ => true
@@ -24,6 +28,8 @@ def getM [Alternative m] : Option α → m α
 @[simp] theorem isSome_none : @isSome α none = false := rfl
 @[simp] theorem isSome_some : isSome (some a) = true := rfl
 
+@[deprecated isSome (since := "2024-04-17"), inline] def toBool : Option α → Bool := isSome
+
 /-- Returns `true` on `none` and `false` on `some x`. -/
 @[inline] def isNone : Option α → Bool
   | some _ => false

src/Init/Data/String/Basic.lean

@@ -514,6 +514,9 @@ instance : Inhabited String := ⟨""⟩
 
 instance : Append String := ⟨String.append⟩
 
+@[deprecated push (since := "2024-04-06")]
+def str : String → Char → String := push
+
 @[inline] def pushn (s : String) (c : Char) (n : Nat) : String :=
   n.repeat (fun s => s.push c) s
 

src/Lean/Data/NameMap.lean

@@ -33,16 +33,6 @@ def find? (m : NameMap α) (n : Name) : Option α := RBMap.find? m n
 instance : ForIn m (NameMap α) (Name × α) :=
   inferInstanceAs (ForIn _ (RBMap ..) ..)
 
-/-- `filter f m` returns the `NameMap` consisting of all
-"`key`/`val`"-pairs in `m` where `f key val` returns `true`. -/
-def filter (f : Name → α → Bool) (m : NameMap α) : NameMap α := RBMap.filter f m
-
-/-- `filterMap f m` filters an `NameMap` and simultaneously modifies the filtered values.
-
-It takes a function `f : Name → α → Option β` and applies `f name` to the value with key `name`.
-The resulting entries with non-`none` value are collected to form the output `NameMap`. -/
-def filterMap (f : Name → α → Option β) (m : NameMap α) : NameMap β := RBMap.filterMap f m
-
 end NameMap
 
 def NameSet := RBTree Name Name.quickCmp
@@ -63,9 +53,6 @@ def append (s t : NameSet) : NameSet :=
 instance : Append NameSet where
   append := NameSet.append
 
-/-- `filter f s` returns the `NameSet` consisting of all `x` in `s` where `f x` returns `true`. -/
-def filter (f : Name → Bool) (s : NameSet) : NameSet := RBTree.filter f s
-
 end NameSet
 
 def NameSSet := SSet Name
@@ -86,9 +73,6 @@ instance : EmptyCollection NameHashSet := ⟨empty⟩
 instance : Inhabited NameHashSet := ⟨{}⟩
 def insert (s : NameHashSet) (n : Name) := Std.HashSet.insert s n
 def contains (s : NameHashSet) (n : Name) : Bool := Std.HashSet.contains s n
-
-/-- `filter f s` returns the `NameHashSet` consisting of all `x` in `s` where `f x` returns `true`. -/
-def filter (f : Name → Bool) (s : NameHashSet) : NameHashSet := Std.HashSet.filter f s
 end NameHashSet
 
 def MacroScopesView.isPrefixOf (v₁ v₂ : MacroScopesView) : Bool :=

src/Lean/Data/RBMap.lean

@@ -404,24 +404,6 @@ def intersectBy {γ : Type v₁} {δ : Type v₂} (mergeFn : α → β → γ
       | some b₂ => acc.insert a <| mergeFn a b₁ b₂
       | none => acc
 
-/--
-`filter f m` returns the `RBMap` consisting of all
-"`key`/`val`"-pairs in `m` where `f key val` returns `true`.
--/
-def filter (f : α → β → Bool) (m : RBMap α β cmp) : RBMap α β cmp :=
-  m.fold (fun r k v => if f k v then r.insert k v else r) {}
-
-/--
-`filterMap f m` filters an `RBMap` and simultaneously modifies the filtered values.
-
-It takes a function `f : α → β → Option γ` and applies `f k v` to the value with key `k`.
-The resulting entries with non-`none` value are collected to form the output `RBMap`.
--/
-def filterMap (f : α → β → Option γ) (m : RBMap α β cmp) : RBMap α γ cmp :=
-  m.fold (fun r k v => match f k v with
-    | none => r
-    | some b => r.insert k b) {}
-
 end RBMap
 
 def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp :=

src/Lean/Data/RBTree.lean

@@ -114,13 +114,6 @@ def union (t₁ t₂ : RBTree α cmp) : RBTree α cmp :=
 def diff (t₁ t₂ : RBTree α cmp) : RBTree α cmp :=
   t₂.fold .erase t₁
 
-/--
-`filter f m` returns the `RBTree` consisting of all
-`x` in `m` where `f x` returns `true`.
--/
-def filter (f : α → Bool) (m : RBTree α cmp) : RBTree α cmp :=
-  RBMap.filter (fun a _ => f a) m
-
 end RBTree
 
 def rbtreeOf {α : Type u} (l : List α) (cmp : α → α → Ordering) : RBTree α cmp :=

src/Lean/Elab/StructInst.lean

@@ -900,16 +900,8 @@ partial def tryToSynthesizeDefault (structs : Array Struct) (allStructNames : Ar
           | none   =>
             let mvarDecl ← getMVarDecl mvarId
             let val ← ensureHasType mvarDecl.type val
-            /-
-            We must use `checkedAssign` here to ensure we do not create a cyclic
-            assignment. See #3150.
-            This can happen when there are holes in the the fields the default value
-            depends on.
-            Possible improvement: create a new `_` instead of returning `false` when
-            `checkedAssign` fails. Reason: the field will not be needed after the
-            other `_` are resolved by the user.
-            -/
-            mvarId.checkedAssign val
+            mvarId.assign val
+            return true
       | _ => loop (i+1) dist
     else
       return false

src/Lean/Meta/Tactic/Apply.lean

@@ -254,6 +254,10 @@ Apply `And.intro` as much as possible to goal `mvarId`.
 abbrev splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
   splitAndCore mvarId
 
+@[deprecated splitAnd (since := "2024-03-17")]
+def _root_.Lean.Meta.splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
+  mvarId.splitAnd
+
 def exfalso (mvarId : MVarId) : MetaM MVarId :=
   mvarId.withContext do
     mvarId.checkNotAssigned `exfalso

src/Std/Data/DHashMap/Internal/WF.lean

@@ -38,7 +38,7 @@ theorem toListModel_mkArray_nil {c} :
 @[simp]
 theorem computeSize_eq {buckets : Array (AssocList α β)} :
     computeSize buckets = (toListModel buckets).length := by
-  rw [computeSize, toListModel, List.flatMap_eq_foldl, Array.foldl_toList]
+  rw [computeSize, toListModel, List.flatMap_eq_foldl, Array.foldl_eq_foldl_toList]
   suffices ∀ (l : List (AssocList α β)) (l' : List ((a : α) × β a)),
       l.foldl (fun d b => d + b.toList.length) l'.length =
         (l.foldl (fun acc a => acc ++ a.toList) l').length
@@ -61,13 +61,13 @@ theorem isEmpty_eq_isEmpty [BEq α] [Hashable α] {m : Raw α β} (h : Raw.WFImp
 
 theorem fold_eq {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :
     l.fold f init = l.buckets.foldl (fun acc l => l.foldl f acc) init := by
-  simp only [Raw.fold, Raw.foldM, ← Array.foldlM_toList, Array.foldl_toList,
+  simp only [Raw.fold, Raw.foldM, Array.foldlM_eq_foldlM_toList, Array.foldl_eq_foldl_toList,
     ← List.foldl_eq_foldlM, Id.run, AssocList.foldl]
 
 theorem fold_cons_apply {l : Raw α β} {acc : List γ} (f : (a : α) → β a → γ) :
     l.fold (fun acc k v => f k v :: acc) acc =
       ((toListModel l.buckets).reverse.map (fun p => f p.1 p.2)) ++ acc := by
-  rw [fold_eq, ← Array.foldl_toList, toListModel]
+  rw [fold_eq, Array.foldl_eq_foldl_toList, toListModel]
   generalize l.buckets.toList = l
   induction l generalizing acc with
   | nil => simp

src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean

@@ -61,7 +61,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
   | nil => cases h1
   | cons hd tl ih =>
     unfold DefaultClause.ofArray at h2
-    rw [← Array.foldr_toList, List.toArray_toList] at h2
+    rw [Array.foldr_eq_foldr_toList, List.toArray_toList] at h2
     dsimp only [List.foldr] at h2
     split at h2
     · cases h2
@@ -77,7 +77,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
             · assumption
             · next heq _ _ =>
               unfold DefaultClause.ofArray
-              rw [← Array.foldr_toList, List.toArray_toList]
+              rw [Array.foldr_eq_foldr_toList, List.toArray_toList]
               exact heq
         · cases h1
           · simp only [← Option.some.inj h2]
@@ -89,7 +89,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
             apply ih
             assumption
             unfold DefaultClause.ofArray
-            rw [← Array.foldr_toList, List.toArray_toList]
+            rw [Array.foldr_eq_foldr_toList, List.toArray_toList]
             exact heq
 
 theorem CNF.Clause.convertLRAT_sat_of_sat (clause : CNF.Clause (PosFin n))

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean

@@ -106,7 +106,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
   constructor
   · simp only [ofArray]
   · have hsize : (ofArray arr).assignments.size = n := by
-      simp only [ofArray, ← Array.foldl_toList]
+      simp only [ofArray, Array.foldl_eq_foldl_toList]
       have hb : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
       have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.toList) :
         (ofArray_fold_fn acc cOpt).size = n := by rw [size_ofArray_fold_fn acc cOpt, ih]
@@ -187,7 +187,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
             exact ih i b h
     rcases List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl with ⟨_h_size, h'⟩
     intro i b h
-    simp only [ofArray, ← Array.foldl_toList] at h
+    simp only [ofArray, Array.foldl_eq_foldl_toList] at h
     exact h' i b h
 
 theorem readyForRatAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))) :
@@ -605,7 +605,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
 theorem readyForRupAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat) :
     ReadyForRupAdd f → ReadyForRupAdd (delete f arr) := by
   intro h
-  rw [delete, ← Array.foldl_toList]
+  rw [delete, Array.foldl_eq_foldl_toList]
   constructor
   · have hb : f.rupUnits = #[] := h.1
     have hl (acc : DefaultFormula n) (ih : acc.rupUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
@@ -625,7 +625,7 @@ theorem readyForRatAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat)
     ReadyForRatAdd f → ReadyForRatAdd (delete f arr) := by
   intro h
   constructor
-  · rw [delete, ← Array.foldl_toList]
+  · rw [delete, Array.foldl_eq_foldl_toList]
     have hb : f.ratUnits = #[] := h.1
     have hl (acc : DefaultFormula n) (ih : acc.ratUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
       (deleteOne acc id).ratUnits = #[] := by rw [deleteOne_preserves_ratUnits, ih]
@@ -659,7 +659,7 @@ theorem deleteOne_subset (f : DefaultFormula n) (id : Nat) (c : DefaultClause n)
 
 theorem delete_subset (f : DefaultFormula n) (arr : Array Nat) (c : DefaultClause n) :
     c ∈ toList (delete f arr) → c ∈ toList f := by
-  simp only [delete, ← Array.foldl_toList]
+  simp only [delete, Array.foldl_eq_foldl_toList]
   have hb : c ∈ toList f → c ∈ toList f := id
   have hl (f' : DefaultFormula n) (ih : c ∈ toList f' → c ∈ toList f) (id : Nat) (_ : id ∈ arr.toList) :
     c ∈ toList (deleteOne f' id) → c ∈ toList f := by intro h; exact ih <| deleteOne_subset f' id c h

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -739,7 +739,7 @@ theorem size_assignemnts_confirmRupHint {n : Nat} (clauses : Array (Option (Defa
 theorem size_assignments_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :
     (performRupCheck f rupHints).1.assignments.size = f.assignments.size := by
   simp only [performRupCheck]
-  rw [← Array.foldl_toList]
+  rw [Array.foldl_eq_foldl_toList]
   have hb : (f.assignments, ([] : CNF.Clause (PosFin n)), false, false).1.size = f.assignments.size := rfl
   have hl (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) (hsize : acc.1.size = f.assignments.size)
     (id : Nat) (_ : id ∈ rupHints.toList) : (confirmRupHint f.clauses acc id).1.size = f.assignments.size := by
@@ -1288,7 +1288,7 @@ theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_a
   have derivedLits_satisfies_invariant := derivedLitsInvariant_performRupCheck f f_assignments_size rupHints f'_assignments_size
   simp only at derivedLits_satisfies_invariant
   generalize (performRupCheck f rupHints).2.1 = derivedLits at *
-  rw [← f'_def, Array.foldl_toList]
+  rw [← f'_def, ← Array.foldl_eq_foldl_toList]
   let derivedLits_arr : Array (Literal (PosFin n)) := {toList := derivedLits}
   have derivedLits_arr_def : derivedLits_arr = {toList := derivedLits} := rfl
   have derivedLits_arr_nodup := nodup_derivedLits f f_assignments_size rupHints f'_assignments_size derivedLits
@@ -1301,7 +1301,7 @@ theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_a
     clear_insert_inductive_case f f_assignments_size derivedLits_arr derivedLits_arr_nodup idx assignments ih
   rcases Array.foldl_induction motive h_base h_inductive with ⟨h_size, h⟩
   apply Array.ext
-  · rw [← Array.foldl_toList, size_clearUnit_foldl f'.assignments clearUnit size_clearUnit derivedLits,
+  · rw [Array.foldl_eq_foldl_toList, size_clearUnit_foldl f'.assignments clearUnit size_clearUnit derivedLits,
       f'_assignments_size, f_assignments_size]
   · intro i hi1 hi2
     rw [f_assignments_size] at hi2

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean

@@ -544,7 +544,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
     (∀ l : Literal (PosFin n), reduce c assignment = reducedToUnit l → ∀ (p : (PosFin n) → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l) := by
   let c_arr := c.clause.toArray
   have c_clause_rw : c.clause = c_arr.toList := by simp [c_arr]
-  rw [reduce, c_clause_rw, Array.foldl_toList]
+  rw [reduce, c_clause_rw, ← Array.foldl_eq_foldl_toList]
   let motive := ReducePostconditionInductionMotive c_arr assignment
   have h_base : motive 0 reducedToEmpty := by
     have : ∀ (a : PosFin n) (b : Bool), (reducedToEmpty = reducedToUnit (a, b)) = False := by intros; simp

src/lake/Lake/CLI/Main.lean

@@ -515,7 +515,7 @@ protected def translateConfig : CliM PUnit := do
   if outFile?.isNone then
     IO.FS.rename pkg.configFile (pkg.configFile.addExtension "bak")
 
-def ReservoirConfig.currentSchemaVersion : StdVer := {major := 1}
+def ReservoirConfig.currentSchemaVersion : StdVer := v!"1.0.0"
 
 structure ReservoirConfig where
   name : String

src/lake/Lake/CLI/Translate/Lean.lean

@@ -119,7 +119,7 @@ def PackageConfig.mkSyntax (cfg : PackageConfig)
     |> addDeclFieldD `testDriverArgs cfg.testDriverArgs #[]
     |> addDeclFieldD `lintDriver lintDriver ""
     |> addDeclFieldD `lintDriverArgs cfg.lintDriverArgs #[]
-    |> addDeclFieldD `version cfg.version {}
+    |> addDeclFieldD `version cfg.version v!"0.0.0"
     |> addDeclField? `versionTags (quoteVerTags? cfg.versionTags)
     |> addDeclFieldD `description cfg.description ""
     |> addDeclFieldD `keywords cfg.keywords #[]

src/lake/Lake/CLI/Translate/Toml.lean

@@ -76,7 +76,7 @@ protected def PackageConfig.toToml (cfg : PackageConfig) (t : Table := {}) : Tab
   |>.smartInsert `releaseRepo (cfg.releaseRepo <|> cfg.releaseRepo?)
   |>.insertD `buildArchive (cfg.buildArchive?.getD cfg.buildArchive) (defaultBuildArchive cfg.name)
   |>.insertD `preferReleaseBuild cfg.preferReleaseBuild false
-  |>.insertD `version cfg.version {}
+  |>.insertD `version cfg.version v!"0.0.0"
   |> smartInsertVerTags cfg.versionTags
   |>.smartInsert `keywords cfg.description
   |>.smartInsert `keywords cfg.keywords

src/lake/Lake/Config/Package.lean

@@ -275,7 +275,7 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
 
   Packages without a defined version default to `0.0.0`.
   -/
-  version : StdVer := {}
+  version : StdVer := v!"0.0.0"
 
   /--
   Git tags of this package's repository that should be treated as versions.

src/lake/Lake/Load/Manifest.lean

@@ -49,7 +49,7 @@ That is, Lake ignores the `-` suffix.
 - `"1.0.0"`: Switches to a semantic versioning scheme
 - `"1.1.0"`: Add optional `scope` package entry field
 -/
-@[inline] def Manifest.version : StdVer := {major := 1, minor := 1}
+@[inline] def Manifest.version : StdVer := v!"1.1.0"
 
 /-- Manifest version `0.6.0` package entry. For backwards compatibility. -/
 inductive PackageEntryV6
@@ -201,14 +201,14 @@ protected def fromJson? (json : Json) : Except String Manifest := do
   if ver.major > 1 then
     throw s!"manifest version '{ver}' is of a higher major version than this \
       Lake's '{Manifest.version}'; you may need to update your 'lean-toolchain'"
-  else if ver < {minor := 5} then
+  else if ver < v!"0.5.0" then
     throw s!"incompatible manifest version '{ver}'"
   else
     let name ← obj.getD "name" Name.anonymous
     let lakeDir ← obj.getD "lakeDir" defaultLakeDir
     let packagesDir? ← obj.get? "packagesDir"
     let packages ←
-      if ver < {minor := 7} then
+      if ver < v!"0.7.0" then
         (·.map PackageEntry.ofV6) <$> obj.getD "packages" #[]
       else
         obj.getD "packages" #[]

src/lake/Lake/Load/Toml.lean

@@ -207,7 +207,7 @@ protected def PackageConfig.decodeToml (t : Table) (ref := Syntax.missing) : Exc
   let testDriverArgs ← t.tryDecodeD `testDriverArgs #[]
   let lintDriver ← t.tryDecodeD `lintDriver ""
   let lintDriverArgs ← t.tryDecodeD `lintDriverArgs #[]
-  let version : StdVer ← t.tryDecodeD `version {}
+  let version : StdVer ← t.tryDecodeD `version v!"0.0.0"
   let versionTags ← optDecodeD defaultVersionTags (t.find? `versionTags)
     <| StrPat.decodeToml (presets := versionTagPresets)
   let description ← t.tryDecodeD `description ""

tests/lean/run/3150.lean

@@ -1,24 +0,0 @@
-class One (α : Type) where
-  one : α
-
-variable (R A : Type) [One R] [One A]
-
-class OneHom where
-  toFun : R → A
-  map_one : toFun One.one = One.one
-
-structure Subone where
-  mem : R → Prop
-  one_mem : mem One.one
-
-structure Subalgebra [OneHom R A] extends Subone A : Type where
-  algebraMap_mem : ∀ r : R, mem (OneHom.toFun r)
-  one_mem := OneHom.map_one (R := R) (A := A) ▸ algebraMap_mem One.one
-
-/--
-error: fields missing: 'one_mem'
--/
-#guard_msgs in
-example [OneHom R A] : Subalgebra R A where
-  mem := _
-  algebraMap_mem := _