fix: Context.setConfig must update metaConfig and indexConfig fields

This PR fixes a bug at `Context.setConfig`. It was not propagating
the configuration to the redundant fields (cache) `metaConfig` and `indexConfig`.

.github/workflows/labels-from-comments.yml

@@ -1,8 +1,7 @@
 # This workflow allows any user to add one of the `awaiting-review`, `awaiting-author`, `WIP`,
-# `release-ci`, or a `changelog-XXX` label by commenting on the PR or issue.
+# or `release-ci` labels by commenting on the PR or issue.
 # If any labels from the set {`awaiting-review`, `awaiting-author`, `WIP`} are added, other labels
 # from that set are removed automatically at the same time.
-# Similarly, if any `changelog-XXX` label is added, other `changelog-YYY` labels are removed.
 
 name: Label PR based on Comment
 
@@ -12,7 +11,7 @@ on:
 
 jobs:
   update-label:
-    if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci') || contains(github.event.comment.body, 'changelog-'))
+    if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci'))
     runs-on: ubuntu-latest
 
     steps:
@@ -21,14 +20,13 @@ jobs:
       with:
         github-token: ${{ secrets.GITHUB_TOKEN }}
         script: |
-          const { owner, repo, number: issue_number } = context.issue;
+          const { owner, repo, number: issue_number  } = context.issue;
           const commentLines = context.payload.comment.body.split('\r\n');
 
           const awaitingReview = commentLines.includes('awaiting-review');
           const awaitingAuthor = commentLines.includes('awaiting-author');
           const wip = commentLines.includes('WIP');
           const releaseCI = commentLines.includes('release-ci');
-          const changelogMatch = commentLines.find(line => line.startsWith('changelog-'));
 
           if (awaitingReview || awaitingAuthor || wip) {
             await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'awaiting-review' }).catch(() => {});
@@ -49,19 +47,3 @@ jobs:
           if (releaseCI) {
             await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['release-ci'] });
           }
-
-          if (changelogMatch) {
-            const changelogLabel = changelogMatch.trim();
-            const { data: existingLabels } = await github.rest.issues.listLabelsOnIssue({ owner, repo, issue_number });
-            const changelogLabels = existingLabels.filter(label => label.name.startsWith('changelog-'));
-
-            // Remove all other changelog labels
-            for (const label of changelogLabels) {
-              if (label.name !== changelogLabel) {
-                await github.rest.issues.removeLabel({ owner, repo, issue_number, name: label.name }).catch(() => {});
-              }
-            }
-
-            // Add the new changelog label
-            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: [changelogLabel] });
-          }

src/Init/Data/Array/Basic.lean

@@ -233,7 +233,7 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
 
 /-- The array `#[0, 1, ..., n - 1]`. -/
 def range (n : Nat) : Array Nat :=
-  ofFn fun (i : Fin n) => i
+  n.fold (flip Array.push) (mkEmpty n)
 
 def singleton (v : α) : Array α :=
   mkArray 1 v

src/Init/Data/Array/Lemmas.lean

@@ -513,10 +513,10 @@ theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = no
 theorem getD_get? (a : Array α) (i : Nat) (d : α) :
   Option.getD a[i]? d = if p : i < a.size then a[i]'p else d := by
   if h : i < a.size then
-    simp [setIfInBounds, h, getElem?_def]
+    simp [setD, h, getElem?_def]
   else
     have p : i ≥ a.size := Nat.le_of_not_gt h
-    simp [setIfInBounds, getElem?_len_le _ p, h]
+    simp [setD, getElem?_len_le _ p, h]
 
 @[simp] theorem getD_eq_get? (a : Array α) (n d) : a.getD n d = (a[n]?).getD d := by
   simp only [getD, get_eq_getElem, get?_eq_getElem?]; split <;> simp [getD_get?, *]
@@ -552,32 +552,31 @@ theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat
     (ne : i ≠ j) : (a.set i v)[j]? = a[j]? := by
   by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
 
-/-! # setIfInBounds -/
+/-! # setD -/
 
-@[simp] theorem set!_is_setIfInBounds : @set! = @setIfInBounds := rfl
+@[simp] theorem set!_is_setD : @set! = @setD := rfl
 
-@[simp] theorem size_setIfInBounds (a : Array α) (index : Nat) (val : α) :
-    (Array.setIfInBounds a index val).size = a.size := by
+@[simp] theorem size_setD (a : Array α) (index : Nat) (val : α) :
+    (Array.setD a index val).size = a.size := by
   if h : index < a.size  then
-    simp [setIfInBounds, h]
+    simp [setD, h]
   else
-    simp [setIfInBounds, h]
+    simp [setD, h]
 
-@[simp] theorem getElem_setIfInBounds_eq (a : Array α) {i : Nat} (v : α) (h : _) :
-    (setIfInBounds a i v)[i]'h = v := by
+@[simp] theorem getElem_setD_eq (a : Array α) {i : Nat} (v : α) (h : _) :
+    (setD a i v)[i]'h = v := by
   simp at h
-  simp only [setIfInBounds, h, ↓reduceDIte, getElem_set_eq]
+  simp only [setD, h, ↓reduceDIte, getElem_set_eq]
 
 @[simp]
-theorem getElem?_setIfInBounds_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) :
-    (a.setIfInBounds i v)[i]? = some v := by
+theorem getElem?_setD_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a.setD i v)[i]? = some v := by
   simp [getElem?_lt, p]
 
 /-- Simplifies a normal form from `get!` -/
-@[simp] theorem getD_get?_setIfInBounds (a : Array α) (i : Nat) (v d : α) :
-    Option.getD (setIfInBounds a i v)[i]? d = if i < a.size then v else d := by
+@[simp] theorem getD_get?_setD (a : Array α) (i : Nat) (v d : α) :
+    Option.getD (setD a i v)[i]? d = if i < a.size then v else d := by
   by_cases h : i < a.size <;>
-    simp [setIfInBounds, Nat.not_lt_of_le, h,  getD_get?]
+    simp [setD, Nat.not_lt_of_le, h,  getD_get?]
 
 /-! # ofFn -/
 
@@ -622,19 +621,6 @@ theorem getElem?_ofFn (f : Fin n → α) (i : Nat) :
     (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none := by
   simp [getElem?_def]
 
-@[simp] theorem ofFn_zero (f : Fin 0 → α) : ofFn f = #[] := rfl
-
-theorem ofFn_succ (f : Fin (n+1) → α) :
-    ofFn f = (ofFn (fun (i : Fin n) => f i.castSucc)).push (f ⟨n, by omega⟩) := by
-  ext i h₁ h₂
-  · simp
-  · simp [getElem_push]
-    split <;> rename_i h₃
-    · rfl
-    · congr
-      simp at h₁ h₂
-      omega
-
 /-! # mkArray -/
 
 @[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
@@ -769,10 +755,10 @@ theorem get_set (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a
     (h : i ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
   simp only [set, getElem_eq_getElem_toList, List.getElem_set_ne h]
 
-theorem getElem_setIfInBounds (a : Array α) (i : Nat) (v : α) (h : i < (setIfInBounds a i v).size) :
-    (setIfInBounds a i v)[i] = v := by
+theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
+    (setD a i v)[i] = v := by
   simp at h
-  simp only [setIfInBounds, h, ↓reduceDIte, getElem_set_eq]
+  simp only [setD, h, ↓reduceDIte, getElem_set_eq]
 
 theorem set_set (a : Array α) (i : Nat) (h) (v v' : α) :
     (a.set i v h).set i v' (by simp [h]) = a.set i v' := by simp [set, List.set_set]
@@ -854,10 +840,16 @@ theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rf
   simp only [reverse]; split <;> simp [go]
 
 @[simp] theorem size_range {n : Nat} : (range n).size = n := by
-  induction n <;> simp [range]
+  unfold range
+  induction n with
+  | zero      => simp [Nat.fold]
+  | succ k ih =>
+    rw [Nat.fold, flip]
+    simp only [mkEmpty_eq, size_push] at *
+    omega
 
 @[simp] theorem toList_range (n : Nat) : (range n).toList = List.range n := by
-  apply List.ext_getElem <;> simp [range]
+  induction n <;> simp_all [range, Nat.fold, flip, List.range_succ]
 
 @[simp]
 theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Array.range n)[x] = x := by
@@ -1743,10 +1735,10 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   apply ext'
   simp
 
-@[simp] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
-    l.toArray.setIfInBounds i a  = (l.set i a).toArray := by
+@[simp] theorem setD_toArray (l : List α) (i : Nat) (a : α) :
+    l.toArray.setD i a  = (l.set i a).toArray := by
   apply ext'
-  simp only [setIfInBounds]
+  simp only [setD]
   split
   · simp
   · simp_all [List.set_eq_of_length_le]
@@ -2098,8 +2090,6 @@ theorem toArray_concat {as : List α} {x : α} :
 
 @[deprecated back!_toArray (since := "2024-10-31")] abbrev back_toArray := @back!_toArray
 
-@[deprecated setIfInBounds_toArray (since := "2024-11-24")] abbrev setD_toArray := @setIfInBounds_toArray
-
 end List
 
 namespace Array
@@ -2245,11 +2235,4 @@ abbrev get_swap' := @getElem_swap'
 @[deprecated eq_push_pop_back!_of_size_ne_zero (since := "2024-10-31")]
 abbrev eq_push_pop_back_of_size_ne_zero := @eq_push_pop_back!_of_size_ne_zero
 
-@[deprecated set!_is_setIfInBounds (since := "2024-11-24")] abbrev set_is_setIfInBounds := @set!_is_setIfInBounds
-@[deprecated size_setIfInBounds (since := "2024-11-24")] abbrev size_setD := @size_setIfInBounds
-@[deprecated getElem_setIfInBounds_eq (since := "2024-11-24")] abbrev getElem_setD_eq := @getElem_setIfInBounds_eq
-@[deprecated getElem?_setIfInBounds_eq (since := "2024-11-24")] abbrev get?_setD_eq := @getElem?_setIfInBounds_eq
-@[deprecated getD_get?_setIfInBounds (since := "2024-11-24")] abbrev getD_setD := @getD_get?_setIfInBounds
-@[deprecated getElem_setIfInBounds (since := "2024-11-24")] abbrev getElem_setD := @getElem_setIfInBounds
-
 end Array

src/Init/Data/Array/Set.lean

@@ -25,11 +25,9 @@ Set an element in an array, or do nothing if the index is out of bounds.
 This will perform the update destructively provided that `a` has a reference
 count of 1 when called.
 -/
-@[inline] def Array.setIfInBounds (a : Array α) (i : Nat) (v : α) : Array α :=
+@[inline] def Array.setD (a : Array α) (i : Nat) (v : α) : Array α :=
   dite (LT.lt i a.size) (fun h => a.set i v h) (fun _ => a)
 
-@[deprecated Array.setIfInBounds (since := "2024-11-24")] abbrev Array.setD := @Array.setIfInBounds
-
 /--
 Set an element in an array, or panic if the index is out of bounds.
 
@@ -38,4 +36,4 @@ count of 1 when called.
 -/
 @[extern "lean_array_set"]
 def Array.set! (a : Array α) (i : @& Nat) (v : α) : Array α :=
-  Array.setIfInBounds a i v
+  Array.setD a i v

src/Init/Data/BitVec/Bitblast.lean

@@ -346,10 +346,6 @@ theorem getMsbD_sub {i : Nat} {i_lt : i < w} {x y : BitVec w} :
   · rfl
   · omega
 
-theorem getElem_sub {i : Nat} {x y : BitVec w} (h : i < w) :
-    (x - y)[i] = (x[i] ^^ ((~~~y + 1#w)[i] ^^ carry i x (~~~y + 1#w) false)) := by
-  simp [← getLsbD_eq_getElem, getLsbD_sub, h]
-
 theorem msb_sub {x y: BitVec w} :
     (x - y).msb
       = (x.msb ^^ ((~~~y + 1#w).msb ^^ carry (w - 1 - 0) x (~~~y + 1#w) false)) := by
@@ -414,10 +410,6 @@ theorem getLsbD_neg {i : Nat} {x : BitVec w} :
   · have h_ge : w ≤ i := by omega
     simp [getLsbD_ge _ _ h_ge, h_ge, hi]
 
-theorem getElem_neg {i : Nat} {x : BitVec w} (h : i < w) :
-    (-x)[i] = (x[i] ^^ decide (∃ j < i, x.getLsbD j = true)) := by
-  simp [← getLsbD_eq_getElem, getLsbD_neg, h]
-
 theorem getMsbD_neg {i : Nat} {x : BitVec w} :
     getMsbD (-x) i =
       (getMsbD x i ^^ decide (∃ j < w, i < j ∧ getMsbD x j = true)) := by

src/Init/Data/BitVec/Lemmas.lean

@@ -269,10 +269,6 @@ theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b'
   getLsbD (x#'lt) i = x.testBit i := by
   simp [getLsbD, BitVec.ofNatLt]
 
-@[simp] theorem getMsbD_ofNatLt {n x i : Nat} (h : x < 2^n) :
-    getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i)) := by
-  simp [getMsbD, getLsbD]
-
 @[simp, bv_toNat] theorem toNat_ofNat (x w : Nat) : (BitVec.ofNat w x).toNat = x % 2^w := by
   simp [BitVec.toNat, BitVec.ofNat, Fin.ofNat']
 
@@ -759,10 +755,6 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
 @[simp] theorem getLsbD_allOnes : (allOnes v).getLsbD i = decide (i < v) := by
   simp [allOnes]
 
-@[simp] theorem getMsbD_allOnes : (allOnes v).getMsbD i = decide (i < v) := by
-  simp [allOnes]
-  omega
-
 @[simp] theorem getElem_allOnes (i : Nat) (h : i < v) : (allOnes v)[i] = true := by
   simp [getElem_eq_testBit_toNat, h]
 
@@ -780,12 +772,6 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
 @[simp] theorem toNat_or (x y : BitVec v) :
     BitVec.toNat (x ||| y) = BitVec.toNat x ||| BitVec.toNat y := rfl
 
-@[simp] theorem toInt_or (x y : BitVec w) :
-    BitVec.toInt (x ||| y) = Int.bmod (BitVec.toNat x ||| BitVec.toNat y) (2^w) := by
-  rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_or, Nat.mod_eq_of_lt
-    (Nat.or_lt_two_pow (BitVec.isLt x) (BitVec.isLt y))]
-  omega
-
 @[simp] theorem toFin_or (x y : BitVec v) :
     BitVec.toFin (x ||| y) = BitVec.toFin x ||| BitVec.toFin y := by
   apply Fin.eq_of_val_eq
@@ -853,12 +839,6 @@ instance : Std.LawfulCommIdentity (α := BitVec n) (· ||| · ) (0#n) where
 @[simp] theorem toNat_and (x y : BitVec v) :
     BitVec.toNat (x &&& y) = BitVec.toNat x &&& BitVec.toNat y := rfl
 
-@[simp] theorem toInt_and (x y : BitVec w) :
-    BitVec.toInt (x &&& y) = Int.bmod (BitVec.toNat x &&& BitVec.toNat y) (2^w) := by
-  rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_and, Nat.mod_eq_of_lt
-    (Nat.and_lt_two_pow x.toNat (BitVec.isLt y))]
-  omega
-
 @[simp] theorem toFin_and (x y : BitVec v) :
     BitVec.toFin (x &&& y) = BitVec.toFin x &&& BitVec.toFin y := by
   apply Fin.eq_of_val_eq
@@ -926,12 +906,6 @@ instance : Std.LawfulCommIdentity (α := BitVec n) (· &&& · ) (allOnes n) wher
 @[simp] theorem toNat_xor (x y : BitVec v) :
     BitVec.toNat (x ^^^ y) = BitVec.toNat x ^^^ BitVec.toNat y := rfl
 
-@[simp] theorem toInt_xor (x y : BitVec w) :
-    BitVec.toInt (x ^^^ y) = Int.bmod (BitVec.toNat x ^^^ BitVec.toNat y) (2^w) := by
-  rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_xor, Nat.mod_eq_of_lt
-    (Nat.xor_lt_two_pow (BitVec.isLt x) (BitVec.isLt y))]
-  omega
-
 @[simp] theorem toFin_xor (x y : BitVec v) :
     BitVec.toFin (x ^^^ y) = BitVec.toFin x ^^^ BitVec.toFin y := by
   apply Fin.eq_of_val_eq
@@ -1009,13 +983,6 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
           _ ≤ 2 ^ i := Nat.pow_le_pow_of_le_right Nat.zero_lt_two w
       · simp
 
-@[simp] theorem toInt_not {x : BitVec w} :
-    (~~~x).toInt = Int.bmod (2^w - 1 - x.toNat) (2^w) := by
-  rw_mod_cast [BitVec.toInt, BitVec.toNat_not, Int.bmod_def]
-  simp [show ((2^w : Nat) : Int) - 1 - x.toNat = ((2^w - 1 - x.toNat) : Nat) by omega]
-  rw_mod_cast [Nat.mod_eq_of_lt (by omega)]
-  omega
-
 @[simp] theorem ofInt_negSucc_eq_not_ofNat {w n : Nat} :
     BitVec.ofInt w (Int.negSucc n) = ~~~.ofNat w n := by
   simp only [BitVec.ofInt, Int.toNat, Int.ofNat_eq_coe, toNat_eq, toNat_ofNatLt, toNat_not,
@@ -1040,10 +1007,6 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
 @[simp] theorem getLsbD_not {x : BitVec v} : (~~~x).getLsbD i = (decide (i < v) && ! x.getLsbD i) := by
   by_cases h' : i < v <;> simp_all [not_def]
 
-@[simp] theorem getMsbD_not {x : BitVec v} :
-    (~~~x).getMsbD i = (decide (i < v) && ! x.getMsbD i) := by
-  by_cases h' : i < v <;> simp_all [not_def]
-
 @[simp] theorem getElem_not {x : BitVec w} {i : Nat} (h : i < w) : (~~~x)[i] = !x[i] := by
   simp only [getElem_eq_testBit_toNat, toNat_not]
   rw [← Nat.sub_add_eq, Nat.add_comm 1]
@@ -1517,12 +1480,6 @@ theorem getLsbD_sshiftRight' {x y: BitVec w} {i : Nat} :
       (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by
   simp only [BitVec.sshiftRight', BitVec.getLsbD_sshiftRight]
 
-@[simp]
-theorem getElem_sshiftRight' {x y : BitVec w} {i : Nat} (h : i < w) :
-    (x.sshiftRight' y)[i] =
-      (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by
-  simp only [← getLsbD_eq_getElem, BitVec.sshiftRight', BitVec.getLsbD_sshiftRight]
-
 @[simp]
 theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} :
     (x.sshiftRight y.toNat).getMsbD i = (decide (i < w) && if i < y.toNat then x.msb else x.getMsbD (i - y.toNat)) := by
@@ -3267,11 +3224,7 @@ theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat els
   · simp [h]
 
 theorem getLsbD_abs {i : Nat} {x : BitVec w} :
-    getLsbD x.abs i = if x.msb then getLsbD (-x) i else getLsbD x i := by
-  by_cases h : x.msb <;> simp [BitVec.abs, h]
-
-theorem getElem_abs {i : Nat} {x : BitVec w} (h : i < w) :
-    x.abs[i] = if x.msb then (-x)[i] else x[i] := by
+   getLsbD x.abs i = if x.msb then getLsbD (-x) i else getLsbD x i := by
   by_cases h : x.msb <;> simp [BitVec.abs, h]
 
 theorem getMsbD_abs {i : Nat} {x : BitVec w} :

src/Init/Data/Nat.lean

@@ -20,4 +20,3 @@ import Init.Data.Nat.Mod
 import Init.Data.Nat.Lcm
 import Init.Data.Nat.Compare
 import Init.Data.Nat.Simproc
-import Init.Data.Nat.Fold

src/Init/Data/Nat/Basic.lean

@@ -35,6 +35,52 @@ Used as the default `Nat` eliminator by the `cases` tactic. -/
 protected abbrev casesAuxOn {motive : Nat → Sort u} (t : Nat) (zero : motive 0) (succ : (n : Nat) → motive (n + 1)) : motive t :=
   Nat.casesOn t zero succ
 
+/--
+`Nat.fold` evaluates `f` on the numbers up to `n` exclusive, in increasing order:
+* `Nat.fold f 3 init = init |> f 0 |> f 1 |> f 2`
+-/
+@[specialize] def fold {α : Type u} (f : Nat → α → α) : (n : Nat) → (init : α) → α
+  | 0,      a => a
+  | succ n, a => f n (fold f n a)
+
+/-- Tail-recursive version of `Nat.fold`. -/
+@[inline] def foldTR {α : Type u} (f : Nat → α → α) (n : Nat) (init : α) : α :=
+  let rec @[specialize] loop
+    | 0,      a => a
+    | succ m, a => loop m (f (n - succ m) a)
+  loop n init
+
+/--
+`Nat.foldRev` evaluates `f` on the numbers up to `n` exclusive, in decreasing order:
+* `Nat.foldRev f 3 init = f 0 <| f 1 <| f 2 <| init`
+-/
+@[specialize] def foldRev {α : Type u} (f : Nat → α → α) : (n : Nat) → (init : α) → α
+  | 0,      a => a
+  | succ n, a => foldRev f n (f n a)
+
+/-- `any f n = true` iff there is `i in [0, n-1]` s.t. `f i = true` -/
+@[specialize] def any (f : Nat → Bool) : Nat → Bool
+  | 0      => false
+  | succ n => any f n || f n
+
+/-- Tail-recursive version of `Nat.any`. -/
+@[inline] def anyTR (f : Nat → Bool) (n : Nat) : Bool :=
+  let rec @[specialize] loop : Nat → Bool
+    | 0      => false
+    | succ m => f (n - succ m) || loop m
+  loop n
+
+/-- `all f n = true` iff every `i in [0, n-1]` satisfies `f i = true` -/
+@[specialize] def all (f : Nat → Bool) : Nat → Bool
+  | 0      => true
+  | succ n => all f n && f n
+
+/-- Tail-recursive version of `Nat.all`. -/
+@[inline] def allTR (f : Nat → Bool) (n : Nat) : Bool :=
+  let rec @[specialize] loop : Nat → Bool
+    | 0      => true
+    | succ m => f (n - succ m) && loop m
+  loop n
 
 /--
 `Nat.repeat f n a` is `f^(n) a`; that is, it iterates `f` `n` times on `a`.
@@ -1112,6 +1158,33 @@ theorem not_lt_eq (a b : Nat) : (¬ (a < b)) = (b ≤ a) :=
 theorem not_gt_eq (a b : Nat) : (¬ (a > b)) = (a ≤ b) :=
   not_lt_eq b a
 
+/-! # csimp theorems -/
+
+@[csimp] theorem fold_eq_foldTR : @fold = @foldTR :=
+  funext fun α => funext fun f => funext fun n => funext fun init =>
+  let rec go : ∀ m n, foldTR.loop f (m + n) m (fold f n init) = fold f (m + n) init
+    | 0,      n => by simp [foldTR.loop]
+    | succ m, n => by rw [foldTR.loop, add_sub_self_left, succ_add]; exact go m (succ n)
+  (go n 0).symm
+
+@[csimp] theorem any_eq_anyTR : @any = @anyTR :=
+  funext fun f => funext fun n =>
+  let rec go : ∀ m n,  (any f n || anyTR.loop f (m + n) m) = any f (m + n)
+    | 0,      n => by simp [anyTR.loop]
+    | succ m, n => by
+      rw [anyTR.loop, add_sub_self_left, ← Bool.or_assoc, succ_add]
+      exact go m (succ n)
+  (go n 0).symm
+
+@[csimp] theorem all_eq_allTR : @all = @allTR :=
+  funext fun f => funext fun n =>
+  let rec go : ∀ m n,  (all f n && allTR.loop f (m + n) m) = all f (m + n)
+    | 0,      n => by simp [allTR.loop]
+    | succ m, n => by
+      rw [allTR.loop, add_sub_self_left, ← Bool.and_assoc, succ_add]
+      exact go m (succ n)
+  (go n 0).symm
+
 @[csimp] theorem repeat_eq_repeatTR : @repeat = @repeatTR :=
   funext fun α => funext fun f => funext fun n => funext fun init =>
   let rec go : ∀ m n, repeatTR.loop f m (repeat f n init) = repeat f (m + n) init
@@ -1120,3 +1193,31 @@ theorem not_gt_eq (a b : Nat) : (¬ (a > b)) = (a ≤ b) :=
   (go n 0).symm
 
 end Nat
+
+namespace Prod
+
+/--
+`(start, stop).foldI f a` evaluates `f` on all the numbers
+from `start` (inclusive) to `stop` (exclusive) in increasing order:
+* `(5, 8).foldI f init = init |> f 5 |> f 6 |> f 7`
+-/
+@[inline] def foldI {α : Type u} (f : Nat → α → α) (i : Nat × Nat) (a : α) : α :=
+  Nat.foldTR.loop f i.2 (i.2 - i.1) a
+
+/--
+`(start, stop).anyI f a` returns true if `f` is true for some natural number
+from `start` (inclusive) to `stop` (exclusive):
+* `(5, 8).anyI f = f 5 || f 6 || f 7`
+-/
+@[inline] def anyI (f : Nat → Bool) (i : Nat × Nat) : Bool :=
+  Nat.anyTR.loop f i.2 (i.2 - i.1)
+
+/--
+`(start, stop).allI f a` returns true if `f` is true for all natural numbers
+from `start` (inclusive) to `stop` (exclusive):
+* `(5, 8).anyI f = f 5 && f 6 && f 7`
+-/
+@[inline] def allI (f : Nat → Bool) (i : Nat × Nat) : Bool :=
+  Nat.allTR.loop f i.2 (i.2 - i.1)
+
+end Prod

src/Init/Data/Nat/Control.lean

@@ -6,51 +6,50 @@ Author: Leonardo de Moura
 prelude
 import Init.Control.Basic
 import Init.Data.Nat.Basic
-import Init.Omega
 
 namespace Nat
 universe u v
 
-@[inline] def forM {m} [Monad m] (n : Nat) (f : (i : Nat) → i < n → m Unit) : m Unit :=
-  let rec @[specialize] loop : ∀ i, i ≤ n → m Unit
-    | 0,   _ => pure ()
-    | i+1, h => do f (n-i-1) (by omega); loop i (Nat.le_of_succ_le h)
-  loop n (by simp)
+@[inline] def forM {m} [Monad m] (n : Nat) (f : Nat → m Unit) : m Unit :=
+  let rec @[specialize] loop
+    | 0   => pure ()
+    | i+1 => do f (n-i-1); loop i
+  loop n
 
-@[inline] def forRevM {m} [Monad m] (n : Nat) (f : (i : Nat) → i < n → m Unit) : m Unit :=
-  let rec @[specialize] loop : ∀ i, i ≤ n → m Unit
-    | 0,   _ => pure ()
-    | i+1, h => do f i (by omega); loop i (Nat.le_of_succ_le h)
-  loop n (by simp)
+@[inline] def forRevM {m} [Monad m] (n : Nat) (f : Nat → m Unit) : m Unit :=
+  let rec @[specialize] loop
+    | 0   => pure ()
+    | i+1 => do f i; loop i
+  loop n
 
-@[inline] def foldM {α : Type u} {m : Type u → Type v} [Monad m] (n : Nat) (f : (i : Nat) → i < n → α → m α) (init : α) : m α :=
-  let rec @[specialize] loop : ∀ i, i ≤ n → α → m α
-    | 0,   h, a => pure a
-    | i+1, h, a => f (n-i-1) (by omega) a >>= loop i (Nat.le_of_succ_le h)
-  loop n (by omega) init
+@[inline] def foldM {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (init : α) (n : Nat) : m α :=
+  let rec @[specialize] loop
+    | 0,   a => pure a
+    | i+1, a => f (n-i-1) a >>= loop i
+  loop n init
 
-@[inline] def foldRevM {α : Type u} {m : Type u → Type v} [Monad m] (n : Nat) (f : (i : Nat) → i < n → α → m α) (init : α) : m α :=
-  let rec @[specialize] loop : ∀ i, i ≤ n → α → m α
-    | 0,   h, a => pure a
-    | i+1, h, a => f i (by omega) a >>= loop i (Nat.le_of_succ_le h)
-  loop n (by omega) init
+@[inline] def foldRevM {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (init : α) (n : Nat) : m α :=
+  let rec @[specialize] loop
+    | 0,   a => pure a
+    | i+1, a => f i a >>= loop i
+  loop n init
 
-@[inline] def allM {m} [Monad m] (n : Nat) (p : (i : Nat) → i < n → m Bool) : m Bool :=
-  let rec @[specialize] loop : ∀ i, i ≤ n → m Bool
-    | 0,   _ => pure true
-    | i+1 , h => do
-      match (← p (n-i-1) (by omega)) with
-      | true  => loop i (by omega)
+@[inline] def allM {m} [Monad m] (n : Nat) (p : Nat → m Bool) : m Bool :=
+  let rec @[specialize] loop
+    | 0   => pure true
+    | i+1 => do
+      match (← p (n-i-1)) with
+      | true  => loop i
       | false => pure false
-  loop n (by simp)
+  loop n
 
-@[inline] def anyM {m} [Monad m] (n : Nat) (p : (i : Nat) → i < n → m Bool) : m Bool :=
-  let rec @[specialize] loop : ∀ i, i ≤ n → m Bool
-    | 0,   _ => pure false
-    | i+1, h => do
-      match (← p (n-i-1) (by omega)) with
+@[inline] def anyM {m} [Monad m] (n : Nat) (p : Nat → m Bool) : m Bool :=
+  let rec @[specialize] loop
+    | 0   => pure false
+    | i+1 => do
+      match (← p (n-i-1)) with
       | true  => pure true
-      | false => loop i (Nat.le_of_succ_le h)
-  loop n (by simp)
+      | false => loop i
+  loop n
 
 end Nat

src/Init/Data/Nat/Fold.lean

@@ -1,168 +0,0 @@
-/-
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn, Leonardo de Moura, Kim Morrison
--/
-prelude
-import Init.Omega
-
-set_option linter.missingDocs true -- keep it documented
-universe u
-
-namespace Nat
-
-/--
-`Nat.fold` evaluates `f` on the numbers up to `n` exclusive, in increasing order:
-* `Nat.fold f 3 init = init |> f 0 |> f 1 |> f 2`
--/
-@[specialize] def fold {α : Type u} : (n : Nat) → (f : (i : Nat) → i < n → α → α) → (init : α) → α
-  | 0,      f, a => a
-  | succ n, f, a => f n (by omega) (fold n (fun i h => f i (by omega)) a)
-
-/-- Tail-recursive version of `Nat.fold`. -/
-@[inline] def foldTR {α : Type u} (n : Nat) (f : (i : Nat) → i < n → α → α) (init : α) : α :=
-  let rec @[specialize] loop : ∀ j, j ≤ n → α → α
-    | 0,      h, a => a
-    | succ m, h, a => loop m (by omega) (f (n - succ m) (by omega) a)
-  loop n (by omega) init
-
-/--
-`Nat.foldRev` evaluates `f` on the numbers up to `n` exclusive, in decreasing order:
-* `Nat.foldRev f 3 init = f 0 <| f 1 <| f 2 <| init`
--/
-@[specialize] def foldRev {α : Type u} : (n : Nat) → (f : (i : Nat) → i < n → α → α) → (init : α) → α
-  | 0,      f, a => a
-  | succ n, f, a => foldRev n (fun i h => f i (by omega)) (f n (by omega) a)
-
-/-- `any f n = true` iff there is `i in [0, n-1]` s.t. `f i = true` -/
-@[specialize] def any : (n : Nat) → (f : (i : Nat) → i < n → Bool) → Bool
-  | 0,      f => false
-  | succ n, f => any n (fun i h => f i (by omega)) || f n (by omega)
-
-/-- Tail-recursive version of `Nat.any`. -/
-@[inline] def anyTR (n : Nat) (f : (i : Nat) → i < n → Bool) : Bool :=
-  let rec @[specialize] loop : (i : Nat) → i ≤ n → Bool
-    | 0,      h => false
-    | succ m, h => f (n - succ m) (by omega) || loop m (by omega)
-  loop n (by omega)
-
-/-- `all f n = true` iff every `i in [0, n-1]` satisfies `f i = true` -/
-@[specialize] def all : (n : Nat) → (f : (i : Nat) → i < n → Bool) → Bool
-  | 0,      f => true
-  | succ n, f => all n (fun i h => f i (by omega)) && f n (by omega)
-
-/-- Tail-recursive version of `Nat.all`. -/
-@[inline] def allTR (n : Nat) (f : (i : Nat) → i < n → Bool) : Bool :=
-  let rec @[specialize] loop : (i : Nat) → i ≤ n   → Bool
-    | 0,      h => true
-    | succ m, h => f (n - succ m) (by omega) && loop m (by omega)
-  loop n (by omega)
-
-/-! # csimp theorems -/
-
-theorem fold_congr {α : Type u} {n m : Nat} (w : n = m)
-     (f : (i : Nat) → i < n → α → α) (init : α) :
-     fold n f init = fold m (fun i h => f i (by omega)) init := by
-  subst m
-  rfl
-
-theorem foldTR_loop_congr {α : Type u} {n m : Nat} (w : n = m)
-     (f : (i : Nat) → i < n → α → α) (j : Nat) (h : j ≤ n) (init : α) :
-     foldTR.loop n f j h init = foldTR.loop m (fun i h => f i (by omega)) j (by omega) init := by
-  subst m
-  rfl
-
-@[csimp] theorem fold_eq_foldTR : @fold = @foldTR :=
-  funext fun α => funext fun n => funext fun f => funext fun init =>
-  let rec go : ∀ m n f, fold (m + n) f init = foldTR.loop (m + n) f m (by omega) (fold n (fun i h => f i (by omega)) init)
-    | 0,      n, f => by
-      simp only [foldTR.loop]
-      have t : 0 + n = n := by omega
-      rw [fold_congr t]
-    | succ m, n, f => by
-      have t : (m + 1) + n = m + (n + 1) := by omega
-      rw [foldTR.loop]
-      simp only [succ_eq_add_one, Nat.add_sub_cancel]
-      rw [fold_congr t, foldTR_loop_congr t, go, fold]
-      congr
-      omega
-  go n 0 f
-
-theorem any_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bool) : any n f = any m (fun i h => f i (by omega)) := by
-  subst m
-  rfl
-
-theorem anyTR_loop_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bool) (j : Nat) (h : j ≤ n) :
-    anyTR.loop n f j h = anyTR.loop m (fun i h => f i (by omega)) j (by omega) := by
-  subst m
-  rfl
-
-@[csimp] theorem any_eq_anyTR : @any = @anyTR :=
-  funext fun n => funext fun f =>
-  let rec go : ∀ m n f, any (m + n) f = (any n (fun i h => f i (by omega)) || anyTR.loop (m + n) f m (by omega))
-    | 0,      n, f => by
-      simp [anyTR.loop]
-      have t : 0 + n = n := by omega
-      rw [any_congr t]
-    | succ m, n, f => by
-      have t : (m + 1) + n = m + (n + 1) := by omega
-      rw [anyTR.loop]
-      simp only [succ_eq_add_one]
-      rw [any_congr t, anyTR_loop_congr t, go, any, Bool.or_assoc]
-      congr
-      omega
-  go n 0 f
-
-theorem all_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bool) : all n f = all m (fun i h => f i (by omega)) := by
-  subst m
-  rfl
-
-theorem allTR_loop_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bool) (j : Nat) (h : j ≤ n) : allTR.loop n f j h = allTR.loop m (fun i h => f i (by omega)) j (by omega) := by
-  subst m
-  rfl
-
-@[csimp] theorem all_eq_allTR : @all = @allTR :=
-  funext fun n => funext fun f =>
-  let rec go : ∀ m n f, all (m + n) f = (all n (fun i h => f i (by omega)) && allTR.loop (m + n) f m (by omega))
-    | 0,      n, f => by
-      simp [allTR.loop]
-      have t : 0 + n = n := by omega
-      rw [all_congr t]
-    | succ m, n, f => by
-      have t : (m + 1) + n = m + (n + 1) := by omega
-      rw [allTR.loop]
-      simp only [succ_eq_add_one]
-      rw [all_congr t, allTR_loop_congr t, go, all, Bool.and_assoc]
-      congr
-      omega
-  go n 0 f
-
-end Nat
-
-namespace Prod
-
-/--
-`(start, stop).foldI f a` evaluates `f` on all the numbers
-from `start` (inclusive) to `stop` (exclusive) in increasing order:
-* `(5, 8).foldI f init = init |> f 5 |> f 6 |> f 7`
--/
-@[inline] def foldI {α : Type u} (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → α → α) (a : α) : α :=
-  (i.2 - i.1).fold (fun j _ => f (i.1 + j) (by omega) (by omega)) a
-
-/--
-`(start, stop).anyI f a` returns true if `f` is true for some natural number
-from `start` (inclusive) to `stop` (exclusive):
-* `(5, 8).anyI f = f 5 || f 6 || f 7`
--/
-@[inline] def anyI (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → Bool) : Bool :=
-  (i.2 - i.1).any (fun j _ => f (i.1 + j) (by omega) (by omega))
-
-/--
-`(start, stop).allI f a` returns true if `f` is true for all natural numbers
-from `start` (inclusive) to `stop` (exclusive):
-* `(5, 8).anyI f = f 5 && f 6 && f 7`
--/
-@[inline] def allI (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → Bool) : Bool :=
-  (i.2 - i.1).all (fun j _ => f (i.1 + j) (by omega) (by omega))
-
-end Prod

src/Init/Data/Sum/Basic.lean

@@ -31,7 +31,7 @@ This file defines basic operations on the the sum type `α ⊕ β`.
 
 ## Further material
 
-See `Init.Data.Sum.Lemmas` for theorems about these definitions.
+See `Batteries.Data.Sum.Lemmas` for theorems about these definitions.
 
 ## Notes
 

src/Init/Notation.lean

@@ -71,9 +71,9 @@ def prio : Category := {}
 
 /-- `prec` is a builtin syntax category for precedences. A precedence is a value
 that expresses how tightly a piece of syntax binds: for example `1 + 2 * 3` is
-parsed as `1 + (2 * 3)` because `*` has a higher precedence than `+`.
+parsed as `1 + (2 * 3)` because `*` has a higher pr0ecedence than `+`.
 Higher numbers denote higher precedence.
-In addition to literals like `37`, there are some special named precedence levels:
+In addition to literals like `37`, there are some special named priorities:
 * `arg` for the precedence of function arguments
 * `max` for the highest precedence used in term parsers (not actually the maximum possible value)
 * `lead` for the precedence of terms not supposed to be used as arguments

src/Init/Syntax.lean

@@ -30,7 +30,7 @@ Does nothing for non-`node` nodes, or if `i` is out of bounds of the node list.
 -/
 def setArg (stx : Syntax) (i : Nat) (arg : Syntax) : Syntax :=
   match stx with
-  | node info k args => node info k (args.setIfInBounds i arg)
+  | node info k args => node info k (args.setD i arg)
   | stx              => stx
 
 end Lean.Syntax

src/Init/System/IO.lean

@@ -462,16 +462,6 @@ Note that it is the caller's job to remove the file after use.
 -/
 @[extern "lean_io_create_tempfile"] opaque createTempFile : IO (Handle × FilePath)
 
-/--
-Creates a temporary directory in the most secure manner possible. There are no race conditions in the
-directory’s creation. The directory is readable and writable only by the creating user ID.
-
-Returns the new directory's path.
-
-It is the caller's job to remove the directory after use.
--/
-@[extern "lean_io_create_tempdir"] opaque createTempDir : IO FilePath
-
 end FS
 
 @[extern "lean_io_getenv"] opaque getEnv (var : @& String) : BaseIO (Option String)
@@ -484,6 +474,17 @@ namespace FS
 def withFile (fn : FilePath) (mode : Mode) (f : Handle → IO α) : IO α :=
   Handle.mk fn mode >>= f
 
+/--
+Like `createTempFile` but also takes care of removing the file after usage.
+-/
+def withTempFile [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : Handle → FilePath → m α) :
+    m α := do
+  let (handle, path) ← createTempFile
+  try
+    f handle path
+  finally
+    removeFile path
+
 def Handle.putStrLn (h : Handle) (s : String) : IO Unit :=
   h.putStr (s.push '\n')
 
@@ -674,10 +675,8 @@ def appDir : IO FilePath := do
     | throw <| IO.userError s!"System.IO.appDir: unexpected filename '{p}'"
   FS.realPath p
 
-namespace FS
-
 /-- Create given path and all missing parents as directories. -/
-partial def createDirAll (p : FilePath) : IO Unit := do
+partial def FS.createDirAll (p : FilePath) : IO Unit := do
   if ← p.isDir then
     return ()
   if let some parent := p.parent then
@@ -694,7 +693,7 @@ partial def createDirAll (p : FilePath) : IO Unit := do
 /--
   Fully remove given directory by deleting all contained files and directories in an unspecified order.
   Fails if any contained entry cannot be deleted or was newly created during execution. -/
-partial def removeDirAll (p : FilePath) : IO Unit := do
+partial def FS.removeDirAll (p : FilePath) : IO Unit := do
   for ent in (← p.readDir) do
     if (← ent.path.isDir : Bool) then
       removeDirAll ent.path
@@ -702,32 +701,6 @@ partial def removeDirAll (p : FilePath) : IO Unit := do
       removeFile ent.path
   removeDir p
 
-/--
-Like `createTempFile`, but also takes care of removing the file after usage.
--/
-def withTempFile [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : Handle → FilePath → m α) :
-    m α := do
-  let (handle, path) ← createTempFile
-  try
-    f handle path
-  finally
-    removeFile path
-
-/--
-Like `createTempDir`, but also takes care of removing the directory after usage.
-
-All files in the directory are recursively deleted, regardless of how or when they were created.
--/
-def withTempDir [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : FilePath → m α) :
-    m α := do
-  let path ← createTempDir
-  try
-    f path
-  finally
-    removeDirAll path
-
-end FS
-
 namespace Process
 
 /-- Returns the current working directory of the calling process. -/

src/Init/Tactics.lean

@@ -428,11 +428,11 @@ macro "infer_instance" : tactic => `(tactic| exact inferInstance)
 /--
 `+opt` is short for `(opt := true)`. It sets the `opt` configuration option to `true`.
 -/
-syntax posConfigItem := " +" noWs ident
+syntax posConfigItem := "+" noWs ident
 /--
 `-opt` is short for `(opt := false)`. It sets the `opt` configuration option to `false`.
 -/
-syntax negConfigItem := " -" noWs ident
+syntax negConfigItem := "-" noWs ident
 /--
 `(opt := val)` sets the `opt` configuration option to `val`.
 

src/Lean/Compiler/IR/Borrow.lean

@@ -205,8 +205,8 @@ def getParamInfo (k : ParamMap.Key) : M (Array Param) := do
 
 /-- For each ps[i], if ps[i] is owned, then mark xs[i] as owned. -/
 def ownArgsUsingParams (xs : Array Arg) (ps : Array Param) : M Unit :=
-  xs.size.forM fun i _ => do
-    let x := xs[i]
+  xs.size.forM fun i => do
+    let x := xs[i]!
     let p := ps[i]!
     unless p.borrow do ownArg x
 
@@ -216,8 +216,8 @@ def ownArgsUsingParams (xs : Array Arg) (ps : Array Param) : M Unit :=
    we would have to insert a `dec xs[i]` after `f xs` and consequently
    "break" the tail call. -/
 def ownParamsUsingArgs (xs : Array Arg) (ps : Array Param) : M Unit :=
-  xs.size.forM fun i _ => do
-    let x := xs[i]
+  xs.size.forM fun i => do
+    let x := xs[i]!
     let p := ps[i]!
     match x with
     | Arg.var x => if (← isOwned x) then ownVar p.x

src/Lean/Compiler/IR/Boxing.lean

@@ -48,9 +48,9 @@ def requiresBoxedVersion (env : Environment) (decl : Decl) : Bool :=
 def mkBoxedVersionAux (decl : Decl) : N Decl := do
   let ps := decl.params
   let qs ← ps.mapM fun _ => do let x ← N.mkFresh; pure { x := x, ty := IRType.object, borrow := false : Param }
-  let (newVDecls, xs) ← qs.size.foldM (init := (#[], #[])) fun i _ (newVDecls, xs) => do
+  let (newVDecls, xs) ← qs.size.foldM (init := (#[], #[])) fun i (newVDecls, xs) => do
     let p := ps[i]!
-    let q := qs[i]
+    let q := qs[i]!
     if !p.ty.isScalar then
       pure (newVDecls, xs.push (Arg.var q.x))
     else

src/Lean/Compiler/IR/ElimDeadBranches.lean

@@ -63,7 +63,7 @@ partial def merge (v₁ v₂ : Value) : Value :=
   | top, _ => top
   | _, top => top
   | v₁@(ctor i₁ vs₁), v₂@(ctor i₂ vs₂) =>
-    if i₁ == i₂ then ctor i₁ <| vs₁.size.fold (init := #[]) fun i _ r => r.push (merge vs₁[i] vs₂[i]!)
+    if i₁ == i₂ then ctor i₁ <| vs₁.size.fold (init := #[]) fun i r => r.push (merge vs₁[i]! vs₂[i]!)
     else choice [v₁, v₂]
   | choice vs₁, choice vs₂ => choice <| vs₁.foldl (addChoice merge) vs₂
   | choice vs, v => choice <| addChoice merge vs v
@@ -225,8 +225,8 @@ def updateCurrFnSummary (v : Value) : M Unit := do
 def updateJPParamsAssignment (ys : Array Param) (xs : Array Arg) : M Bool := do
   let ctx ← read
   let currFnIdx := ctx.currFnIdx
-  ys.size.foldM (init := false) fun i _ r => do
-    let y := ys[i]
+  ys.size.foldM (init := false) fun i r => do
+    let y := ys[i]!
     let x := xs[i]!
     let yVal ← findVarValue y.x
     let xVal ← findArgValue x
@@ -282,8 +282,8 @@ partial def interpFnBody : FnBody → M Unit
 def inferStep : M Bool := do
   let ctx ← read
   modify fun s => { s with assignments := ctx.decls.map fun _ => {} }
-  ctx.decls.size.foldM (init := false) fun idx _ modified => do
-    match ctx.decls[idx] with
+  ctx.decls.size.foldM (init := false) fun idx modified => do
+    match ctx.decls[idx]! with
     | .fdecl (xs := ys) (body := b) .. => do
       let s ← get
       let currVals := s.funVals[idx]!
@@ -336,8 +336,8 @@ def elimDeadBranches (decls : Array Decl) : CompilerM (Array Decl) := do
   let funVals := s.funVals
   let assignments := s.assignments
   modify fun s =>
-    let env := decls.size.fold (init := s.env) fun i _ env =>
-      addFunctionSummary env decls[i].name funVals[i]!
+    let env := decls.size.fold (init := s.env) fun i env =>
+      addFunctionSummary env decls[i]!.name funVals[i]!
     { s with env := env }
   return decls.mapIdx fun i decl => elimDead assignments[i]! decl
 

src/Lean/Compiler/IR/EmitC.lean

@@ -108,9 +108,9 @@ def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M U
     if ps.size > closureMaxArgs && isBoxedName decl.name then
       emit "lean_object**"
     else
-      ps.size.forM fun i _ => do
+      ps.size.forM fun i => do
         if i > 0 then emit ", "
-        emit (toCType ps[i].ty)
+        emit (toCType ps[i]!.ty)
     emit ")"
   emitLn ";"
 
@@ -321,22 +321,20 @@ def emitSSet (x : VarId) (n : Nat) (offset : Nat) (y : VarId) (t : IRType) : M U
 
 def emitJmp (j : JoinPointId) (xs : Array Arg) : M Unit := do
   let ps ← getJPParams j
-  if h : xs.size = ps.size then
-    xs.size.forM fun i _ => do
-      let p := ps[i]
-      let x := xs[i]
-      emit p.x; emit " = "; emitArg x; emitLn ";"
-    emit "goto "; emit j; emitLn ";"
-  else
-    do throw "invalid goto"
+  unless xs.size == ps.size do throw "invalid goto"
+  xs.size.forM fun i => do
+    let p := ps[i]!
+    let x := xs[i]!
+    emit p.x; emit " = "; emitArg x; emitLn ";"
+  emit "goto "; emit j; emitLn ";"
 
 def emitLhs (z : VarId) : M Unit := do
   emit z; emit " = "
 
 def emitArgs (ys : Array Arg) : M Unit :=
-  ys.size.forM fun i _ => do
+  ys.size.forM fun i => do
     if i > 0 then emit ", "
-    emitArg ys[i]
+    emitArg ys[i]!
 
 def emitCtorScalarSize (usize : Nat) (ssize : Nat) : M Unit := do
   if usize == 0 then emit ssize
@@ -348,8 +346,8 @@ def emitAllocCtor (c : CtorInfo) : M Unit := do
   emitCtorScalarSize c.usize c.ssize; emitLn ");"
 
 def emitCtorSetArgs (z : VarId) (ys : Array Arg) : M Unit :=
-  ys.size.forM fun i _ => do
-    emit "lean_ctor_set("; emit z; emit ", "; emit i; emit ", "; emitArg ys[i]; emitLn ");"
+  ys.size.forM fun i => do
+    emit "lean_ctor_set("; emit z; emit ", "; emit i; emit ", "; emitArg ys[i]!; emitLn ");"
 
 def emitCtor (z : VarId) (c : CtorInfo) (ys : Array Arg) : M Unit := do
   emitLhs z;
@@ -360,7 +358,7 @@ def emitCtor (z : VarId) (c : CtorInfo) (ys : Array Arg) : M Unit := do
 
 def emitReset (z : VarId) (n : Nat) (x : VarId) : M Unit := do
   emit "if (lean_is_exclusive("; emit x; emitLn ")) {";
-  n.forM fun i _ => do
+  n.forM fun i => do
     emit " lean_ctor_release("; emit x; emit ", "; emit i; emitLn ");"
   emit " "; emitLhs z; emit x; emitLn ";";
   emitLn "} else {";
@@ -401,12 +399,12 @@ def emitSimpleExternalCall (f : String) (ps : Array Param) (ys : Array Arg) : M
   emit f; emit "("
   -- We must remove irrelevant arguments to extern calls.
   discard <| ys.size.foldM
-    (fun i _ (first : Bool) =>
+    (fun i (first : Bool) =>
       if ps[i]!.ty.isIrrelevant then
         pure first
       else do
         unless first do emit ", "
-        emitArg ys[i]
+        emitArg ys[i]!
         pure false)
     true
   emitLn ");"
@@ -433,8 +431,8 @@ def emitPartialApp (z : VarId) (f : FunId) (ys : Array Arg) : M Unit := do
   let decl ← getDecl f
   let arity := decl.params.size;
   emitLhs z; emit "lean_alloc_closure((void*)("; emitCName f; emit "), "; emit arity; emit ", "; emit ys.size; emitLn ");";
-  ys.size.forM fun i _ => do
-    let y := ys[i]
+  ys.size.forM fun i => do
+    let y := ys[i]!
     emit "lean_closure_set("; emit z; emit ", "; emit i; emit ", "; emitArg y; emitLn ");"
 
 def emitApp (z : VarId) (f : VarId) (ys : Array Arg) : M Unit :=
@@ -546,36 +544,34 @@ That is, we have
 -/
 def overwriteParam (ps : Array Param) (ys : Array Arg) : Bool :=
   let n := ps.size;
-  n.any fun i _ =>
-    let p := ps[i]
-    (i+1, n).anyI fun j _ _ => paramEqArg p ys[j]!
+  n.any fun i =>
+    let p := ps[i]!
+    (i+1, n).anyI fun j => paramEqArg p ys[j]!
 
 def emitTailCall (v : Expr) : M Unit :=
   match v with
   | Expr.fap _ ys => do
     let ctx ← read
     let ps := ctx.mainParams
-    if h : ps.size = ys.size then
-      if overwriteParam ps ys then
-        emitLn "{"
-        ps.size.forM fun i _ => do
-          let p := ps[i]
-          let y := ys[i]
-          unless paramEqArg p y do
-            emit (toCType p.ty); emit " _tmp_"; emit i; emit " = "; emitArg y; emitLn ";"
-        ps.size.forM fun i _ => do
-          let p := ps[i]
-          let y := ys[i]
-          unless paramEqArg p y do emit p.x; emit " = _tmp_"; emit i; emitLn ";"
-        emitLn "}"
-      else
-        ys.size.forM fun i _ => do
-          let p := ps[i]
-          let y := ys[i]
-          unless paramEqArg p y do emit p.x; emit " = "; emitArg y; emitLn ";"
-      emitLn "goto _start;"
+    unless ps.size == ys.size do throw "invalid tail call"
+    if overwriteParam ps ys then
+      emitLn "{"
+      ps.size.forM fun i => do
+        let p := ps[i]!
+        let y := ys[i]!
+        unless paramEqArg p y do
+          emit (toCType p.ty); emit " _tmp_"; emit i; emit " = "; emitArg y; emitLn ";"
+      ps.size.forM fun i => do
+        let p := ps[i]!
+        let y := ys[i]!
+        unless paramEqArg p y do emit p.x; emit " = _tmp_"; emit i; emitLn ";"
+      emitLn "}"
     else
-      throw "invalid tail call"
+      ys.size.forM fun i => do
+        let p := ps[i]!
+        let y := ys[i]!
+        unless paramEqArg p y do emit p.x; emit " = "; emitArg y; emitLn ";"
+    emitLn "goto _start;"
   | _ => throw "bug at emitTailCall"
 
 mutual
@@ -658,16 +654,16 @@ def emitDeclAux (d : Decl) : M Unit := do
         if xs.size > closureMaxArgs && isBoxedName d.name then
           emit "lean_object** _args"
         else
-          xs.size.forM fun i _ => do
+          xs.size.forM fun i => do
             if i > 0 then emit ", "
-            let x := xs[i]
+            let x := xs[i]!
             emit (toCType x.ty); emit " "; emit x.x
         emit ")"
       else
         emit ("_init_" ++ baseName ++ "()")
       emitLn " {";
       if xs.size > closureMaxArgs && isBoxedName d.name then
-        xs.size.forM fun i _ => do
+        xs.size.forM fun i => do
           let x := xs[i]!
           emit "lean_object* "; emit x.x; emit " = _args["; emit i; emitLn "];"
       emitLn "_start:";

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -571,9 +571,9 @@ def emitAllocCtor (builder : LLVM.Builder llvmctx)
 
 def emitCtorSetArgs (builder : LLVM.Builder llvmctx)
     (z : VarId) (ys : Array Arg) : M llvmctx Unit := do
-  ys.size.forM fun i _ => do
+  ys.size.forM fun i => do
     let zv ← emitLhsVal builder z
-    let (_yty, yv) ← emitArgVal builder ys[i]
+    let (_yty, yv) ← emitArgVal builder ys[i]!
     let iv ← constIntUnsigned i
     callLeanCtorSet builder zv iv yv
     emitLhsSlotStore builder z zv
@@ -702,8 +702,8 @@ def emitPartialApp (builder : LLVM.Builder llvmctx) (z : VarId) (f : FunId) (ys
                                     (← constIntUnsigned arity)
                                     (← constIntUnsigned ys.size)
   LLVM.buildStore builder zval zslot
-  ys.size.forM fun i _ => do
-    let (yty, yslot) ← emitArgSlot_ builder ys[i]
+  ys.size.forM fun i => do
+    let (yty, yslot) ← emitArgSlot_ builder ys[i]!
     let yval ← LLVM.buildLoad2 builder yty yslot
     callLeanClosureSetFn builder zval (← constIntUnsigned i) yval
 
@@ -922,7 +922,7 @@ def emitReset (builder : LLVM.Builder llvmctx) (z : VarId) (n : Nat) (x : VarId)
   buildIfThenElse_ builder "isExclusive" isExclusive
    (fun builder => do
      let xv ← emitLhsVal builder x
-     n.forM fun i _ => do
+     n.forM fun i => do
          callLeanCtorRelease builder xv (← constIntUnsigned i)
      emitLhsSlotStore builder z xv
      return ShouldForwardControlFlow.yes

src/Lean/Compiler/IR/ExpandResetReuse.lean

@@ -134,15 +134,15 @@ abbrev M := ReaderT Context (StateM Nat)
   modifyGet fun n => ({ idx := n }, n + 1)
 
 def releaseUnreadFields (y : VarId) (mask : Mask) (b : FnBody) : M FnBody :=
-  mask.size.foldM (init := b) fun i _ b =>
-    match mask[i] with
+  mask.size.foldM (init := b) fun i b =>
+    match mask.get! i with
     | some _ => pure b -- code took ownership of this field
     | none   => do
       let fld ← mkFresh
       pure (FnBody.vdecl fld IRType.object (Expr.proj i y) (FnBody.dec fld 1 true false b))
 
 def setFields (y : VarId) (zs : Array Arg) (b : FnBody) : FnBody :=
-  zs.size.fold (init := b) fun i _ b => FnBody.set y i zs[i] b
+  zs.size.fold (init := b) fun i b => FnBody.set y i (zs.get! i) b
 
 /-- Given `set x[i] := y`, return true iff `y := proj[i] x` -/
 def isSelfSet (ctx : Context) (x : VarId) (i : Nat) (y : Arg) : Bool :=

src/Lean/Compiler/IR/RC.lean

@@ -79,13 +79,13 @@ private def addDecForAlt (ctx : Context) (caseLiveVars altLiveVars : LiveVarSet)
 /-- `isFirstOcc xs x i = true` if `xs[i]` is the first occurrence of `xs[i]` in `xs` -/
 private def isFirstOcc (xs : Array Arg) (i : Nat) : Bool :=
   let x := xs[i]!
-  i.all fun j _ => xs[j]! != x
+  i.all fun j => xs[j]! != x
 
 /-- Return true if `x` also occurs in `ys` in a position that is not consumed.
    That is, it is also passed as a borrow reference. -/
 private def isBorrowParamAux (x : VarId) (ys : Array Arg) (consumeParamPred : Nat → Bool) : Bool :=
-  ys.size.any fun i _ =>
-    let y := ys[i]
+  ys.size.any fun i =>
+    let y := ys[i]!
     match y with
     | Arg.irrelevant => false
     | Arg.var y      => x == y && !consumeParamPred i
@@ -99,15 +99,15 @@ Return `n`, the number of times `x` is consumed.
 - `consumeParamPred i = true` if parameter `i` is consumed.
 -/
 private def getNumConsumptions (x : VarId) (ys : Array Arg) (consumeParamPred : Nat → Bool) : Nat :=
-  ys.size.fold (init := 0) fun i _ n =>
-    let y := ys[i]
+  ys.size.fold (init := 0) fun i n =>
+    let y := ys[i]!
     match y with
     | Arg.irrelevant => n
     | Arg.var y      => if x == y && consumeParamPred i then n+1 else n
 
 private def addIncBeforeAux (ctx : Context) (xs : Array Arg) (consumeParamPred : Nat → Bool) (b : FnBody) (liveVarsAfter : LiveVarSet) : FnBody :=
-  xs.size.fold (init := b) fun i _ b =>
-    let x := xs[i]
+  xs.size.fold (init := b) fun i b =>
+    let x := xs[i]!
     match x with
     | Arg.irrelevant => b
     | Arg.var x =>
@@ -128,8 +128,8 @@ private def addIncBefore (ctx : Context) (xs : Array Arg) (ps : Array Param) (b
 
 /-- See `addIncBeforeAux`/`addIncBefore` for the procedure that inserts `inc` operations before an application.  -/
 private def addDecAfterFullApp (ctx : Context) (xs : Array Arg) (ps : Array Param) (b : FnBody) (bLiveVars : LiveVarSet) : FnBody :=
-xs.size.fold (init := b) fun i _ b =>
-  match xs[i] with
+xs.size.fold (init := b) fun i b =>
+  match xs[i]! with
   | Arg.irrelevant => b
   | Arg.var x      =>
     /- We must add a `dec` if `x` must be consumed, it is alive after the application,

src/Lean/Compiler/LCNF/ElimDeadBranches.lean

@@ -587,15 +587,15 @@ def Decl.elimDeadBranches (decls : Array Decl) : CompilerM (Array Decl) := do
     refer to the docstring of `Decl.safe`.
     -/
     if decls[i]!.safe then .bot else .top
-  let mut funVals := decls.size.fold (init := .empty) fun i _ p => p.push (initialVal i)
+  let mut funVals := decls.size.fold (init := .empty) fun i p => p.push (initialVal i)
   let ctx := { decls }
   let mut state := { assignments, funVals }
   (_, state) ← inferMain |>.run ctx |>.run state
   funVals := state.funVals
   assignments := state.assignments
   modifyEnv fun e =>
-    decls.size.fold (init := e) fun i _ env =>
-      addFunctionSummary env decls[i].name funVals[i]!
+    decls.size.fold (init := e) fun i env =>
+      addFunctionSummary env decls[i]!.name funVals[i]!
 
   decls.mapIdxM fun i decl => if decl.safe then elimDead assignments[i]! decl else return decl
 

src/Lean/Compiler/LCNF/InferType.lean

@@ -76,8 +76,8 @@ def getType (fvarId : FVarId) : InferTypeM Expr := do
 
 def mkForallFVars (xs : Array Expr) (type : Expr) : InferTypeM Expr :=
   let b := type.abstract xs
-  xs.size.foldRevM (init := b) fun i _ b => do
-    let x := xs[i]
+  xs.size.foldRevM (init := b) fun i b => do
+    let x := xs[i]!
     let n ← InferType.getBinderName x.fvarId!
     let ty ← InferType.getType x.fvarId!
     let ty := ty.abstractRange i xs;

src/Lean/CoreM.lean

@@ -11,7 +11,6 @@ import Lean.ResolveName
 import Lean.Elab.InfoTree.Types
 import Lean.MonadEnv
 import Lean.Elab.Exception
-import Lean.Language.Basic
 
 namespace Lean
 register_builtin_option diagnostics : Bool := {
@@ -73,13 +72,6 @@ structure State where
   messages        : MessageLog     := {}
   /-- Info tree. We have the info tree here because we want to update it while adding attributes. -/
   infoState       : Elab.InfoState := {}
-  /--
-  Snapshot trees of asynchronous subtasks. As these are untyped and reported only at the end of the
-  command's main elaboration thread, they are only useful for basic message log reporting; for
-  incremental reporting and reuse within a long-running elaboration thread, types rooted in
-  `CommandParsedSnapshot` need to be adjusted.
-  -/
-  snapshotTasks : Array (Language.SnapshotTask Language.SnapshotTree) := #[]
   deriving Nonempty
 
 /-- Context for the CoreM monad. -/
@@ -188,8 +180,7 @@ instance : Elab.MonadInfoTree CoreM where
   modifyInfoState f := modify fun s => { s with infoState := f s.infoState }
 
 @[inline] def modifyCache (f : Cache → Cache) : CoreM Unit :=
-  modify fun ⟨env, next, ngen, trace, cache, messages, infoState, snaps⟩ =>
-   ⟨env, next, ngen, trace, f cache, messages, infoState, snaps⟩
+  modify fun ⟨env, next, ngen, trace, cache, messages, infoState⟩ => ⟨env, next, ngen, trace, f cache, messages, infoState⟩
 
 @[inline] def modifyInstLevelTypeCache (f : InstantiateLevelCache → InstantiateLevelCache) : CoreM Unit :=
   modifyCache fun ⟨c₁, c₂⟩ => ⟨f c₁, c₂⟩
@@ -364,83 +355,13 @@ instance : MonadLog CoreM where
     if (← read).suppressElabErrors then
       -- discard elaboration errors, except for a few important and unlikely misleading ones, on
       -- parse error
-      unless msg.data.hasTag (· matches `Elab.synthPlaceholder | `Tactic.unsolvedGoals | `trace) do
+      unless msg.data.hasTag (· matches `Elab.synthPlaceholder | `Tactic.unsolvedGoals) do
         return
 
     let ctx ← read
     let msg := { msg with data := MessageData.withNamingContext { currNamespace := ctx.currNamespace, openDecls := ctx.openDecls } msg.data };
     modify fun s => { s with messages := s.messages.add msg }
 
-/--
-Includes a given task (such as from `wrapAsyncAsSnapshot`) in the overall snapshot tree for this
-command's elaboration, making its result available to reporting and the language server. The
-reporter will not know about this snapshot tree node until the main elaboration thread for this
-command has finished so this function is not useful for incremental reporting within a longer
-elaboration thread but only for tasks that outlive it such as background kernel checking or proof
-elaboration.
--/
-def logSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) : CoreM Unit :=
-  modify fun s => { s with snapshotTasks := s.snapshotTasks.push task }
-
-/-- Wraps the given action for use in `EIO.asTask` etc., discarding its final monadic state. -/
-def wrapAsync (act : Unit → CoreM α) : CoreM (EIO Exception α) := do
-  let st ← get
-  let ctx ← read
-  let heartbeats := (← IO.getNumHeartbeats) - ctx.initHeartbeats
-  return withCurrHeartbeats (do
-      -- include heartbeats since start of elaboration in new thread as well such that forking off
-      -- an action doesn't suddenly allow it to succeed from a lower heartbeat count
-      IO.addHeartbeats heartbeats.toUInt64
-      act () : CoreM _)
-    |>.run' ctx st
-
-/-- Option for capturing output to stderr during elaboration. -/
-register_builtin_option stderrAsMessages : Bool := {
-  defValue := true
-  group    := "server"
-  descr    := "(server) capture output to the Lean stderr channel (such as from `dbg_trace`) during elaboration of a command as a diagnostic message"
-}
-
-open Language in
-/--
-Wraps the given action for use in `BaseIO.asTask` etc., discarding its final state except for
-`logSnapshotTask` tasks, which are reported as part of the returned tree.
--/
-def wrapAsyncAsSnapshot (act : Unit → CoreM Unit) (desc : String := by exact decl_name%.toString) :
-    CoreM (BaseIO SnapshotTree) := do
-  let t ← wrapAsync fun _ => do
-    IO.FS.withIsolatedStreams (isolateStderr := stderrAsMessages.get (← getOptions)) do
-      let tid ← IO.getTID
-      -- reset trace state and message log so as not to report them twice
-      modify ({ · with messages := {}, traceState := { tid } })
-      try
-        withTraceNode `Elab.async (fun _ => return desc) do
-          act ()
-      catch e =>
-        logError e.toMessageData
-      finally
-        addTraceAsMessages
-      get
-  let ctx ← readThe Core.Context
-  return do
-    match (← t.toBaseIO) with
-    | .ok (output, st) =>
-      let mut msgs := st.messages
-      if !output.isEmpty then
-        msgs := msgs.add {
-          fileName := ctx.fileName
-          severity := MessageSeverity.information
-          pos      := ctx.fileMap.toPosition <| ctx.ref.getPos?.getD 0
-          data     := output
-        }
-      return .mk {
-        desc
-        diagnostics := (← Language.Snapshot.Diagnostics.ofMessageLog msgs)
-        traces := st.traceState
-      } st.snapshotTasks
-    -- interrupt or abort exception as `try catch` above should have caught any others
-    | .error _ => default
-
 end Core
 
 export Core (CoreM mkFreshUserName checkSystem withCurrHeartbeats)

src/Lean/Data/PersistentArray.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Data.Nat.Fold
 import Init.Data.Array.Basic
 import Init.NotationExtra
 import Init.Data.ToString.Macro
@@ -372,7 +371,7 @@ instance : ToString Stats := ⟨Stats.toString⟩
 end PersistentArray
 
 def mkPersistentArray {α : Type u} (n : Nat) (v : α) : PArray α :=
-  n.fold (init := PersistentArray.empty) fun _ _ p => p.push v
+  n.fold (init := PersistentArray.empty) fun _ p => p.push v
 
 @[inline] def mkPArray {α : Type u} (n : Nat) (v : α) : PArray α :=
   mkPersistentArray n v

src/Lean/Elab.lean

@@ -23,7 +23,6 @@ import Lean.Elab.Quotation
 import Lean.Elab.Syntax
 import Lean.Elab.Do
 import Lean.Elab.StructInst
-import Lean.Elab.MutualInductive
 import Lean.Elab.Inductive
 import Lean.Elab.Structure
 import Lean.Elab.Print

src/Lean/Elab/App.lean

@@ -807,8 +807,8 @@ def getElabElimExprInfo (elimExpr : Expr) : MetaM ElabElimInfo := do
     These are the primary set of major parameters.
     -/
     let initMotiveFVars : CollectFVars.State := motiveArgs.foldl (init := {}) collectFVars
-    let motiveFVars ← xs.size.foldRevM (init := initMotiveFVars) fun i _ s => do
-      let x := xs[i]
+    let motiveFVars ← xs.size.foldRevM (init := initMotiveFVars) fun i s => do
+      let x := xs[i]!
       if s.fvarSet.contains x.fvarId! then
         return collectFVars s (← inferType x)
       else

src/Lean/Elab/Command.lean

@@ -84,7 +84,6 @@ structure State where
   ngen           : NameGenerator := {}
   infoState      : InfoState := {}
   traceState     : TraceState := {}
-  snapshotTasks  : Array (Language.SnapshotTask Language.SnapshotTree) := #[]
   deriving Nonempty
 
 structure Context where
@@ -115,7 +114,8 @@ structure Context where
   -/
   suppressElabErrors : Bool := false
 
-abbrev CommandElabM := ReaderT Context $ StateRefT State $ EIO Exception
+abbrev CommandElabCoreM (ε) := ReaderT Context $ StateRefT State $ EIO ε
+abbrev CommandElabM := CommandElabCoreM Exception
 abbrev CommandElab  := Syntax → CommandElabM Unit
 structure Linter where
   run : Syntax → CommandElabM Unit
@@ -198,6 +198,36 @@ instance : AddErrorMessageContext CommandElabM where
     let msg ← addMacroStack msg ctx.macroStack
     return (ref, msg)
 
+def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity) : Message :=
+  let pos := ref.getPos?.getD ctx.cmdPos
+  let endPos := ref.getTailPos?.getD pos
+  mkMessageCore ctx.fileName ctx.fileMap msgData severity pos endPos
+
+private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog := Id.run do
+  if traceState.traces.isEmpty then return log
+  let mut traces : Std.HashMap (String.Pos × String.Pos) (Array MessageData) := ∅
+  for traceElem in traceState.traces do
+    let ref := replaceRef traceElem.ref ctx.ref
+    let pos := ref.getPos?.getD 0
+    let endPos := ref.getTailPos?.getD pos
+    traces := traces.insert (pos, endPos) <| traces.getD (pos, endPos) #[] |>.push traceElem.msg
+  let mut log := log
+  let traces' := traces.toArray.qsort fun ((a, _), _) ((b, _), _) => a < b
+  for ((pos, endPos), traceMsg) in traces' do
+    let data := .tagged `trace <| .joinSep traceMsg.toList "\n"
+    log := log.add <| mkMessageCore ctx.fileName ctx.fileMap data .information pos endPos
+  return log
+
+private def addTraceAsMessages : CommandElabM Unit := do
+  let ctx ← read
+  -- do not add trace messages if `trace.profiler.output` is set as it would be redundant and
+  -- pretty printing the trace messages is expensive
+  if trace.profiler.output.get? (← getOptions) |>.isNone then
+    modify fun s => { s with
+      messages          := addTraceAsMessagesCore ctx s.messages s.traceState
+      traceState.traces := {}
+    }
+
 private def runCore (x : CoreM α) : CommandElabM α := do
   let s ← get
   let ctx ← read
@@ -223,7 +253,6 @@ private def runCore (x : CoreM α) : CommandElabM α := do
     nextMacroScope := s.nextMacroScope
     infoState.enabled := s.infoState.enabled
     traceState := s.traceState
-    snapshotTasks := s.snapshotTasks
   }
   let (ea, coreS) ← liftM x
   modify fun s => { s with
@@ -232,7 +261,6 @@ private def runCore (x : CoreM α) : CommandElabM α := do
     ngen              := coreS.ngen
     infoState.trees   := s.infoState.trees.append coreS.infoState.trees
     traceState.traces := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }
-    snapshotTasks     := coreS.snapshotTasks
     messages          := s.messages ++ coreS.messages
   }
   return ea
@@ -240,6 +268,10 @@ private def runCore (x : CoreM α) : CommandElabM α := do
 def liftCoreM (x : CoreM α) : CommandElabM α := do
   MonadExcept.ofExcept (← runCore (observing x))
 
+private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : Message :=
+  let ref := getBetterRef ref ctx.macroStack
+  mkMessageAux ctx ref (toString err) MessageSeverity.error
+
 @[inline] def liftIO {α} (x : IO α) : CommandElabM α := do
   let ctx ← read
   IO.toEIO (fun (ex : IO.Error) => Exception.error ctx.ref ex.toString) x
@@ -262,8 +294,9 @@ instance : MonadLog CommandElabM where
   logMessage msg := do
     if (← read).suppressElabErrors then
       -- discard elaboration errors on parse error
-      unless msg.data.hasTag (· matches `trace) do
-        return
+      -- NOTE: unlike `CoreM`'s `logMessage`, we do not currently have any command-level errors that
+      -- we want to allowlist
+      return
     let currNamespace ← getCurrNamespace
     let openDecls ← getOpenDecls
     let msg := { msg with data := MessageData.withNamingContext { currNamespace := currNamespace, openDecls := openDecls } msg.data }
@@ -289,61 +322,6 @@ def runLinters (stx : Syntax) : CommandElabM Unit := do
             finally
               modify fun s => { savedState with messages := s.messages }
 
-/--
-Catches and logs exceptions occurring in `x`. Unlike `try catch` in `CommandElabM`, this function
-catches interrupt exceptions as well and thus is intended for use at the top level of elaboration.
-Interrupt and abort exceptions are caught but not logged.
--/
-@[inline] def withLoggingExceptions (x : CommandElabM Unit) : CommandElabM Unit := fun ctx ref =>
-  EIO.catchExceptions (withLogging x ctx ref) (fun _ => pure ())
-
-@[inherit_doc Core.wrapAsync]
-def wrapAsync (act : Unit → CommandElabM α) : CommandElabM (EIO Exception α) := do
-  return act () |>.run (← read) |>.run' (← get)
-
-open Language in
-@[inherit_doc Core.wrapAsyncAsSnapshot]
--- `CoreM` and `CommandElabM` are too different to meaningfully share this code
-def wrapAsyncAsSnapshot (act : Unit → CommandElabM Unit)
-    (desc : String := by exact decl_name%.toString) :
-    CommandElabM (BaseIO SnapshotTree) := do
-  let t ← wrapAsync fun _ => do
-    IO.FS.withIsolatedStreams (isolateStderr := Core.stderrAsMessages.get (← getOptions)) do
-      let tid ← IO.getTID
-      -- reset trace state and message log so as not to report them twice
-      modify ({ · with messages := {}, traceState := { tid } })
-      try
-        withTraceNode `Elab.async (fun _ => return desc) do
-          act ()
-      catch e =>
-        logError e.toMessageData
-      finally
-        addTraceAsMessages
-      get
-  let ctx ← read
-  return do
-    match (← t.toBaseIO) with
-    | .ok (output, st) =>
-      let mut msgs := st.messages
-      if !output.isEmpty then
-        msgs := msgs.add {
-          fileName := ctx.fileName
-          severity := MessageSeverity.information
-          pos      := ctx.fileMap.toPosition <| ctx.ref.getPos?.getD 0
-          data     := output
-        }
-      return .mk {
-        desc
-        diagnostics := (← Language.Snapshot.Diagnostics.ofMessageLog msgs)
-        traces := st.traceState
-      } st.snapshotTasks
-    -- interrupt or abort exception as `try catch` above should have caught any others
-    | .error _ => default
-
-@[inherit_doc Core.logSnapshotTask]
-def logSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) : CommandElabM Unit :=
-  modify fun s => { s with snapshotTasks := s.snapshotTasks.push task }
-
 protected def getCurrMacroScope : CommandElabM Nat  := do pure (← read).currMacroScope
 protected def getMainModule     : CommandElabM Name := do pure (← getEnv).mainModule
 
@@ -554,6 +532,12 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
     let mut msgs := (← get).messages
     for tree in (← getInfoTrees) do
       trace[Elab.info] (← tree.format)
+    if (← isTracingEnabledFor `Elab.snapshotTree) then
+      if let some snap := (← read).snap? then
+        -- We can assume that the root command snapshot is not involved in parallelism yet, so this
+        -- should be true iff the command supports incrementality
+        if (← IO.hasFinished snap.new.result) then
+          liftCoreM <| Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.trace
     modify fun st => { st with
       messages := initMsgs ++ msgs
       infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees }
@@ -684,6 +668,14 @@ def runTermElabM (elabFn : Array Expr → TermElabM α) : CommandElabM α := do
           Term.addAutoBoundImplicits' xs someType fun xs _ =>
             Term.withoutAutoBoundImplicit <| elabFn xs
 
+/--
+Catches and logs exceptions occurring in `x`. Unlike `try catch` in `CommandElabM`, this function
+catches interrupt exceptions as well and thus is intended for use at the top level of elaboration.
+Interrupt and abort exceptions are caught but not logged.
+-/
+@[inline] def withLoggingExceptions (x : CommandElabM Unit) : CommandElabCoreM Empty Unit := fun ctx ref =>
+  EIO.catchExceptions (withLogging x ctx ref) (fun _ => pure ())
+
 private def liftAttrM {α} (x : AttrM α) : CommandElabM α := do
   liftCoreM x
 

src/Lean/Elab/Declaration.lean

@@ -7,8 +7,9 @@ prelude
 import Lean.Util.CollectLevelParams
 import Lean.Elab.DeclUtil
 import Lean.Elab.DefView
+import Lean.Elab.Inductive
+import Lean.Elab.Structure
 import Lean.Elab.MutualDef
-import Lean.Elab.MutualInductive
 import Lean.Elab.DeclarationRange
 namespace Lean.Elab.Command
 
@@ -162,11 +163,15 @@ def elabDeclaration : CommandElab := fun stx => do
     if declKind == ``Lean.Parser.Command.«axiom» then
       let modifiers ← elabModifiers modifiers
       elabAxiom modifiers decl
-    else if declKind == ``Lean.Parser.Command.«inductive»
-        || declKind == ``Lean.Parser.Command.classInductive
-        || declKind == ``Lean.Parser.Command.«structure» then
+    else if declKind == ``Lean.Parser.Command.«inductive» then
       let modifiers ← elabModifiers modifiers
       elabInductive modifiers decl
+    else if declKind == ``Lean.Parser.Command.classInductive then
+      let modifiers ← elabModifiers modifiers
+      elabClassInductive modifiers decl
+    else if declKind == ``Lean.Parser.Command.«structure» then
+      let modifiers ← elabModifiers modifiers
+      elabStructure modifiers decl
     else
       throwError "unexpected declaration"
 
@@ -273,10 +278,10 @@ def elabMutual : CommandElab := fun stx => do
     -- only case implementing incrementality currently
     elabMutualDef stx[1].getArgs
   else withoutCommandIncrementality true do
-    if ← isMutualInductive stx then
+    if isMutualInductive stx then
       elabMutualInductive stx[1].getArgs
     else
-      throwError "invalid mutual block: either all elements of the block must be inductive/structure declarations, or they must all be definitions/theorems/abbrevs"
+      throwError "invalid mutual block: either all elements of the block must be inductive declarations, or they must all be definitions/theorems/abbrevs"
 
 /- leading_parser "attribute " >> "[" >> sepBy1 (eraseAttr <|> Term.attrInstance) ", " >> "]" >> many1 ident -/
 @[builtin_command_elab «attribute»] def elabAttr : CommandElab := fun stx => do

src/Lean/Elab/Inductive.lean

@@ -1,36 +1,102 @@
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Kyle Miller
+Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Elab.MutualInductive
+import Lean.Util.ForEachExprWhere
+import Lean.Util.ReplaceLevel
+import Lean.Util.ReplaceExpr
+import Lean.Util.CollectLevelParams
+import Lean.Meta.Constructions
+import Lean.Meta.CollectFVars
+import Lean.Meta.SizeOf
+import Lean.Meta.Injective
+import Lean.Meta.IndPredBelow
+import Lean.Elab.Command
+import Lean.Elab.ComputedFields
+import Lean.Elab.DefView
+import Lean.Elab.DeclUtil
+import Lean.Elab.Deriving.Basic
+import Lean.Elab.DeclarationRange
 
 namespace Lean.Elab.Command
 open Meta
 
-/-
-```
-def Lean.Parser.Command.«inductive» :=
-  leading_parser "inductive " >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor
+builtin_initialize
+  registerTraceClass `Elab.inductive
 
-def Lean.Parser.Command.classInductive :=
-  leading_parser atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor >> optDeriving
-```
+register_builtin_option inductive.autoPromoteIndices : Bool := {
+    defValue := true
+    descr    := "Promote indices to parameters in inductive types whenever possible."
+  }
+
+def checkValidInductiveModifier [Monad m] [MonadError m] (modifiers : Modifiers) : m Unit := do
+  if modifiers.isNoncomputable then
+    throwError "invalid use of 'noncomputable' in inductive declaration"
+  if modifiers.isPartial then
+    throwError "invalid use of 'partial' in inductive declaration"
+
+def checkValidCtorModifier [Monad m] [MonadError m] (modifiers : Modifiers) : m Unit := do
+  if modifiers.isNoncomputable then
+    throwError "invalid use of 'noncomputable' in constructor declaration"
+  if modifiers.isPartial then
+    throwError "invalid use of 'partial' in constructor declaration"
+  if modifiers.isUnsafe then
+    throwError "invalid use of 'unsafe' in constructor declaration"
+  if modifiers.attrs.size != 0 then
+    throwError "invalid use of attributes in constructor declaration"
+
+structure CtorView where
+  ref       : Syntax
+  modifiers : Modifiers
+  declName  : Name
+  binders   : Syntax
+  type?     : Option Syntax
+  deriving Inhabited
+
+structure ComputedFieldView where
+  ref       : Syntax
+  modifiers : Syntax
+  fieldId   : Name
+  type      : Syntax.Term
+  matchAlts : TSyntax ``Parser.Term.matchAlts
+
+structure InductiveView where
+  ref             : Syntax
+  declId          : Syntax
+  modifiers       : Modifiers
+  shortDeclName   : Name
+  declName        : Name
+  levelNames      : List Name
+  binders         : Syntax
+  type?           : Option Syntax
+  ctors           : Array CtorView
+  derivingClasses : Array DerivingClassView
+  computedFields  : Array ComputedFieldView
+  deriving Inhabited
+
+structure ElabHeaderResult where
+  view       : InductiveView
+  lctx       : LocalContext
+  localInsts : LocalInstances
+  levelNames : List Name
+  params     : Array Expr
+  type       : Expr
+  deriving Inhabited
+
+/-
+leading_parser "inductive " >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor
+leading_parser atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor >> optDeriving
 -/
 private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : TermElabM InductiveView := do
-  let isClass := decl.isOfKind ``Parser.Command.classInductive
-  let modifiers := if isClass then modifiers.addAttr { name := `class } else modifiers
+  checkValidInductiveModifier modifiers
   let (binders, type?) := expandOptDeclSig decl[2]
   let declId           := decl[1]
   let ⟨name, declName, levelNames⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers
   addDeclarationRangesForBuiltin declName modifiers.stx decl
   let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
-    /-
-    ```
-    def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
-    ```
-    -/
+    -- def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
     let mut ctorModifiers ← elabModifiers ⟨ctor[2]⟩
     if let some leadingDocComment := ctor[0].getOptional? then
       if ctorModifiers.docString?.isSome then
@@ -47,7 +113,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Term
     let (binders, type?) := expandOptDeclSig ctor[4]
     addDocString' ctorName ctorModifiers.docString?
     addDeclarationRangesFromSyntax ctorName ctor ctor[3]
-    return { ref := ctor, declId := ctor[3], modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
+    return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
   let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
     return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
   let classes ← getOptDerivingClasses decl[6]
@@ -59,13 +125,137 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Term
     ref             := decl
     shortDeclName   := name
     derivingClasses := classes
-    allowIndices    := true
-    allowSortPolymorphism := true
-    declId, modifiers, isClass, declName, levelNames
+    declId, modifiers, declName, levelNames
     binders, type?, ctors
     computedFields
   }
 
+private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc : Array ElabHeaderResult) : TermElabM (Array ElabHeaderResult) :=
+  Term.withAutoBoundImplicitForbiddenPred (fun n => views.any (·.shortDeclName == n)) do
+    if h : i < views.size then
+      let view := views[i]
+      let acc ← Term.withAutoBoundImplicit <| Term.elabBinders view.binders.getArgs fun params => do
+        match view.type? with
+        | none         =>
+          let u ← mkFreshLevelMVar
+          let type := mkSort u
+          Term.synthesizeSyntheticMVarsNoPostponing
+          Term.addAutoBoundImplicits' params type fun params type => do
+            let levelNames ← Term.getLevelNames
+            return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), levelNames, params, type, view }
+        | some typeStx =>
+          let (type, _) ← Term.withAutoBoundImplicit do
+            let type ← Term.elabType typeStx
+            unless (← isTypeFormerType type) do
+              throwErrorAt typeStx "invalid inductive type, resultant type is not a sort"
+            Term.synthesizeSyntheticMVarsNoPostponing
+            let indices ← Term.addAutoBoundImplicits #[]
+            return (← mkForallFVars indices type, indices.size)
+          Term.addAutoBoundImplicits' params type fun params type => do
+            trace[Elab.inductive] "header params: {params}, type: {type}"
+            let levelNames ← Term.getLevelNames
+            return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), levelNames, params, type, view }
+      elabHeaderAux views (i+1) acc
+    else
+      return acc
+
+private def checkNumParams (rs : Array ElabHeaderResult) : TermElabM Nat := do
+  let numParams := rs[0]!.params.size
+  for r in rs do
+    unless r.params.size == numParams do
+      throwErrorAt r.view.ref "invalid inductive type, number of parameters mismatch in mutually inductive datatypes"
+  return numParams
+
+private def checkUnsafe (rs : Array ElabHeaderResult) : TermElabM Unit := do
+  let isUnsafe := rs[0]!.view.modifiers.isUnsafe
+  for r in rs do
+    unless r.view.modifiers.isUnsafe == isUnsafe do
+      throwErrorAt r.view.ref "invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes"
+
+private def InductiveView.checkLevelNames (views : Array InductiveView) : TermElabM Unit := do
+  if h : views.size > 1 then
+    let levelNames := views[0].levelNames
+    for view in views do
+      unless view.levelNames == levelNames do
+        throwErrorAt view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
+
+private def ElabHeaderResult.checkLevelNames (rs : Array ElabHeaderResult) : TermElabM Unit := do
+  if h : rs.size > 1 then
+    let levelNames := rs[0].levelNames
+    for r in rs do
+      unless r.levelNames == levelNames do
+        throwErrorAt r.view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
+
+private def mkTypeFor (r : ElabHeaderResult) : TermElabM Expr := do
+  withLCtx r.lctx r.localInsts do
+    mkForallFVars r.params r.type
+
+private def throwUnexpectedInductiveType : TermElabM α :=
+  throwError "unexpected inductive resulting type"
+
+private def eqvFirstTypeResult (firstType type : Expr) : MetaM Bool :=
+  forallTelescopeReducing firstType fun _ firstTypeResult => isDefEq firstTypeResult type
+
+-- Auxiliary function for checking whether the types in mutually inductive declaration are compatible.
+private partial def checkParamsAndResultType (type firstType : Expr) (numParams : Nat) : TermElabM Unit := do
+  try
+    forallTelescopeCompatible type firstType numParams fun _ type firstType =>
+    forallTelescopeReducing type fun _ type =>
+    forallTelescopeReducing firstType fun _ firstType => do
+      let type ← whnfD type
+      match type with
+      | .sort .. =>
+        unless (← isDefEq firstType type) do
+          throwError "resulting universe mismatch, given{indentExpr type}\nexpected type{indentExpr firstType}"
+      | _ =>
+        throwError "unexpected inductive resulting type"
+  catch
+    | Exception.error ref msg => throw (Exception.error ref m!"invalid mutually inductive types, {msg}")
+    | ex => throw ex
+
+-- Auxiliary function for checking whether the types in mutually inductive declaration are compatible.
+private def checkHeader (r : ElabHeaderResult) (numParams : Nat) (firstType? : Option Expr) : TermElabM Expr := do
+  let type ← mkTypeFor r
+  match firstType? with
+  | none           => return type
+  | some firstType =>
+    withRef r.view.ref <| checkParamsAndResultType type firstType numParams
+    return firstType
+
+-- Auxiliary function for checking whether the types in mutually inductive declaration are compatible.
+private partial def checkHeaders (rs : Array ElabHeaderResult) (numParams : Nat) (i : Nat) (firstType? : Option Expr) : TermElabM Unit := do
+  if h : i < rs.size then
+    let type ← checkHeader rs[i] numParams firstType?
+    checkHeaders rs numParams (i+1) type
+
+private def elabHeader (views : Array InductiveView) : TermElabM (Array ElabHeaderResult) := do
+  let rs ← elabHeaderAux views 0 #[]
+  if rs.size > 1 then
+    checkUnsafe rs
+    let numParams ← checkNumParams rs
+    checkHeaders rs numParams 0 none
+  return rs
+
+/-- Create a local declaration for each inductive type in `rs`, and execute `x params indFVars`, where `params` are the inductive type parameters and
+   `indFVars` are the new local declarations.
+   We use the local context/instances and parameters of rs[0].
+   Note that this method is executed after we executed `checkHeaders` and established all
+   parameters are compatible. -/
+private partial def withInductiveLocalDecls (rs : Array ElabHeaderResult) (x : Array Expr → Array Expr → TermElabM α) : TermElabM α := do
+  let namesAndTypes ← rs.mapM fun r => do
+    let type ← mkTypeFor r
+    pure (r.view.declName, r.view.shortDeclName, type)
+  let r0     := rs[0]!
+  let params := r0.params
+  withLCtx r0.lctx r0.localInsts <| withRef r0.view.ref do
+    let rec loop (i : Nat) (indFVars : Array Expr) := do
+      if h : i < namesAndTypes.size then
+        let (declName, shortDeclName, type) := namesAndTypes[i]
+        Term.withAuxDecl shortDeclName type declName fun indFVar => loop (i+1) (indFVars.push indFVar)
+      else
+        x params indFVars
+    loop 0 #[]
+
 private def isInductiveFamily (numParams : Nat) (indFVar : Expr) : TermElabM Bool := do
   let indFVarType ← inferType indFVar
   forallTelescopeReducing indFVarType fun xs _ =>
@@ -81,8 +271,8 @@ where
     | _ => acc
 
 /--
-Replaces binder names in `type` with `newNames`.
-Remark: we only replace the names for binder containing macroscopes.
+  Replace binder names in `type` with `newNames`.
+  Remark: we only replace the names for binder containing macroscopes.
 -/
 private def replaceArrowBinderNames (type : Expr) (newNames : Array Name) : Expr :=
   go type 0
@@ -100,20 +290,20 @@ where
       type
 
 /--
-Reorders constructor arguments to improve the effectiveness of the `fixedIndicesToParams` method.
+  Reorder constructor arguments to improve the effectiveness of the `fixedIndicesToParams` method.
 
-The idea is quite simple. Given a constructor type of the form
-```
-(a₁ : A₁) → ... → (aₙ : Aₙ) → C b₁ ... bₘ
-```
-We try to find the longest prefix `b₁ ... bᵢ`, `i ≤ m` s.t.
-- each `bₖ` is in `{a₁, ..., aₙ}`
-- each `bₖ` only depends on variables in `{b₁, ..., bₖ₋₁}`
+  The idea is quite simple. Given a constructor type of the form
+  ```
+  (a₁ : A₁) → ... → (aₙ : Aₙ) → C b₁ ... bₘ
+  ```
+  We try to find the longest prefix `b₁ ... bᵢ`, `i ≤ m` s.t.
+  - each `bₖ` is in `{a₁, ..., aₙ}`
+  - each `bₖ` only depends on variables in `{b₁, ..., bₖ₋₁}`
 
-Then, it moves this prefix `b₁ ... bᵢ` to the front.
+  Then, it moves this prefix `b₁ ... bᵢ` to the front.
 
-Remark: We only reorder implicit arguments that have macroscopes. See issue #1156.
-The macroscope test is an approximation, we could have restricted ourselves to auto-implicit arguments.
+  Remark: We only reorder implicit arguments that have macroscopes. See issue #1156.
+  The macroscope test is an approximation, we could have restricted ourselves to auto-implicit arguments.
 -/
 private def reorderCtorArgs (ctorType : Expr) : MetaM Expr := do
   forallTelescopeReducing ctorType fun as type => do
@@ -158,6 +348,16 @@ private def reorderCtorArgs (ctorType : Expr) : MetaM Expr := do
       let binderNames := getArrowBinderNames (← instantiateMVars (← inferType C))
       return replaceArrowBinderNames r binderNames[:bsPrefix.size]
 
+/--
+  Execute `k` with updated binder information for `xs`. Any `x` that is explicit becomes implicit.
+-/
+private def withExplicitToImplicit (xs : Array Expr) (k : TermElabM α) : TermElabM α := do
+  let mut toImplicit := #[]
+  for x in xs do
+    if (← getFVarLocalDecl x).binderInfo.isExplicit then
+      toImplicit := toImplicit.push (x.fvarId!, BinderInfo.implicit)
+  withNewBinderInfos toImplicit k
+
 /--
   Elaborate constructor types.
 
@@ -166,20 +366,17 @@ private def reorderCtorArgs (ctorType : Expr) : MetaM Expr := do
   - Positivity (it is a rare failure, and the kernel already checks for it).
   - Universe constraints (the kernel checks for it).
 -/
-private def elabCtors (indFVars : Array Expr) (params : Array Expr) (r : ElabHeaderResult) : TermElabM (List Constructor) :=
-  withRef r.view.ref do
-  withExplicitToImplicit params do
-  let indFVar := r.indFVar
+private def elabCtors (indFVars : Array Expr) (indFVar : Expr) (params : Array Expr) (r : ElabHeaderResult) : TermElabM (List Constructor) := withRef r.view.ref do
   let indFamily ← isInductiveFamily params.size indFVar
   r.view.ctors.toList.mapM fun ctorView =>
     Term.withAutoBoundImplicit <| Term.elabBinders ctorView.binders.getArgs fun ctorParams =>
       withRef ctorView.ref do
-        let elabCtorType : TermElabM Expr := do
+        let rec elabCtorType (k : Expr → TermElabM Constructor) : TermElabM Constructor := do
           match ctorView.type? with
           | none          =>
             if indFamily then
               throwError "constructor resulting type must be specified in inductive family declaration"
-            return mkAppN indFVar params
+            k <| mkAppN indFVar params
           | some ctorType =>
             let type ← Term.elabType ctorType
             trace[Elab.inductive] "elabType {ctorView.declName} : {type} "
@@ -191,43 +388,43 @@ private def elabCtors (indFVars : Array Expr) (params : Array Expr) (r : ElabHea
                 throwError "unexpected constructor resulting type{indentExpr resultingType}"
               unless (← isType resultingType) do
                 throwError "unexpected constructor resulting type, type expected{indentExpr resultingType}"
-            return type
-        let type ← elabCtorType
-        Term.synthesizeSyntheticMVarsNoPostponing
-        let ctorParams ← Term.addAutoBoundImplicits ctorParams
-        let except (mvarId : MVarId) := ctorParams.any fun ctorParam => ctorParam.isMVar && ctorParam.mvarId! == mvarId
-        /-
-          We convert metavariables in the resulting type into extra parameters. Otherwise, we would not be able to elaborate
-          declarations such as
-          ```
-          inductive Palindrome : List α → Prop where
-            | nil      : Palindrome [] -- We would get an error here saying "failed to synthesize implicit argument" at `@List.nil ?m`
-            | single   : (a : α) → Palindrome [a]
-            | sandwich : (a : α) → Palindrome as → Palindrome ([a] ++ as ++ [a])
-          ```
-          We used to also collect unassigned metavariables on `ctorParams`, but it produced counterintuitive behavior.
-          For example, the following declaration used to be accepted.
-          ```
-          inductive Foo
-          | bar (x)
+            k type
+        elabCtorType fun type => do
+          Term.synthesizeSyntheticMVarsNoPostponing
+          let ctorParams ← Term.addAutoBoundImplicits ctorParams
+          let except (mvarId : MVarId) := ctorParams.any fun ctorParam => ctorParam.isMVar && ctorParam.mvarId! == mvarId
+          /-
+            We convert metavariables in the resulting type info extra parameters. Otherwise, we would not be able to elaborate
+            declarations such as
+            ```
+            inductive Palindrome : List α → Prop where
+              | nil      : Palindrome [] -- We would get an error here saying "failed to synthesize implicit argument" at `@List.nil ?m`
+              | single   : (a : α) → Palindrome [a]
+              | sandwich : (a : α) → Palindrome as → Palindrome ([a] ++ as ++ [a])
+            ```
+            We used to also collect unassigned metavariables on `ctorParams`, but it produced counterintuitive behavior.
+            For example, the following declaration used to be accepted.
+            ```
+            inductive Foo
+            | bar (x)
 
-          #check Foo.bar
-          -- @Foo.bar : {x : Sort u_1} → x → Foo
-          ```
-          which is also inconsistent with the behavior of auto implicits in definitions. For example, the following example was never accepted.
-          ```
-          def bar (x) := 1
-          ```
-        -/
-        let extraCtorParams ← Term.collectUnassignedMVars (← instantiateMVars type) #[] except
-        trace[Elab.inductive] "extraCtorParams: {extraCtorParams}"
-        /- We must abstract `extraCtorParams` and `ctorParams` simultaneously to make
-            sure we do not create auxiliary metavariables. -/
-        let type ← mkForallFVars (extraCtorParams ++ ctorParams) type
-        let type ← reorderCtorArgs type
-        let type ← mkForallFVars params type
-        trace[Elab.inductive] "{ctorView.declName} : {type}"
-        return { name := ctorView.declName, type }
+            #check Foo.bar
+            -- @Foo.bar : {x : Sort u_1} → x → Foo
+            ```
+            which is also inconsistent with the behavior of auto implicits in definitions. For example, the following example was never accepted.
+            ```
+            def bar (x) := 1
+            ```
+          -/
+          let extraCtorParams ← Term.collectUnassignedMVars (← instantiateMVars type) #[] except
+          trace[Elab.inductive] "extraCtorParams: {extraCtorParams}"
+          /- We must abstract `extraCtorParams` and `ctorParams` simultaneously to make
+             sure we do not create auxiliary metavariables. -/
+          let type  ← mkForallFVars (extraCtorParams ++ ctorParams) type
+          let type ← reorderCtorArgs type
+          let type ← mkForallFVars params type
+          trace[Elab.inductive] "{ctorView.declName} : {type}"
+          return { name := ctorView.declName, type }
 where
   checkParamOccs (ctorType : Expr) : MetaM Expr :=
     let visit (e : Expr) : MetaM TransformStep := do
@@ -247,15 +444,555 @@ where
         return .continue
     transform ctorType (pre := visit)
 
-@[builtin_inductive_elab Lean.Parser.Command.inductive, builtin_inductive_elab Lean.Parser.Command.classInductive]
-def elabInductiveCommand : InductiveElabDescr where
-  mkInductiveView (modifiers : Modifiers) (stx : Syntax) := do
-    let view ← inductiveSyntaxToView modifiers stx
-    return {
-      view
-      elabCtors := fun rs r params => do
-        let ctors ← elabCtors (rs.map (·.indFVar)) params r
-        return { ctors }
-    }
+private def getResultingUniverse : List InductiveType → TermElabM Level
+  | []           => throwError "unexpected empty inductive declaration"
+  | indType :: _ => forallTelescopeReducing indType.type fun _ r => do
+    let r ← whnfD r
+    match r with
+    | Expr.sort u => return u
+    | _           => throwError "unexpected inductive type resulting type{indentExpr r}"
+
+/--
+  Return `some ?m` if `u` is of the form `?m + k`.
+  Return none if `u` does not contain universe metavariables.
+  Throw exception otherwise. -/
+def shouldInferResultUniverse (u : Level) : TermElabM (Option LMVarId) := do
+  let u ← instantiateLevelMVars u
+  if u.hasMVar then
+    match u.getLevelOffset with
+    | Level.mvar mvarId => return some mvarId
+    | _ =>
+      throwError "cannot infer resulting universe level of inductive datatype, given level contains metavariables {mkSort u}, provide universe explicitly"
+  else
+    return none
+
+/--
+  Convert universe metavariables into new parameters. It skips `univToInfer?` (the inductive datatype resulting universe) because
+  it should be inferred later using `inferResultingUniverse`.
+-/
+private def levelMVarToParam (indTypes : List InductiveType) (univToInfer? : Option LMVarId) : TermElabM (List InductiveType) :=
+  indTypes.mapM fun indType => do
+    let type  ← levelMVarToParam' indType.type
+    let ctors ← indType.ctors.mapM fun ctor => do
+      let ctorType ← levelMVarToParam' ctor.type
+      return { ctor with type := ctorType }
+    return { indType with ctors, type }
+where
+  levelMVarToParam' (type : Expr) : TermElabM Expr := do
+    Term.levelMVarToParam type (except := fun mvarId => univToInfer? == some mvarId)
+
+def mkResultUniverse (us : Array Level) (rOffset : Nat) (preferProp : Bool) : Level :=
+  if us.isEmpty && rOffset == 0 then
+    if preferProp then levelZero else levelOne
+  else
+    let r := Level.mkNaryMax us.toList
+    if rOffset == 0 && !r.isZero && !r.isNeverZero then
+      mkLevelMax r levelOne |>.normalize
+    else
+      r.normalize
+
+ /--
+   Auxiliary function for `updateResultingUniverse`
+   `accLevel u r rOffset` add `u` to state if it is not already there and
+   it is different from the resulting universe level `r+rOffset`.
+
+
+   If `u` is a `max`, then its components are recursively processed.
+   If `u` is a `succ` and `rOffset > 0`, we process the `u`s child using `rOffset-1`.
+
+   This method is used to infer the resulting universe level of an inductive datatype.
+ -/
+def accLevel (u : Level) (r : Level) (rOffset : Nat) : OptionT (StateT (Array Level) Id) Unit := do
+  go u rOffset
+where
+  go (u : Level) (rOffset : Nat) : OptionT (StateT (Array Level) Id) Unit := do
+    match u, rOffset with
+    | .max u v,  rOffset   => go u rOffset; go v rOffset
+    | .imax u v, rOffset   => go u rOffset; go v rOffset
+    | .zero,     _         => return ()
+    | .succ u,   rOffset+1 => go u rOffset
+    | u,         rOffset   =>
+      if rOffset == 0 && u == r then
+        return ()
+      else if r.occurs u  then
+        failure
+      else if rOffset > 0 then
+        failure
+      else if (← get).contains u then
+        return ()
+      else
+        modify fun us => us.push u
+
+/--
+  Auxiliary function for `updateResultingUniverse`
+  `accLevelAtCtor ctor ctorParam r rOffset` add `u` (`ctorParam`'s universe) to state if it is not already there and
+  it is different from the resulting universe level `r+rOffset`.
+
+  See `accLevel`.
+-/
+def accLevelAtCtor (ctor : Constructor) (ctorParam : Expr) (r : Level) (rOffset : Nat) : StateRefT (Array Level) TermElabM Unit := do
+  let type ← inferType ctorParam
+  let u ← instantiateLevelMVars (← getLevel type)
+  match (← modifyGet fun s => accLevel u r rOffset |>.run |>.run s) with
+  | some _ => pure ()
+  | none =>
+    let typeType ← inferType type
+    let mut msg := m!"failed to compute resulting universe level of inductive datatype, constructor '{ctor.name}' has type{indentExpr ctor.type}\nparameter"
+    let localDecl ← getFVarLocalDecl ctorParam
+    unless localDecl.userName.hasMacroScopes do
+      msg := msg ++ m!" '{ctorParam}'"
+    msg := msg ++ m!" has type{indentD m!"{type} : {typeType}"}\ninductive type resulting type{indentExpr (mkSort (r.addOffset rOffset))}"
+    if r.isMVar then
+      msg := msg ++ "\nrecall that Lean only infers the resulting universe level automatically when there is a unique solution for the universe level constraints, consider explicitly providing the inductive type resulting universe level"
+    throwError msg
+
+/--
+  Execute `k` using the `Syntax` reference associated with constructor `ctorName`.
+-/
+def withCtorRef [Monad m] [MonadRef m] (views : Array InductiveView) (ctorName : Name) (k : m α) : m α := do
+  for view in views do
+    for ctorView in view.ctors do
+      if ctorView.declName == ctorName then
+        return (← withRef ctorView.ref k)
+  k
+
+/-- Auxiliary function for `updateResultingUniverse` -/
+private partial def collectUniverses (views : Array InductiveView) (r : Level) (rOffset : Nat) (numParams : Nat) (indTypes : List InductiveType) : TermElabM (Array Level) := do
+  let (_, us) ← go |>.run #[]
+  return us
+where
+  go : StateRefT (Array Level) TermElabM Unit :=
+    indTypes.forM fun indType => indType.ctors.forM fun ctor =>
+      withCtorRef views ctor.name do
+        forallTelescopeReducing ctor.type fun ctorParams _ =>
+          for ctorParam in ctorParams[numParams:] do
+            accLevelAtCtor ctor ctorParam r rOffset
+
+/--
+Decides whether the inductive type should be `Prop`-valued when the universe is not given
+and when the universe inference algorithm `collectUniverses` determines
+that the inductive type could naturally be `Prop`-valued.
+Recall: the natural universe level is the mimimum universe level for all the types of all the constructor parameters.
+
+Heuristic:
+- We want `Prop` when each inductive type is a syntactic subsingleton.
+  That's to say, when each inductive type has at most one constructor.
+  Such types carry no data anyway.
+- Exception: if no inductive type has any constructors, these are likely stubbed-out declarations,
+  so we prefer `Type` instead.
+- Exception: if each constructor has no parameters, then these are likely partially-written enumerations,
+  so we prefer `Type` instead.
+-/
+private def isPropCandidate (numParams : Nat) (indTypes : List InductiveType) : MetaM Bool := do
+  unless indTypes.foldl (fun n indType => max n indType.ctors.length) 0 == 1 do
+    return false
+  for indType in indTypes do
+    for ctor in indType.ctors do
+      let cparams ← forallTelescopeReducing ctor.type fun ctorParams _ => pure (ctorParams.size - numParams)
+      unless cparams == 0 do
+        return true
+  return false
+
+private def updateResultingUniverse (views : Array InductiveView) (numParams : Nat) (indTypes : List InductiveType) : TermElabM (List InductiveType) := do
+  let r ← getResultingUniverse indTypes
+  let rOffset : Nat   := r.getOffset
+  let r       : Level := r.getLevelOffset
+  unless r.isMVar do
+    throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly: {r}"
+  let us ← collectUniverses views r rOffset numParams indTypes
+  trace[Elab.inductive] "updateResultingUniverse us: {us}, r: {r}, rOffset: {rOffset}"
+  let rNew := mkResultUniverse us rOffset (← isPropCandidate numParams indTypes)
+  assignLevelMVar r.mvarId! rNew
+  indTypes.mapM fun indType => do
+    let type ← instantiateMVars indType.type
+    let ctors ← indType.ctors.mapM fun ctor => return { ctor with type := (← instantiateMVars ctor.type) }
+    return { indType with type, ctors }
+
+register_builtin_option bootstrap.inductiveCheckResultingUniverse : Bool := {
+    defValue := true,
+    group    := "bootstrap",
+    descr    := "by default the `inductive`/`structure` commands report an error if the resulting universe is not zero, but may be zero for some universe parameters. Reason: unless this type is a subsingleton, it is hardly what the user wants since it can only eliminate into `Prop`. In the `Init` package, we define subsingletons, and we use this option to disable the check. This option may be deleted in the future after we improve the validator"
+}
+
+def checkResultingUniverse (u : Level) : TermElabM Unit := do
+  if bootstrap.inductiveCheckResultingUniverse.get (← getOptions) then
+    let u ← instantiateLevelMVars u
+    if !u.isZero && !u.isNeverZero then
+      throwError "invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'){indentD u}"
+
+private def checkResultingUniverses (views : Array InductiveView) (numParams : Nat) (indTypes : List InductiveType) : TermElabM Unit := do
+  let u := (← instantiateLevelMVars (← getResultingUniverse indTypes)).normalize
+  checkResultingUniverse u
+  unless u.isZero do
+    indTypes.forM fun indType => indType.ctors.forM fun ctor =>
+      forallTelescopeReducing ctor.type fun ctorArgs _ => do
+        for ctorArg in ctorArgs[numParams:] do
+          let type ← inferType ctorArg
+          let v := (← instantiateLevelMVars (← getLevel type)).normalize
+          let rec check (v' : Level) (u' : Level) : TermElabM Unit :=
+            match v', u' with
+            | .succ v', .succ u' => check v' u'
+            | .mvar id, .param ..  =>
+              /- Special case:
+                 The constructor parameter `v` is at unverse level `?v+k` and
+                 the resulting inductive universe level is `u'+k`, where `u'` is a parameter (or zero).
+                 Thus, `?v := u'` is the only choice for satisfying the universe constraint `?v+k <= u'+k`.
+                 Note that, we still generate an error for cases where there is more than one of satisfying the constraint.
+                 Examples:
+                 -----------------------------------------------------------
+                 | ctor universe level | inductive datatype universe level |
+                 -----------------------------------------------------------
+                 |   ?v                | max u w                           |
+                 -----------------------------------------------------------
+                 |   ?v                | u + 1                             |
+                 -----------------------------------------------------------
+              -/
+              assignLevelMVar id u'
+            | .mvar id, .zero => assignLevelMVar id u' -- TODO: merge with previous case
+            | _, _ =>
+              unless u.geq v do
+                let mut msg := m!"invalid universe level in constructor '{ctor.name}', parameter"
+                let localDecl ← getFVarLocalDecl ctorArg
+                unless localDecl.userName.hasMacroScopes do
+                  msg := msg ++ m!" '{ctorArg}'"
+                msg := msg ++ m!" has type{indentExpr type}"
+                msg := msg ++ m!"\nat universe level{indentD v}"
+                msg := msg ++ m!"\nit must be smaller than or equal to the inductive datatype universe level{indentD u}"
+                withCtorRef views ctor.name <| throwError msg
+          check v u
+
+private def collectUsed (indTypes : List InductiveType) : StateRefT CollectFVars.State MetaM Unit := do
+  indTypes.forM fun indType => do
+    indType.type.collectFVars
+    indType.ctors.forM fun ctor =>
+      ctor.type.collectFVars
+
+private def removeUnused (vars : Array Expr) (indTypes : List InductiveType) : TermElabM (LocalContext × LocalInstances × Array Expr) := do
+  let (_, used) ← (collectUsed indTypes).run {}
+  Meta.removeUnused vars used
+
+private def withUsed {α} (vars : Array Expr) (indTypes : List InductiveType) (k : Array Expr → TermElabM α) : TermElabM α := do
+  let (lctx, localInsts, vars) ← removeUnused vars indTypes
+  withLCtx lctx localInsts <| k vars
+
+private def updateParams (vars : Array Expr) (indTypes : List InductiveType) : TermElabM (List InductiveType) :=
+  indTypes.mapM fun indType => do
+    let type ← mkForallFVars vars indType.type
+    let ctors ← indType.ctors.mapM fun ctor => do
+      let ctorType ← withExplicitToImplicit vars (mkForallFVars vars ctor.type)
+      return { ctor with type := ctorType }
+    return { indType with type, ctors }
+
+private def collectLevelParamsInInductive (indTypes : List InductiveType) : Array Name := Id.run do
+  let mut usedParams : CollectLevelParams.State := {}
+  for indType in indTypes do
+    usedParams := collectLevelParams usedParams indType.type
+    for ctor in indType.ctors do
+      usedParams := collectLevelParams usedParams ctor.type
+  return usedParams.params
+
+private def mkIndFVar2Const (views : Array InductiveView) (indFVars : Array Expr) (levelNames : List Name) : ExprMap Expr := Id.run do
+  let levelParams := levelNames.map mkLevelParam;
+  let mut m : ExprMap Expr := {}
+  for h : i in [:views.size] do
+    let view    := views[i]
+    let indFVar := indFVars[i]!
+    m := m.insert indFVar (mkConst view.declName levelParams)
+  return m
+
+/-- Remark: `numVars <= numParams`. `numVars` is the number of context `variables` used in the inductive declaration,
+   and `numParams` is `numVars` + number of explicit parameters provided in the declaration. -/
+private def replaceIndFVarsWithConsts (views : Array InductiveView) (indFVars : Array Expr) (levelNames : List Name)
+    (numVars : Nat) (numParams : Nat) (indTypes : List InductiveType) : TermElabM (List InductiveType) :=
+  let indFVar2Const := mkIndFVar2Const views indFVars levelNames
+  indTypes.mapM fun indType => do
+    let ctors ← indType.ctors.mapM fun ctor => do
+      let type ← forallBoundedTelescope ctor.type numParams fun params type => do
+        let type := type.replace fun e =>
+          if !e.isFVar then
+            none
+          else match indFVar2Const[e]? with
+            | none   => none
+            | some c => mkAppN c (params.extract 0 numVars)
+        instantiateMVars (← mkForallFVars params type)
+      return { ctor with type }
+    return { indType with ctors }
+
+private def mkAuxConstructions (views : Array InductiveView) : TermElabM Unit := do
+  let env ← getEnv
+  let hasEq   := env.contains ``Eq
+  let hasHEq  := env.contains ``HEq
+  let hasUnit := env.contains ``PUnit
+  let hasProd := env.contains ``Prod
+  for view in views do
+    let n := view.declName
+    mkRecOn n
+    if hasUnit then mkCasesOn n
+    if hasUnit && hasEq && hasHEq then mkNoConfusion n
+    if hasUnit && hasProd then mkBelow n
+    if hasUnit && hasProd then mkIBelow n
+  for view in views do
+    let n := view.declName;
+    if hasUnit && hasProd then mkBRecOn n
+    if hasUnit && hasProd then mkBInductionOn n
+
+private def getArity (indType : InductiveType) : MetaM Nat :=
+  forallTelescopeReducing indType.type fun xs _ => return xs.size
+
+private def resetMaskAt (mask : Array Bool) (i : Nat) : Array Bool :=
+  mask.setD i false
+
+/--
+  Compute a bit-mask that for `indType`. The size of the resulting array `result` is the arity of `indType`.
+  The first `numParams` elements are `false` since they are parameters.
+  For `i ∈ [numParams, arity)`, we have that `result[i]` if this index of the inductive family is fixed.
+-/
+private def computeFixedIndexBitMask (numParams : Nat) (indType : InductiveType) (indFVars : Array Expr) : MetaM (Array Bool) := do
+  let arity ← getArity indType
+  if arity ≤ numParams then
+    return mkArray arity false
+  else
+    let maskRef ← IO.mkRef (mkArray numParams false ++ mkArray (arity - numParams) true)
+    let rec go (ctors : List Constructor) : MetaM (Array Bool) := do
+      match ctors with
+      | [] => maskRef.get
+      | ctor :: ctors =>
+        forallTelescopeReducing ctor.type fun xs type => do
+          let typeArgs := type.getAppArgs
+          for i in [numParams:arity] do
+            unless i < xs.size && xs[i]! == typeArgs[i]! do -- Remark: if we want to allow arguments to be rearranged, this test should be xs.contains typeArgs[i]
+              maskRef.modify fun mask => mask.set! i false
+          for x in xs[numParams:] do
+            let xType ← inferType x
+            let cond (e : Expr) := indFVars.any (fun indFVar => e.getAppFn == indFVar)
+            xType.forEachWhere (stopWhenVisited := true) cond fun e => do
+              let eArgs := e.getAppArgs
+              for i in [numParams:eArgs.size] do
+                if i >= typeArgs.size then
+                  maskRef.modify (resetMaskAt · i)
+                else
+                  unless eArgs[i]! == typeArgs[i]! do
+                    maskRef.modify (resetMaskAt · i)
+              /-If an index is missing in the arguments of the inductive type, then it must be non-fixed.
+                Consider the following example:
+                ```lean
+                inductive All {I : Type u} (P : I → Type v) : List I → Type (max u v) where
+                  | cons : P x → All P xs → All P (x :: xs)
+
+                inductive Iμ {I : Type u}  : I → Type (max u v) where
+                  | mk : (i : I)  → All Iμ [] → Iμ i
+                ```
+                because `i` doesn't appear in `All Iμ []`, the index shouldn't be fixed.
+              -/
+              for i in [eArgs.size:arity] do
+                maskRef.modify (resetMaskAt · i)
+        go ctors
+    go indType.ctors
+
+/-- Return true iff `arrowType` is an arrow and its domain is defeq to `type` -/
+private def isDomainDefEq (arrowType : Expr) (type : Expr) : MetaM Bool := do
+  if !arrowType.isForall then
+    return false
+  else
+    /-
+      We used to use `withNewMCtxDepth` to make sure we do not assign universe metavariables,
+      but it was not satisfactory. For example, in declarations such as
+      ```
+      inductive Eq : α → α → Prop where
+      | refl (a : α) : Eq a a
+      ```
+      We want the first two indices to be promoted to parameters, and this will only
+      happen if we can assign universe metavariables.
+    -/
+    isDefEq arrowType.bindingDomain! type
+
+/--
+  Convert fixed indices to parameters.
+-/
+private partial def fixedIndicesToParams (numParams : Nat) (indTypes : Array InductiveType) (indFVars : Array Expr) : MetaM Nat := do
+  if !inductive.autoPromoteIndices.get (← getOptions) then
+    return numParams
+  let masks ← indTypes.mapM (computeFixedIndexBitMask numParams · indFVars)
+  trace[Elab.inductive] "masks: {masks}"
+  if masks.all fun mask => !mask.contains true then
+    return numParams
+  -- We process just a non-fixed prefix of the indices for now. Reason: we don't want to change the order.
+  -- TODO: extend it in the future. For example, it should be reasonable to change
+  -- the order of indices generated by the auto implicit feature.
+  let mask := masks[0]!
+  forallBoundedTelescope indTypes[0]!.type numParams fun params type => do
+    let otherTypes ← indTypes[1:].toArray.mapM fun indType => do whnfD (← instantiateForall indType.type params)
+    let ctorTypes ← indTypes.toList.mapM fun indType => indType.ctors.mapM fun ctor => do whnfD (← instantiateForall ctor.type params)
+    let typesToCheck := otherTypes.toList ++ ctorTypes.flatten
+    let rec go (i : Nat) (type : Expr) (typesToCheck : List Expr) : MetaM Nat := do
+      if i < mask.size then
+        if !masks.all fun mask => i < mask.size && mask[i]! then
+           return i
+        if !type.isForall then
+          return i
+        let paramType := type.bindingDomain!
+        if !(← typesToCheck.allM fun type => isDomainDefEq type paramType) then
+          trace[Elab.inductive] "domain not def eq: {i}, {type} =?= {paramType}"
+          return i
+        withLocalDeclD `a paramType fun paramNew => do
+          let typesToCheck ← typesToCheck.mapM fun type => whnfD (type.bindingBody!.instantiate1 paramNew)
+          go (i+1) (type.bindingBody!.instantiate1 paramNew) typesToCheck
+      else
+        return i
+    go numParams type typesToCheck
+
+private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) : TermElabM Unit := Term.withoutSavingRecAppSyntax do
+  let view0 := views[0]!
+  let scopeLevelNames ← Term.getLevelNames
+  InductiveView.checkLevelNames views
+  let allUserLevelNames := view0.levelNames
+  let isUnsafe          := view0.modifiers.isUnsafe
+  withRef view0.ref <| Term.withLevelNames allUserLevelNames do
+    let rs ← elabHeader views
+    Term.synthesizeSyntheticMVarsNoPostponing
+    ElabHeaderResult.checkLevelNames rs
+    let allUserLevelNames := rs[0]!.levelNames
+    trace[Elab.inductive] "level names: {allUserLevelNames}"
+    withInductiveLocalDecls rs fun params indFVars => do
+      trace[Elab.inductive] "indFVars: {indFVars}"
+      let mut indTypesArray := #[]
+      for h : i in [:views.size] do
+        let indFVar := indFVars[i]!
+        Term.addLocalVarInfo views[i].declId indFVar
+        let r     := rs[i]!
+        /- At this point, because of `withInductiveLocalDecls`, the only fvars that are in context are the ones related to the first inductive type.
+           Because of this, we need to replace the fvars present in each inductive type's header of the mutual block with those of the first inductive.
+           However, some mvars may still be uninstantiated there, and might hide some of the old fvars.
+           As such we first need to synthesize all possible mvars at this stage, instantiate them in the header types and only
+           then replace the parameters' fvars in the header type.
+
+           See issue #3242 (`https://github.com/leanprover/lean4/issues/3242`)
+        -/
+        let type  ←  instantiateMVars r.type
+        let type  := type.replaceFVars r.params params
+        let type  ← mkForallFVars params type
+        let ctors ← withExplicitToImplicit params (elabCtors indFVars indFVar params r)
+        indTypesArray := indTypesArray.push { name := r.view.declName, type, ctors }
+      let numExplicitParams ← fixedIndicesToParams params.size indTypesArray indFVars
+      trace[Elab.inductive] "numExplicitParams: {numExplicitParams}"
+      let indTypes := indTypesArray.toList
+      let u ← getResultingUniverse indTypes
+      let univToInfer? ← shouldInferResultUniverse u
+      withUsed vars indTypes fun vars => do
+        let numVars   := vars.size
+        let numParams := numVars + numExplicitParams
+        let indTypes ← updateParams vars indTypes
+        let indTypes ← if let some univToInfer := univToInfer? then
+          updateResultingUniverse views numParams (← levelMVarToParam indTypes univToInfer)
+        else
+          checkResultingUniverses views numParams indTypes
+          levelMVarToParam indTypes none
+        let usedLevelNames := collectLevelParamsInInductive indTypes
+        match sortDeclLevelParams scopeLevelNames allUserLevelNames usedLevelNames with
+        | .error msg      => throwError msg
+        | .ok levelParams => do
+          let indTypes ← replaceIndFVarsWithConsts views indFVars levelParams numVars numParams indTypes
+          let decl := Declaration.inductDecl levelParams numParams indTypes isUnsafe
+          Term.ensureNoUnassignedMVars decl
+          addDecl decl
+          mkAuxConstructions views
+    withSaveInfoContext do  -- save new env
+      for view in views do
+        Term.addTermInfo' view.ref[1] (← mkConstWithLevelParams view.declName) (isBinder := true)
+        for ctor in view.ctors do
+          Term.addTermInfo' ctor.ref[3] (← mkConstWithLevelParams ctor.declName) (isBinder := true)
+        -- We need to invoke `applyAttributes` because `class` is implemented as an attribute.
+        Term.applyAttributesAt view.declName view.modifiers.attrs .afterTypeChecking
+
+private def applyDerivingHandlers (views : Array InductiveView) : CommandElabM Unit := do
+  let mut processed : NameSet := {}
+  for view in views do
+    for classView in view.derivingClasses do
+      let className := classView.className
+      unless processed.contains className do
+        processed := processed.insert className
+        let mut declNames := #[]
+        for view in views do
+          if view.derivingClasses.any fun classView => classView.className == className then
+            declNames := declNames.push view.declName
+        classView.applyHandlers declNames
+
+private def applyComputedFields (indViews : Array InductiveView) : CommandElabM Unit := do
+  if indViews.all (·.computedFields.isEmpty) then return
+
+  let mut computedFields := #[]
+  let mut computedFieldDefs := #[]
+  for indView@{declName, ..} in indViews do
+    for {ref, fieldId, type, matchAlts, modifiers, ..} in indView.computedFields do
+      computedFieldDefs := computedFieldDefs.push <| ← do
+        let modifiers ← match modifiers with
+          | `(Lean.Parser.Command.declModifiersT| $[$doc:docComment]? $[$attrs:attributes]? $[$vis]? $[noncomputable]?) =>
+            `(Lean.Parser.Command.declModifiersT| $[$doc]? $[$attrs]? $[$vis]? noncomputable)
+          | _ => do
+            withRef modifiers do logError "unsupported modifiers for computed field"
+            `(Parser.Command.declModifiersT| noncomputable)
+        `($(⟨modifiers⟩):declModifiers
+          def%$ref $(mkIdent <| `_root_ ++ declName ++ fieldId):ident : $type $matchAlts:matchAlts)
+    let computedFieldNames := indView.computedFields.map fun {fieldId, ..} => declName ++ fieldId
+    computedFields := computedFields.push (declName, computedFieldNames)
+  withScope (fun scope => { scope with
+      opts := scope.opts
+        |>.setBool `bootstrap.genMatcherCode false
+        |>.setBool `elaboratingComputedFields true}) <|
+    elabCommand <| ← `(mutual $computedFieldDefs* end)
+
+  liftTermElabM do Term.withDeclName indViews[0]!.declName do
+    ComputedFields.setComputedFields computedFields
+
+def elabInductiveViews (vars : Array Expr) (views : Array InductiveView) : TermElabM Unit := do
+  let view0 := views[0]!
+  let ref := view0.ref
+  Term.withDeclName view0.declName do withRef ref do
+    mkInductiveDecl vars views
+    mkSizeOfInstances view0.declName
+    Lean.Meta.IndPredBelow.mkBelow view0.declName
+    for view in views do
+      mkInjectiveTheorems view.declName
+
+def elabInductiveViewsPostprocessing (views : Array InductiveView) : CommandElabM Unit := do
+  let view0 := views[0]!
+  let ref := view0.ref
+  applyComputedFields views -- NOTE: any generated code before this line is invalid
+  applyDerivingHandlers views
+  runTermElabM fun _ => Term.withDeclName view0.declName do withRef ref do
+    for view in views do
+      Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation
+
+def elabInductives (inductives : Array (Modifiers × Syntax)) : CommandElabM Unit := do
+  let vs ← runTermElabM fun vars => do
+    let vs ← inductives.mapM fun (modifiers, stx) => inductiveSyntaxToView modifiers stx
+    elabInductiveViews vars vs
+    pure vs
+  elabInductiveViewsPostprocessing vs
+
+def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
+  elabInductives #[(modifiers, stx)]
+
+def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
+  let modifiers := modifiers.addAttr { name := `class }
+  elabInductive modifiers stx
+
+/--
+Returns true if all elements of the `mutual` block (`Lean.Parser.Command.mutual`) are inductive declarations.
+-/
+def isMutualInductive (stx : Syntax) : Bool :=
+  stx[1].getArgs.all fun elem =>
+    let decl     := elem[1]
+    let declKind := decl.getKind
+    declKind == `Lean.Parser.Command.inductive
+
+/--
+Elaborates a `mutual` block satisfying `Lean.Elab.Command.isMutualInductive`.
+-/
+def elabMutualInductive (elems : Array Syntax) : CommandElabM Unit := do
+  let inductives ← elems.mapM fun stx => do
+    let modifiers ← elabModifiers ⟨stx[0]⟩
+    pure (modifiers, stx[1])
+  elabInductives inductives
 
 end Lean.Elab.Command

src/Lean/Elab/MutualDef.lean

@@ -840,8 +840,8 @@ private def mkLetRecClosures (sectionVars : Array Expr) (mainFVarIds : Array FVa
 abbrev Replacement := FVarIdMap Expr
 
 def insertReplacementForMainFns (r : Replacement) (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mainFVars : Array Expr) : Replacement :=
-  mainFVars.size.fold (init := r) fun i _ r =>
-    r.insert mainFVars[i].fvarId! (mkAppN (Lean.mkConst mainHeaders[i]!.declName) sectionVars)
+  mainFVars.size.fold (init := r) fun i r =>
+    r.insert mainFVars[i]!.fvarId! (mkAppN (Lean.mkConst mainHeaders[i]!.declName) sectionVars)
 
 
 def insertReplacementForLetRecs (r : Replacement) (letRecClosures : List LetRecClosure) : Replacement :=
@@ -871,8 +871,8 @@ def Replacement.apply (r : Replacement) (e : Expr) : Expr :=
 
 def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mainVals : Array Expr)
     : TermElabM (Array PreDefinition) :=
-  mainHeaders.size.foldM (init := preDefs) fun i _ preDefs => do
-    let header := mainHeaders[i]
+  mainHeaders.size.foldM (init := preDefs) fun i preDefs => do
+    let header := mainHeaders[i]!
     let termination ← declValToTerminationHint header.value
     let termination := termination.rememberExtraParams header.numParams mainVals[i]!
     let value ← mkLambdaFVars sectionVars mainVals[i]!

src/Lean/Elab/StructInst.lean

@@ -302,58 +302,59 @@ instance : ToFormat FieldLHS where
     | .fieldIndex _ i => format i
     | .modifyOp _ i   => "[" ++ i.prettyPrint ++ "]"
 
-mutual
-  /--
-  `FieldVal StructInstView` is a representation of a field value in the structure instance.
-  -/
-  inductive FieldVal where
-    /-- A `term` to use for the value of the field. -/
-    | term (stx : Syntax)         : FieldVal
-    /-- A `StructInstView` to use for the value of a subobject field. -/
-    | nested (s : StructInstView) : FieldVal
-    /-- A field that was not provided and should be synthesized using default values. -/
-    | default                     : FieldVal
-    deriving Inhabited
+/--
+`FieldVal StructInstView` is a representation of a field value in the structure instance.
+-/
+inductive FieldVal (σ : Type) where
+  /-- A `term` to use for the value of the field. -/
+  | term (stx : Syntax)  : FieldVal σ
+  /-- A `StructInstView` to use for the value of a subobject field. -/
+  | nested (s : σ)       : FieldVal σ
+  /-- A field that was not provided and should be synthesized using default values. -/
+  | default              : FieldVal σ
+  deriving Inhabited
 
-  /--
-  `Field StructInstView` is a representation of a field in the structure instance.
-  -/
-  structure Field where
-    /-- The whole field syntax. -/
-    ref   : Syntax
-    /-- The LHS decomposed into components. -/
-    lhs   : List FieldLHS
-    /-- The value of the field. -/
-    val   : FieldVal
-    /-- The elaborated field value, filled in at `elabStruct`.
-    Missing fields use a metavariable for the elaborated value and are later solved for in `DefaultFields.propagate`. -/
-    expr? : Option Expr := none
-    deriving Inhabited
-
-  /--
-  The view for structure instance notation.
-  -/
-  structure StructInstView where
-    /-- The syntax for the whole structure instance. -/
-    ref : Syntax
-    /-- The name of the structure for the type of the structure instance. -/
-    structName : Name
-    /-- Used for default values, to propagate structure type parameters. It is initially empty, and then set at `elabStruct`. -/
-    params : Array (Name × Expr)
-    /-- The fields of the structure instance. -/
-    fields : List Field
-    /-- The additional sources for fields for the structure instance. -/
-    sources : SourcesView
-    deriving Inhabited
-end
+/--
+`Field StructInstView` is a representation of a field in the structure instance.
+-/
+structure Field (σ : Type) where
+  /-- The whole field syntax. -/
+  ref   : Syntax
+  /-- The LHS decomposed into components. -/
+  lhs   : List FieldLHS
+  /-- The value of the field. -/
+  val   : FieldVal σ
+  /-- The elaborated field value, filled in at `elabStruct`.
+  Missing fields use a metavariable for the elaborated value and are later solved for in `DefaultFields.propagate`. -/
+  expr? : Option Expr := none
+  deriving Inhabited
 
 /--
 Returns if the field has a single component in its LHS.
 -/
-def Field.isSimple : Field → Bool
+def Field.isSimple {σ} : Field σ → Bool
   | { lhs := [_], .. } => true
   | _                  => false
 
+/--
+The view for structure instance notation.
+-/
+structure StructInstView where
+  /-- The syntax for the whole structure instance. -/
+  ref : Syntax
+  /-- The name of the structure for the type of the structure instance. -/
+  structName : Name
+  /-- Used for default values, to propagate structure type parameters. It is initially empty, and then set at `elabStruct`. -/
+  params : Array (Name × Expr)
+  /-- The fields of the structure instance. -/
+  fields : List (Field StructInstView)
+  /-- The additional sources for fields for the structure instance. -/
+  sources : SourcesView
+  deriving Inhabited
+
+/-- Abbreviation for the type of `StructInstView.fields`, namely `List (Field StructInstView)`. -/
+abbrev Fields := List (Field StructInstView)
+
 /-- `true` iff all fields of the given structure are marked as `default` -/
 partial def StructInstView.allDefault (s : StructInstView) : Bool :=
   s.fields.all fun { val := val,  .. } => match val with
@@ -361,7 +362,7 @@ partial def StructInstView.allDefault (s : StructInstView) : Bool :=
     | .default  => true
     | .nested s => allDefault s
 
-def formatField (formatStruct : StructInstView → Format) (field : Field) : Format :=
+def formatField (formatStruct : StructInstView → Format) (field : Field StructInstView) : Format :=
   Format.joinSep field.lhs " . " ++ " := " ++
     match field.val with
     | .term v   => v.prettyPrint
@@ -377,11 +378,11 @@ partial def formatStruct : StructInstView → Format
     else
       "{" ++ format (source.explicit.map (·.stx)) ++ " with " ++ fieldsFmt ++ implicitFmt ++ "}"
 
-instance : ToFormat StructInstView := ⟨formatStruct⟩
+instance : ToFormat StructInstView     := ⟨formatStruct⟩
 instance : ToString StructInstView := ⟨toString ∘ format⟩
 
-instance : ToFormat Field := ⟨formatField formatStruct⟩
-instance : ToString Field := ⟨toString ∘ format⟩
+instance : ToFormat (Field StructInstView) := ⟨formatField formatStruct⟩
+instance : ToString (Field StructInstView) := ⟨toString ∘ format⟩
 
 /--
 Converts a `FieldLHS` back into syntax. This assumes the `ref` fields have the correct structure.
@@ -402,14 +403,14 @@ private def FieldLHS.toSyntax (first : Bool) : FieldLHS → Syntax
 /--
 Converts a `FieldVal StructInstView` back into syntax. Only supports `.term`, and it assumes the `stx` field has the correct structure.
 -/
-private def FieldVal.toSyntax : FieldVal → Syntax
+private def FieldVal.toSyntax : FieldVal Struct → Syntax
   | .term stx => stx
   | _         => unreachable!
 
 /--
 Converts a `Field StructInstView` back into syntax. Used to construct synthetic structure instance notation for subobjects in `StructInst.expandStruct` processing.
 -/
-private def Field.toSyntax : Field → Syntax
+private def Field.toSyntax : Field Struct → Syntax
   | field =>
     let stx := field.ref
     let stx := stx.setArg 2 field.val.toSyntax
@@ -451,14 +452,14 @@ private def mkStructView (stx : Syntax) (structName : Name) (sources : SourcesVi
     let val      := fieldStx[2]
     let first    ← toFieldLHS fieldStx[0][0]
     let rest     ← fieldStx[0][1].getArgs.toList.mapM toFieldLHS
-    return { ref := fieldStx, lhs := first :: rest, val := FieldVal.term val : Field }
+    return { ref := fieldStx, lhs := first :: rest, val := FieldVal.term val : Field StructInstView }
   return { ref := stx, structName, params := #[], fields, sources }
 
-def StructInstView.modifyFieldsM {m : Type → Type} [Monad m] (s : StructInstView) (f : List Field → m (List Field)) : m StructInstView :=
+def StructInstView.modifyFieldsM {m : Type → Type} [Monad m] (s : StructInstView) (f : Fields → m Fields) : m StructInstView :=
   match s with
   | { ref, structName, params, fields, sources } => return { ref, structName, params, fields := (← f fields), sources }
 
-def StructInstView.modifyFields (s : StructInstView) (f : List Field → List Field) : StructInstView :=
+def StructInstView.modifyFields (s : StructInstView) (f : Fields → Fields) : StructInstView :=
   Id.run <| s.modifyFieldsM f
 
 /-- Expands name field LHSs with multi-component names into multi-component LHSs. -/
@@ -524,14 +525,14 @@ private def expandParentFields (s : StructInstView) : TermElabM StructInstView :
           | _ => throwErrorAt ref "failed to access field '{fieldName}' in parent structure"
     | _ => return field
 
-private abbrev FieldMap := Std.HashMap Name (List Field)
+private abbrev FieldMap := Std.HashMap Name Fields
 
 /--
 Creates a hash map collecting all fields with the same first name component.
 Throws an error if there are multiple simple fields with the same name.
 Used by `StructInst.expandStruct` processing.
 -/
-private def mkFieldMap (fields : List Field) : TermElabM FieldMap :=
+private def mkFieldMap (fields : Fields) : TermElabM FieldMap :=
   fields.foldlM (init := {}) fun fieldMap field =>
     match field.lhs with
     | .fieldName _ fieldName :: _    =>
@@ -547,7 +548,7 @@ private def mkFieldMap (fields : List Field) : TermElabM FieldMap :=
 /--
 Given a value of the hash map created by `mkFieldMap`, returns true if the value corresponds to a simple field.
 -/
-private def isSimpleField? : List Field → Option Field
+private def isSimpleField? : Fields → Option (Field StructInstView)
   | [field] => if field.isSimple then some field else none
   | _       => none
 
@@ -565,7 +566,7 @@ def mkProjStx? (s : Syntax) (structName : Name) (fieldName : Name) : TermElabM (
 /--
 Finds a simple field of the given name.
 -/
-def findField? (fields : List Field) (fieldName : Name) : Option Field :=
+def findField? (fields : Fields) (fieldName : Name) : Option (Field StructInstView) :=
   fields.find? fun field =>
     match field.lhs with
     | [.fieldName _ n] => n == fieldName
@@ -619,7 +620,7 @@ mutual
         match findField? s.fields fieldName with
         | some field => return field::fields
         | none       =>
-          let addField (val : FieldVal) : TermElabM (List Field) := do
+          let addField (val : FieldVal StructInstView) : TermElabM Fields := do
             return { ref, lhs := [FieldLHS.fieldName ref fieldName], val := val } :: fields
           match Lean.isSubobjectField? env s.structName fieldName with
           | some substructName =>
@@ -772,7 +773,7 @@ private partial def elabStructInstView (s : StructInstView) (expectedType? : Opt
       trace[Elab.struct] "elabStruct {field}, {type}"
       match type with
       | .forallE _ d b bi =>
-        let cont (val : Expr) (field : Field) (instMVars := instMVars) : TermElabM (Expr × Expr × List Field × Array MVarId) := do
+        let cont (val : Expr) (field : Field StructInstView) (instMVars := instMVars) : TermElabM (Expr × Expr × Fields × Array MVarId) := do
           pushInfoTree <| InfoTree.node (children := {}) <| Info.ofFieldInfo {
             projName := s.structName.append fieldName, fieldName, lctx := (← getLCtx), val, stx := ref }
           let e     := mkApp e val
@@ -878,7 +879,7 @@ partial def getHierarchyDepth (struct : StructInstView) : Nat :=
     | _ => max
 
 /-- Returns whether the field is still missing. -/
-def isDefaultMissing? [Monad m] [MonadMCtx m] (field : Field) : m Bool := do
+def isDefaultMissing? [Monad m] [MonadMCtx m] (field : Field Struct) : m Bool := do
   if let some expr := field.expr? then
     if let some (.mvar mvarId) := defaultMissing? expr then
       unless (← mvarId.isAssigned) do
@@ -886,17 +887,17 @@ def isDefaultMissing? [Monad m] [MonadMCtx m] (field : Field) : m Bool := do
   return false
 
 /-- Returns a field that is still missing. -/
-partial def findDefaultMissing? [Monad m] [MonadMCtx m] (struct : StructInstView) : m (Option Field) :=
+partial def findDefaultMissing? [Monad m] [MonadMCtx m] (struct : StructInstView) : m (Option (Field StructInstView)) :=
   struct.fields.findSomeM? fun field => do
    match field.val with
    | .nested struct => findDefaultMissing? struct
    | _ => return if (← isDefaultMissing? field) then field else none
 
 /-- Returns all fields that are still missing. -/
-partial def allDefaultMissing [Monad m] [MonadMCtx m] (struct : StructInstView) : m (Array Field) :=
+partial def allDefaultMissing [Monad m] [MonadMCtx m] (struct : StructInstView) : m (Array (Field StructInstView)) :=
   go struct *> get |>.run' #[]
 where
-  go (struct : StructInstView) : StateT (Array Field) m Unit :=
+  go (struct : StructInstView) : StateT (Array (Field StructInstView)) m Unit :=
     for field in struct.fields do
       if let .nested struct := field.val then
         go struct
@@ -904,7 +905,7 @@ where
         modify (·.push field)
 
 /-- Returns the name of the field. Assumes all fields under consideration are simple and named. -/
-def getFieldName (field : Field) : Name :=
+def getFieldName (field : Field StructInstView) : Name :=
   match field.lhs with
   | [.fieldName _ fieldName] => fieldName
   | _ => unreachable!

src/Lean/Elab/Structure.lean

@@ -4,15 +4,22 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Class
+import Lean.Parser.Command
+import Lean.Meta.Closure
+import Lean.Meta.SizeOf
+import Lean.Meta.Injective
 import Lean.Meta.Structure
-import Lean.Elab.MutualInductive
+import Lean.Meta.AppBuilder
+import Lean.Elab.Command
+import Lean.Elab.DeclModifiers
+import Lean.Elab.DeclUtil
+import Lean.Elab.Inductive
+import Lean.Elab.DeclarationRange
+import Lean.Elab.Binders
 
 namespace Lean.Elab.Command
 
-builtin_initialize
-  registerTraceClass `Elab.structure
-  registerTraceClass `Elab.structure.resolutionOrder
-
 register_builtin_option structureDiamondWarning : Bool := {
   defValue := false
   descr    := "if true, enable warnings when a structure has diamond inheritance"
@@ -32,6 +39,13 @@ leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder
 ```
 -/
 
+structure StructCtorView where
+  ref       : Syntax
+  modifiers : Modifiers
+  name      : Name
+  declName  : Name
+  deriving Inhabited
+
 structure StructFieldView where
   ref        : Syntax
   modifiers  : Modifiers
@@ -47,15 +61,22 @@ structure StructFieldView where
   type?      : Option Syntax
   value?     : Option Syntax
 
-structure StructView extends InductiveView where
-  parents         : Array Syntax
-  fields          : Array StructFieldView
+structure StructView where
+  ref             : Syntax
+  declId          : Syntax
+  modifiers       : Modifiers
+  isClass         : Bool -- struct-only
+  shortDeclName   : Name
+  declName        : Name
+  levelNames      : List Name
+  binders         : Syntax
+  type            : Syntax -- modified (inductive has type?)
+  parents         : Array Syntax -- struct-only
+  ctor            : StructCtorView -- struct-only
+  fields          : Array StructFieldView -- struct-only
+  derivingClasses : Array DerivingClassView
   deriving Inhabited
 
-def StructView.ctor : StructView → CtorView
-  | { ctors := #[ctor], ..} => ctor
-  | _ => unreachable!
-
 structure StructParentInfo where
   ref        : Syntax
   fvar?      : Option Expr
@@ -81,6 +102,18 @@ structure StructFieldInfo where
   value?   : Option Expr := none
   deriving Inhabited, Repr
 
+structure ElabStructHeaderResult where
+  view             : StructView
+  lctx             : LocalContext
+  localInsts       : LocalInstances
+  levelNames       : List Name
+  params           : Array Expr
+  type             : Expr
+  parents          : Array StructParentInfo
+  /-- Field infos from parents. -/
+  parentFieldInfos : Array StructFieldInfo
+  deriving Inhabited
+
 def StructFieldInfo.isFromParent (info : StructFieldInfo) : Bool :=
   match info.kind with
   | StructFieldKind.fromParent => true
@@ -97,12 +130,12 @@ The structure constructor syntax is
 leading_parser try (declModifiers >> ident >> " :: ")
 ```
 -/
-private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : TermElabM CtorView := do
+private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : TermElabM StructCtorView := do
   let useDefault := do
     let declName := structDeclName ++ defaultCtorName
     let ref := structStx[1].mkSynthetic
     addDeclarationRangesFromSyntax declName ref
-    pure { ref, declId := ref, modifiers := default, declName }
+    pure { ref, modifiers := default, name := defaultCtorName, declName }
   if structStx[5].isNone then
     useDefault
   else
@@ -123,7 +156,7 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc
       let declName ← applyVisibility ctorModifiers.visibility declName
       addDocString' declName ctorModifiers.docString?
       addDeclarationRangesFromSyntax declName ctor[1]
-      pure { ref := ctor[1], declId := ctor[1], modifiers := ctorModifiers, declName }
+      pure { ref := ctor[1], name, modifiers := ctorModifiers, declName }
 
 def checkValidFieldModifier (modifiers : Modifiers) : TermElabM Unit := do
   if modifiers.isNoncomputable then
@@ -238,7 +271,7 @@ def structureSyntaxToView (modifiers : Modifiers) (stx : Syntax) : TermElabM Str
   let parents   := if exts.isNone then #[] else exts[0][1].getSepArgs
   let optType   := stx[4]
   let derivingClasses ← getOptDerivingClasses stx[6]
-  let type?     := if optType.isNone then none else some optType[0][1]
+  let type      ← if optType.isNone then `(Sort _) else pure optType[0][1]
   let ctor ← expandCtor stx modifiers declName
   let fields ← expandFields stx modifiers declName
   fields.forM fun field => do
@@ -254,13 +287,10 @@ def structureSyntaxToView (modifiers : Modifiers) (stx : Syntax) : TermElabM Str
     declName
     levelNames
     binders
-    type?
-    allowIndices := false
-    allowSortPolymorphism := false
-    ctors := #[ctor]
+    type
     parents
+    ctor
     fields
-    computedFields := #[]
     derivingClasses
   }
 
@@ -506,7 +536,7 @@ private partial def mkToParentName (parentStructName : Name) (p : Name → Bool)
       if p curr then curr else go (i+1)
     go 1
 
-private partial def withParents (view : StructView) (rs : Array ElabHeaderResult) (indFVar : Expr)
+private partial def elabParents (view : StructView)
     (k : Array StructFieldInfo → Array StructParentInfo → TermElabM α) : TermElabM α := do
   go 0 #[] #[]
 where
@@ -514,17 +544,11 @@ where
     if h : i < view.parents.size then
       let parent := view.parents[i]
       withRef parent do
-      -- The only use case for autobound implicits for parents might be outParams, but outParam is not propagated.
-      let type ← Term.withoutAutoBoundImplicit <| Term.elabType parent
+      let type ← Term.elabType parent
       let parentType ← whnf type
-      if parentType.getAppFn == indFVar then
-        logWarning "structure extends itself, skipping"
-        return ← go (i + 1) infos parents
-      if rs.any (fun r => r.indFVar == parentType.getAppFn) then
-        throwError "structure cannot extend types defined in the same mutual block"
       let parentStructName ← getStructureName parentType
       if parents.any (fun info => info.structName == parentStructName) then
-        logWarning m!"duplicate parent structure '{.ofConstName parentStructName}', skipping"
+        logWarningAt parent m!"duplicate parent structure '{.ofConstName parentStructName}', skipping"
         go (i + 1) infos parents
       else if let some existingFieldName ← findExistingField? infos parentStructName then
         if structureDiamondWarning.get (← getOptions) then
@@ -546,13 +570,6 @@ where
     else
       k infos parents
 
-private def registerFailedToInferFieldType (fieldName : Name) (e : Expr) (ref : Syntax) : TermElabM Unit := do
-  Term.registerCustomErrorIfMVar (← instantiateMVars e) ref m!"failed to infer type of field '{.ofConstName fieldName}'"
-
-private def registerFailedToInferDefaultValue (fieldName : Name) (e : Expr) (ref : Syntax) : TermElabM Unit := do
-  Term.registerCustomErrorIfMVar (← instantiateMVars e) ref m!"failed to infer default value for field '{.ofConstName fieldName}'"
-  Term.registerLevelMVarErrorExprInfo e ref m!"failed to infer universe levels in default value for field '{.ofConstName fieldName}'"
-
 private def elabFieldTypeValue (view : StructFieldView) : TermElabM (Option Expr × Option Expr) :=
   Term.withAutoBoundImplicit <| Term.withAutoBoundImplicitForbiddenPred (fun n => view.name == n) <| Term.elabBinders view.binders.getArgs fun params => do
     match view.type? with
@@ -564,13 +581,10 @@ private def elabFieldTypeValue (view : StructFieldView) : TermElabM (Option Expr
         -- TODO: add forbidden predicate using `shortDeclName` from `view`
         let params ← Term.addAutoBoundImplicits params
         let value ← Term.withoutAutoBoundImplicit <| Term.elabTerm valStx none
-        registerFailedToInferFieldType view.name (← inferType value) view.nameId
-        registerFailedToInferDefaultValue view.name value valStx
         let value ← mkLambdaFVars params value
         return (none, value)
     | some typeStx =>
       let type ← Term.elabType typeStx
-      registerFailedToInferFieldType view.name type typeStx
       Term.synthesizeSyntheticMVarsNoPostponing
       let params ← Term.addAutoBoundImplicits params
       match view.value? with
@@ -579,7 +593,6 @@ private def elabFieldTypeValue (view : StructFieldView) : TermElabM (Option Expr
         return (type, none)
       | some valStx =>
         let value ← Term.withoutAutoBoundImplicit <| Term.elabTermEnsuringType valStx type
-        registerFailedToInferDefaultValue view.name value valStx
         Term.synthesizeSyntheticMVarsNoPostponing
         let type  ← mkForallFVars params type
         let value ← mkLambdaFVars params value
@@ -626,7 +639,6 @@ where
                 valStx ← `(fun $(view.binders.getArgs)* => $valStx:term)
               let fvarType ← inferType info.fvar
               let value ← Term.elabTermEnsuringType valStx fvarType
-              registerFailedToInferDefaultValue view.name value valStx
               pushInfoLeaf <| .ofFieldRedeclInfo { stx := view.ref }
               let infos := replaceFieldInfo infos { info with ref := view.nameId, value? := value }
               go (i+1) defaultValsOverridden infos
@@ -638,14 +650,113 @@ where
     else
       k infos
 
-private def collectUsedFVars (lctx : LocalContext) (localInsts : LocalInstances) (fieldInfos : Array StructFieldInfo) :
-    StateRefT CollectFVars.State MetaM Unit := do
-  withLCtx lctx localInsts do
-    fieldInfos.forM fun info => do
-      let fvarType ← inferType info.fvar
-      fvarType.collectFVars
-      if let some value := info.value? then
-        value.collectFVars
+private def getResultUniverse (type : Expr) : TermElabM Level := do
+  let type ← whnf type
+  match type with
+  | Expr.sort u => pure u
+  | _           => throwError "unexpected structure resulting type"
+
+private def collectUsed (params : Array Expr) (fieldInfos : Array StructFieldInfo) : StateRefT CollectFVars.State MetaM Unit := do
+  params.forM fun p => do
+    let type ← inferType p
+    type.collectFVars
+  fieldInfos.forM fun info => do
+    let fvarType ← inferType info.fvar
+    fvarType.collectFVars
+    match info.value? with
+    | none       => pure ()
+    | some value => value.collectFVars
+
+private def removeUnused (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo)
+    : TermElabM (LocalContext × LocalInstances × Array Expr) := do
+  let (_, used) ← (collectUsed params fieldInfos).run {}
+  Meta.removeUnused scopeVars used
+
+private def withUsed {α} (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo) (k : Array Expr → TermElabM α)
+    : TermElabM α := do
+  let (lctx, localInsts, vars) ← removeUnused scopeVars params fieldInfos
+  withLCtx lctx localInsts <| k vars
+
+private def levelMVarToParam (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo) (univToInfer? : Option LMVarId) : TermElabM (Array StructFieldInfo) := do
+  levelMVarToParamFVars scopeVars
+  levelMVarToParamFVars params
+  fieldInfos.mapM fun info => do
+    levelMVarToParamFVar info.fvar
+    match info.value? with
+    | none       => pure info
+    | some value =>
+      let value ← levelMVarToParam' value
+      pure { info with value? := value }
+where
+  levelMVarToParam' (type : Expr) : TermElabM Expr := do
+    Term.levelMVarToParam type (except := fun mvarId => univToInfer? == some mvarId)
+
+  levelMVarToParamFVars (fvars : Array Expr) : TermElabM Unit :=
+    fvars.forM levelMVarToParamFVar
+
+  levelMVarToParamFVar (fvar : Expr) : TermElabM Unit := do
+    let type ← inferType fvar
+    discard <| levelMVarToParam' type
+
+
+private partial def collectUniversesFromFields (r : Level) (rOffset : Nat) (fieldInfos : Array StructFieldInfo) : TermElabM (Array Level) := do
+  let (_, us) ← go |>.run #[]
+  return us
+where
+  go : StateRefT (Array Level) TermElabM Unit :=
+    for info in fieldInfos do
+      let type ← inferType info.fvar
+      let u ← getLevel type
+      let u ← instantiateLevelMVars u
+      match (← modifyGet fun s => accLevel u r rOffset |>.run |>.run s) with
+      | some _ => pure ()
+      | none =>
+        let typeType ← inferType type
+        let mut msg := m!"failed to compute resulting universe level of structure, field '{info.declName}' has type{indentD m!"{type} : {typeType}"}\nstructure resulting type{indentExpr (mkSort (r.addOffset rOffset))}"
+        if r.isMVar then
+          msg := msg ++ "\nrecall that Lean only infers the resulting universe level automatically when there is a unique solution for the universe level constraints, consider explicitly providing the structure resulting universe level"
+        throwError msg
+
+/--
+Decides whether the structure should be `Prop`-valued when the universe is not given
+and when the universe inference algorithm `collectUniversesFromFields` determines
+that the inductive type could naturally be `Prop`-valued.
+
+See `Lean.Elab.Command.isPropCandidate` for an explanation.
+Specialized to structures, the heuristic is that we prefer a `Prop` instead of a `Type` structure
+when it could be a syntactic subsingleton.
+Exception: no-field structures are `Type` since they are likely stubbed-out declarations.
+-/
+private def isPropCandidate (fieldInfos : Array StructFieldInfo) : Bool :=
+  !fieldInfos.isEmpty
+
+private def updateResultingUniverse (fieldInfos : Array StructFieldInfo) (type : Expr) : TermElabM Expr := do
+  let r ← getResultUniverse type
+  let rOffset : Nat   := r.getOffset
+  let r       : Level := r.getLevelOffset
+  unless r.isMVar do
+    throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly: {r}"
+  let us ← collectUniversesFromFields r rOffset fieldInfos
+  trace[Elab.structure] "updateResultingUniverse us: {us}, r: {r}, rOffset: {rOffset}"
+  let rNew := mkResultUniverse us rOffset (isPropCandidate fieldInfos)
+  assignLevelMVar r.mvarId! rNew
+  instantiateMVars type
+
+private def collectLevelParamsInFVar (s : CollectLevelParams.State) (fvar : Expr) : TermElabM CollectLevelParams.State := do
+  let type ← inferType fvar
+  let type ← instantiateMVars type
+  return collectLevelParams s type
+
+private def collectLevelParamsInFVars (fvars : Array Expr) (s : CollectLevelParams.State) : TermElabM CollectLevelParams.State :=
+  fvars.foldlM collectLevelParamsInFVar s
+
+private def collectLevelParamsInStructure (structType : Expr) (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo)
+    : TermElabM (Array Name) := do
+  let s := collectLevelParams {} structType
+  let s ← collectLevelParamsInFVars scopeVars s
+  let s ← collectLevelParamsInFVars params s
+  let s ← fieldInfos.foldlM (init := s) fun s info => collectLevelParamsInFVar s info.fvar
+  return s.params
 
 private def addCtorFields (fieldInfos : Array StructFieldInfo) : Nat → Expr → TermElabM Expr
   | 0,   type => pure type
@@ -661,29 +772,19 @@ private def addCtorFields (fieldInfos : Array StructFieldInfo) : Nat → Expr
     | _  =>
       addCtorFields fieldInfos i (mkForall decl.userName decl.binderInfo decl.type type)
 
-private def mkCtor (view : StructView) (r : ElabHeaderResult) (params : Array Expr) (fieldInfos : Array StructFieldInfo) : TermElabM Constructor :=
+private def mkCtor (view : StructView) (levelParams : List Name) (params : Array Expr) (fieldInfos : Array StructFieldInfo) : TermElabM Constructor :=
   withRef view.ref do
-  let type := mkAppN r.indFVar params
+  let type := mkAppN (mkConst view.declName (levelParams.map mkLevelParam)) params
   let type ← addCtorFields fieldInfos fieldInfos.size type
   let type ← mkForallFVars params type
   let type ← instantiateMVars type
   let type := type.inferImplicit params.size true
   pure { name := view.ctor.declName, type }
 
-private partial def checkResultingUniversesForFields (fieldInfos : Array StructFieldInfo) (u : Level) : TermElabM Unit := do
-  for info in fieldInfos do
-    let type ← inferType info.fvar
-    let v := (← instantiateLevelMVars (← getLevel type)).normalize
-    unless u.geq v do
-      let msg := m!"invalid universe level for field '{info.name}', has type{indentExpr type}\n\
-        at universe level{indentD v}\n\
-        which is not less than or equal to the structure's resulting universe level{indentD u}"
-      throwErrorAt info.ref msg
-
 @[extern "lean_mk_projections"]
 private opaque mkProjections (env : Environment) (structName : Name) (projs : List Name) (isClass : Bool) : Except KernelException Environment
 
-private def addProjections (r : ElabHeaderResult) (fieldInfos : Array StructFieldInfo) : TermElabM Unit := do
+private def addProjections (r : ElabStructHeaderResult) (fieldInfos : Array StructFieldInfo) : TermElabM Unit := do
   if r.type.isProp then
     if let some fieldInfo ← fieldInfos.findM? (not <$> Meta.isProof ·.fvar) then
       throwErrorAt fieldInfo.ref m!"failed to generate projections for 'Prop' structure, field '{format fieldInfo.name}' is not a proof"
@@ -694,71 +795,49 @@ private def addProjections (r : ElabHeaderResult) (fieldInfos : Array StructFiel
 
 private def registerStructure (structName : Name) (infos : Array StructFieldInfo) : TermElabM Unit := do
   let fields ← infos.filterMapM fun info => do
-    if info.kind == StructFieldKind.fromParent then
-      return none
-    else
-      return some {
-        fieldName  := info.name
-        projFn     := info.declName
-        binderInfo := (← getFVarLocalDecl info.fvar).binderInfo
-        autoParam? := (← inferType info.fvar).getAutoParamTactic?
-        subobject? := if let .subobject parentName := info.kind then parentName else none
-      }
+      if info.kind == StructFieldKind.fromParent then
+        return none
+      else
+        return some {
+          fieldName  := info.name
+          projFn     := info.declName
+          binderInfo := (← getFVarLocalDecl info.fvar).binderInfo
+          autoParam? := (← inferType info.fvar).getAutoParamTactic?
+          subobject? := if let .subobject parentName := info.kind then parentName else none
+        }
   modifyEnv fun env => Lean.registerStructure env { structName, fields }
 
-private def checkDefaults (fieldInfos : Array StructFieldInfo) : TermElabM Unit := do
-  let mut mvars := {}
-  let mut lmvars := {}
-  for fieldInfo in fieldInfos do
-    if let some value := fieldInfo.value? then
-      let value ← instantiateMVars value
-      mvars := Expr.collectMVars mvars value
-      lmvars := collectLevelMVars lmvars value
-  -- Log errors and ignore the failure; we later will just omit adding a default value.
-  if ← Term.logUnassignedUsingErrorInfos mvars.result then
-    return
-  else if ← Term.logUnassignedLevelMVarsUsingErrorInfos lmvars.result then
-    return
+private def mkAuxConstructions (declName : Name) : TermElabM Unit := do
+  let env ← getEnv
+  let hasEq   := env.contains ``Eq
+  let hasHEq  := env.contains ``HEq
+  let hasUnit := env.contains ``PUnit
+  let hasProd := env.contains ``Prod
+  mkRecOn declName
+  if hasUnit then mkCasesOn declName
+  if hasUnit && hasEq && hasHEq then mkNoConfusion declName
+  let ival ← getConstInfoInduct declName
+  if ival.isRec then
+    if hasUnit && hasProd then mkBelow declName
+    if hasUnit && hasProd then mkIBelow declName
+    if hasUnit && hasProd then mkBRecOn declName
+    if hasUnit && hasProd then mkBInductionOn declName
 
-private def addDefaults (params : Array Expr) (replaceIndFVars : Expr → MetaM Expr) (fieldInfos : Array StructFieldInfo) : TermElabM Unit := do
-  let lctx ← getLCtx
-  /- The `lctx` and `defaultAuxDecls` are used to create the auxiliary "default value" declarations
-    The parameters `params` for these definitions must be marked as implicit, and all others as explicit. -/
-  let lctx :=
-    params.foldl (init := lctx) fun (lctx : LocalContext) (p : Expr) =>
-      if p.isFVar then
-        lctx.setBinderInfo p.fvarId! BinderInfo.implicit
-      else
-        lctx
-  let lctx :=
-    fieldInfos.foldl (init := lctx) fun (lctx : LocalContext) (info : StructFieldInfo) =>
-      if info.isFromParent then lctx -- `fromParent` fields are elaborated as let-decls, and are zeta-expanded when creating "default value" auxiliary functions
-      else lctx.setBinderInfo info.fvar.fvarId! BinderInfo.default
-  -- Make all indFVar replacements in the local context.
-  let lctx ←
-    lctx.foldlM (init := {}) fun lctx ldecl => do
-     match ldecl with
-     | .cdecl _ fvarId userName type bi k =>
-       let type ← replaceIndFVars type
-       return lctx.mkLocalDecl fvarId userName type bi k
-     | .ldecl _ fvarId userName type value nonDep k =>
-       let type ← replaceIndFVars type
-       let value ← replaceIndFVars value
-       return lctx.mkLetDecl fvarId userName type value nonDep k
+private def addDefaults (lctx : LocalContext) (fieldInfos : Array StructFieldInfo) : TermElabM Unit := do
   withLCtx lctx (← getLocalInstances) do
     fieldInfos.forM fun fieldInfo => do
       if let some value := fieldInfo.value? then
         let declName := mkDefaultFnOfProjFn fieldInfo.declName
-        let type ← replaceIndFVars (← inferType fieldInfo.fvar)
-        let value ← instantiateMVars (← replaceIndFVars value)
-        trace[Elab.structure] "default value after 'replaceIndFVars': {indentExpr value}"
-        -- If there are mvars, `checkDefaults` already logged an error.
-        unless value.hasMVar || value.hasSyntheticSorry do
-          /- The identity function is used as "marker". -/
-          let value ← mkId value
-          -- No need to compile the definition, since it is only used during elaboration.
-          discard <| mkAuxDefinition declName type value (zetaDelta := true) (compile := false)
-          setReducibleAttribute declName
+        let type ← inferType fieldInfo.fvar
+        let value ← instantiateMVars value
+        if value.hasExprMVar then
+          discard <| Term.logUnassignedUsingErrorInfos (← getMVars value)
+          throwErrorAt fieldInfo.ref "invalid default value for field '{format fieldInfo.name}', it contains metavariables{indentExpr value}"
+        /- The identity function is used as "marker". -/
+        let value ← mkId value
+        -- No need to compile the definition, since it is only used during elaboration.
+        discard <| mkAuxDefinition declName type value (zetaDelta := true) (compile := false)
+        setReducibleAttribute declName
 
 /--
 Given `type` of the form `forall ... (source : A), B`, return `forall ... [source : A], B`.
@@ -827,6 +906,57 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
       setReducibleAttribute declName
     return { structName := parentStructName, subobject := false, projFn := declName }
 
+private def elabStructHeader (view : StructView) : TermElabM ElabStructHeaderResult :=
+  Term.withAutoBoundImplicitForbiddenPred (fun n => view.shortDeclName == n) do
+  Term.withAutoBoundImplicit do
+  Term.elabBinders view.binders.getArgs fun params => do
+  elabParents view fun parentFieldInfos parents => do
+    let type ← Term.elabType view.type
+    Term.synthesizeSyntheticMVarsNoPostponing
+    let u ← mkFreshLevelMVar
+    unless ← isDefEq type (mkSort u) do
+      throwErrorAt view.type "invalid structure type, expecting 'Type _' or 'Prop'"
+    let type ← instantiateMVars (← whnf type)
+    Term.addAutoBoundImplicits' params type fun params type => do
+      let levelNames ← Term.getLevelNames
+      trace[Elab.structure] "header params: {params}, type: {type}, levelNames: {levelNames}"
+      return { lctx := (← getLCtx), localInsts := (← getLocalInstances), levelNames, params, type, view, parents, parentFieldInfos }
+
+private def mkTypeFor (r : ElabStructHeaderResult) : TermElabM Expr := do
+  withLCtx r.lctx r.localInsts do
+    mkForallFVars r.params r.type
+
+/--
+Create a local declaration for the structure and execute `x params indFVar`, where `params` are the structure's type parameters and
+`indFVar` is the new local declaration.
+-/
+private partial def withStructureLocalDecl (r : ElabStructHeaderResult) (x : Array Expr → Expr → TermElabM α) : TermElabM α := do
+  let declName := r.view.declName
+  let shortDeclName := r.view.shortDeclName
+  let type ← mkTypeFor r
+  let params := r.params
+  withLCtx r.lctx r.localInsts <| withRef r.view.ref do
+    Term.withAuxDecl shortDeclName type declName fun indFVar =>
+      x params indFVar
+
+/--
+Remark: `numVars <= numParams`.
+`numVars` is the number of context `variables` used in the declaration,
+and `numParams - numVars` is the number of parameters provided as binders in the declaration.
+-/
+private def mkInductiveType (view : StructView) (indFVar : Expr) (levelNames : List Name)
+    (numVars : Nat) (numParams : Nat) (type : Expr) (ctor : Constructor) : TermElabM InductiveType := do
+  let levelParams := levelNames.map mkLevelParam
+  let const := mkConst view.declName levelParams
+  let ctorType ← forallBoundedTelescope ctor.type numParams fun params type => do
+    let type := type.replace fun e =>
+      if e == indFVar then
+        mkAppN const (params.extract 0 numVars)
+      else
+        none
+    instantiateMVars (← mkForallFVars params type)
+  return { name := view.declName, type := ← instantiateMVars type, ctors := [{ ctor with type := ← instantiateMVars ctorType }] }
+
 /--
 Precomputes the structure's resolution order.
 Option `structure.strictResolutionOrder` controls whether to create a warning if the C3 algorithm failed.
@@ -857,50 +987,109 @@ private def addParentInstances (parents : Array StructureParentInfo) : MetaM Uni
   for instParent in instParents do
     addInstance instParent.projFn AttributeKind.global (eval_prio default)
 
-@[builtin_inductive_elab Lean.Parser.Command.«structure»]
-def elabStructureCommand : InductiveElabDescr where
-  mkInductiveView (modifiers : Modifiers) (stx : Syntax) := do
+def mkStructureDecl (vars : Array Expr) (view : StructView) : TermElabM Unit := Term.withoutSavingRecAppSyntax do
+  let scopeLevelNames ← Term.getLevelNames
+  let isUnsafe := view.modifiers.isUnsafe
+  withRef view.ref <| Term.withLevelNames view.levelNames do
+    let r ← elabStructHeader view
+    Term.synthesizeSyntheticMVarsNoPostponing
+    withLCtx r.lctx r.localInsts do
+    withStructureLocalDecl r fun params indFVar => do
+    trace[Elab.structure] "indFVar: {indFVar}"
+    Term.addLocalVarInfo view.declId indFVar
+    withFields view.fields r.parentFieldInfos fun fieldInfos =>
+    withRef view.ref do
+      Term.synthesizeSyntheticMVarsNoPostponing
+      let type ← instantiateMVars r.type
+      let u ← getResultUniverse type
+      let univToInfer? ← shouldInferResultUniverse u
+      withUsed vars params fieldInfos fun scopeVars => do
+        let fieldInfos ← levelMVarToParam scopeVars params fieldInfos univToInfer?
+        let type ← withRef view.ref do
+          if univToInfer?.isSome then
+            updateResultingUniverse fieldInfos type
+          else
+            checkResultingUniverse (← getResultUniverse type)
+            pure type
+        trace[Elab.structure] "type: {type}"
+        let usedLevelNames ← collectLevelParamsInStructure type scopeVars params fieldInfos
+        match sortDeclLevelParams scopeLevelNames r.levelNames usedLevelNames with
+        | Except.error msg      => throwErrorAt view.declId msg
+        | Except.ok levelParams =>
+          let params := scopeVars ++ params
+          let ctor ← mkCtor view levelParams params fieldInfos
+          let type ← mkForallFVars params type
+          let type ← instantiateMVars type
+          let indType ← mkInductiveType view indFVar levelParams scopeVars.size params.size type ctor
+          let decl    := Declaration.inductDecl levelParams params.size [indType] isUnsafe
+          Term.ensureNoUnassignedMVars decl
+          addDecl decl
+          -- rename indFVar so that it does not shadow the actual declaration:
+          let lctx := (← getLCtx).modifyLocalDecl indFVar.fvarId! fun decl => decl.setUserName .anonymous
+          withLCtx lctx (← getLocalInstances) do
+          addProjections r fieldInfos
+          registerStructure view.declName fieldInfos
+          mkAuxConstructions view.declName
+          withSaveInfoContext do  -- save new env
+            Term.addLocalVarInfo view.ref[1] (← mkConstWithLevelParams view.declName)
+            if let some _ := view.ctor.ref.getPos? (canonicalOnly := true) then
+              Term.addTermInfo' view.ctor.ref (← mkConstWithLevelParams view.ctor.declName) (isBinder := true)
+            for field in view.fields do
+              -- may not exist if overriding inherited field
+              if (← getEnv).contains field.declName then
+                Term.addTermInfo' field.ref (← mkConstWithLevelParams field.declName) (isBinder := true)
+          withRef view.declId do
+            Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking
+          let parentInfos ← r.parents.mapM fun parent => do
+            if parent.subobject then
+              let some info := fieldInfos.find? (·.kind == .subobject parent.structName) | unreachable!
+              pure { structName := parent.structName, subobject := true, projFn := info.declName }
+            else
+              mkCoercionToCopiedParent levelParams params view parent.structName parent.type
+          setStructureParents view.declName parentInfos
+          checkResolutionOrder view.declName
+          if view.isClass then
+            addParentInstances parentInfos
+
+          let lctx ← getLCtx
+          /- The `lctx` and `defaultAuxDecls` are used to create the auxiliary "default value" declarations
+            The parameters `params` for these definitions must be marked as implicit, and all others as explicit. -/
+          let lctx :=
+            params.foldl (init := lctx) fun (lctx : LocalContext) (p : Expr) =>
+              if p.isFVar then
+                lctx.setBinderInfo p.fvarId! BinderInfo.implicit
+              else
+                lctx
+          let lctx :=
+            fieldInfos.foldl (init := lctx) fun (lctx : LocalContext) (info : StructFieldInfo) =>
+              if info.isFromParent then lctx -- `fromParent` fields are elaborated as let-decls, and are zeta-expanded when creating "default value" auxiliary functions
+              else lctx.setBinderInfo info.fvar.fvarId! BinderInfo.default
+          addDefaults lctx fieldInfos
+
+
+def elabStructureView (vars : Array Expr) (view : StructView) : TermElabM Unit := do
+  Term.withDeclName view.declName <| withRef view.ref do
+    mkStructureDecl vars view
+    unless view.isClass do
+      Lean.Meta.IndPredBelow.mkBelow view.declName
+      mkSizeOfInstances view.declName
+      mkInjectiveTheorems view.declName
+
+def elabStructureViewPostprocessing (view : StructView) : CommandElabM Unit := do
+  view.derivingClasses.forM fun classView => classView.applyHandlers #[view.declName]
+  runTermElabM fun _ => Term.withDeclName view.declName <| withRef view.declId do
+    Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation
+
+def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
+  let view ← runTermElabM fun vars => do
     let view ← structureSyntaxToView modifiers stx
     trace[Elab.structure] "view.levelNames: {view.levelNames}"
-    return {
-      view := view.toInductiveView
-      elabCtors := fun rs r params => do
-        withParents view rs r.indFVar fun parentFieldInfos parents =>
-        withFields view.fields parentFieldInfos fun fieldInfos => do
-        withRef view.ref do
-          Term.synthesizeSyntheticMVarsNoPostponing
-          let lctx ← getLCtx
-          let localInsts ← getLocalInstances
-          let ctor ← mkCtor view r params fieldInfos
-          return {
-            ctors := [ctor]
-            collectUsedFVars := collectUsedFVars lctx localInsts fieldInfos
-            checkUniverses := fun _ u => withLCtx lctx localInsts do checkResultingUniversesForFields fieldInfos u
-            finalizeTermElab := withLCtx lctx localInsts do checkDefaults fieldInfos
-            prefinalize := fun _ _ _ => do
-              withLCtx lctx localInsts do
-                addProjections r fieldInfos
-                registerStructure view.declName fieldInfos
-              withSaveInfoContext do  -- save new env
-                for field in view.fields do
-                  -- may not exist if overriding inherited field
-                  if (← getEnv).contains field.declName then
-                    Term.addTermInfo' field.ref (← mkConstWithLevelParams field.declName) (isBinder := true)
-            finalize := fun levelParams params replaceIndFVars => do
-              let parentInfos ← parents.mapM fun parent => do
-                if parent.subobject then
-                  let some info := fieldInfos.find? (·.kind == .subobject parent.structName) | unreachable!
-                  pure { structName := parent.structName, subobject := true, projFn := info.declName }
-                else
-                  mkCoercionToCopiedParent levelParams params view parent.structName parent.type
-              setStructureParents view.declName parentInfos
-              checkResolutionOrder view.declName
-              if view.isClass then
-                addParentInstances parentInfos
+    elabStructureView vars view
+    pure view
+  elabStructureViewPostprocessing view
 
-              withLCtx lctx localInsts do
-                addDefaults params replaceIndFVars fieldInfos
-          }
-    }
+builtin_initialize
+  registerTraceClass `Elab.structure
+  registerTraceClass `Elab.structure.resolutionOrder
 
 end Lean.Elab.Command

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean

@@ -58,28 +58,15 @@ where
     let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none
     let eqBV ← ReifiedBVLogical.ofPred eqBVPred
 
+    let trueExpr := mkConst ``Bool.true
+    let impExpr ← mkArrow (← mkEq eqDiscrExpr trueExpr) (← mkEq eqBVExpr trueExpr)
+    let decideImpExpr ← mkAppOptM ``Decidable.decide #[some impExpr, none]
     let imp ← ReifiedBVLogical.mkGate eqDiscr eqBV eqDiscrExpr eqBVExpr .imp
 
     let proof := do
       let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr
       let congrProof ← imp.evalsAtAtoms
       let lemmaProof := mkApp4 (mkConst lemmaName) (toExpr lhs.width) discrExpr lhsExpr rhsExpr
-
-      let trueExpr := mkConst ``Bool.true
-      let eqDiscrTrueExpr ← mkEq eqDiscrExpr trueExpr
-      let eqBVExprTrueExpr ← mkEq eqBVExpr trueExpr
-      let impExpr ← mkArrow eqDiscrTrueExpr eqBVExprTrueExpr
-      -- construct a `Decidable` instance for the implication using forall_prop_decidable
-      let decEqDiscrTrue := mkApp2 (mkConst ``instDecidableEqBool) eqDiscrExpr trueExpr
-      let decEqBVExprTrue := mkApp2 (mkConst ``instDecidableEqBool) eqBVExpr trueExpr
-      let impDecidable := mkApp4 (mkConst ``forall_prop_decidable)
-        eqDiscrTrueExpr
-        (.lam .anonymous eqDiscrTrueExpr eqBVExprTrueExpr .default)
-        decEqDiscrTrue
-        (.lam .anonymous eqDiscrTrueExpr decEqBVExprTrue .default)
-
-      let decideImpExpr := mkApp2 (mkConst ``Decidable.decide) impExpr impDecidable
-
       return mkApp4
         (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.lemma_congr)
         decideImpExpr

src/Lean/Elab/Tactic/Injection.lean

@@ -40,7 +40,7 @@ private def tryAssumption (mvarId : MVarId) : MetaM (List MVarId) := do
   let ids := stx[1].getArgs.toList.map getNameOfIdent'
   liftMetaTactic fun mvarId => do
     match (← Meta.injections mvarId ids) with
-    | .solved                      => checkUnusedIds `injections mvarId ids; return []
-    | .subgoal mvarId' unusedIds _ => checkUnusedIds `injections mvarId unusedIds; tryAssumption mvarId'
+    | .solved                    => checkUnusedIds `injections mvarId ids; return []
+    | .subgoal mvarId' unusedIds => checkUnusedIds `injections mvarId unusedIds; tryAssumption mvarId'
 
 end Lean.Elab.Tactic

src/Lean/Elab/Term.lean

@@ -473,26 +473,6 @@ def withoutTacticReuse [Monad m] [MonadWithReaderOf Context m] [MonadOptions m]
       return !cond }
   }) act
 
-@[inherit_doc Core.wrapAsync]
-def wrapAsync (act : Unit → TermElabM α) : TermElabM (EIO Exception α) := do
-  let ctx ← read
-  let st ← get
-  let metaCtx ← readThe Meta.Context
-  let metaSt ← getThe Meta.State
-  Core.wrapAsync fun _ =>
-    act () |>.run ctx |>.run' st |>.run' metaCtx metaSt
-
-@[inherit_doc Core.wrapAsyncAsSnapshot]
-def wrapAsyncAsSnapshot (act : Unit → TermElabM Unit)
-    (desc : String := by exact decl_name%.toString) :
-    TermElabM (BaseIO Language.SnapshotTree) := do
-  let ctx ← read
-  let st ← get
-  let metaCtx ← readThe Meta.Context
-  let metaSt ← getThe Meta.State
-  Core.wrapAsyncAsSnapshot (desc := desc) fun _ =>
-    act () |>.run ctx |>.run' st |>.run' metaCtx metaSt
-
 abbrev TermElabResult (α : Type) := EStateM.Result Exception SavedState α
 
 /--

src/Lean/Language/Basic.lean

@@ -10,8 +10,9 @@ Authors: Sebastian Ullrich
 
 prelude
 import Init.System.Promise
+import Lean.Message
 import Lean.Parser.Types
-import Lean.Util.Trace
+import Lean.Elab.InfoTree
 
 set_option linter.missingDocs true
 
@@ -197,13 +198,32 @@ def withAlwaysResolvedPromises [Monad m] [MonadLiftT BaseIO m] [MonadFinally m]
   for asynchronously collecting information about the entirety of snapshots in the language server.
   The involved tasks may form a DAG on the `Task` dependency level but this is not captured by this
   data structure. -/
-structure SnapshotTree where
-  /-- The immediately available element of the snapshot tree node. -/
-  element : Snapshot
-  /-- The asynchronously available children of the snapshot tree node. -/
-  children : Array (SnapshotTask SnapshotTree)
+inductive SnapshotTree where
+  /-- Creates a snapshot tree node. -/
+  | mk (element : Snapshot) (children : Array (SnapshotTask SnapshotTree))
 deriving Inhabited
 
+/-- The immediately available element of the snapshot tree node. -/
+abbrev SnapshotTree.element : SnapshotTree → Snapshot
+  | mk s _ => s
+/-- The asynchronously available children of the snapshot tree node. -/
+abbrev SnapshotTree.children : SnapshotTree → Array (SnapshotTask SnapshotTree)
+  | mk _ children => children
+
+/-- Produces trace of given snapshot tree, synchronously waiting on all children. -/
+partial def SnapshotTree.trace (s : SnapshotTree) : CoreM Unit :=
+  go none s
+where go range? s := do
+  let file ← getFileMap
+  let mut desc := f!"{s.element.desc}"
+  if let some range := range? then
+    desc := desc ++ f!"{file.toPosition range.start}-{file.toPosition range.stop} "
+  desc := desc ++ .prefixJoin "\n• " (← s.element.diagnostics.msgLog.toList.mapM (·.toString))
+  if let some t := s.element.infoTree? then
+    trace[Elab.info] (← t.format)
+  withTraceNode `Elab.snapshotTree (fun _ => pure desc) do
+    s.children.toList.forM fun c => go c.range? c.get
+
 /--
   Helper class for projecting a heterogeneous hierarchy of snapshot classes to a homogeneous
   representation. -/
@@ -288,14 +308,6 @@ def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options) (json := false
 def SnapshotTree.getAll (s : SnapshotTree) : Array Snapshot :=
   s.forM (m := StateM _) (fun s => modify (·.push s)) |>.run #[] |>.2
 
-/-- Returns a task that waits on all snapshots in the tree. -/
-def SnapshotTree.waitAll : SnapshotTree → BaseIO (Task Unit)
-  | mk _ children => go children.toList
-where
-  go : List (SnapshotTask SnapshotTree) → BaseIO (Task Unit)
-    | [] => return .pure ()
-    | t::ts => BaseIO.bindTask t.task fun _ => go ts
-
 /-- Context of an input processing invocation. -/
 structure ProcessingContext extends Parser.InputContext
 

src/Lean/Language/Lean.lean

@@ -10,7 +10,6 @@ Authors: Sebastian Ullrich
 
 prelude
 import Lean.Language.Basic
-import Lean.Language.Util
 import Lean.Language.Lean.Types
 import Lean.Parser.Module
 import Lean.Elab.Import
@@ -167,6 +166,13 @@ namespace Lean.Language.Lean
 open Lean.Elab Command
 open Lean.Parser
 
+/-- Option for capturing output to stderr during elaboration. -/
+register_builtin_option stderrAsMessages : Bool := {
+  defValue := true
+  group    := "server"
+  descr    := "(server) capture output to the Lean stderr channel (such as from `dbg_trace`) during elaboration of a command as a diagnostic message"
+}
+
 /-- Lean-specific processing context. -/
 structure LeanProcessingContext extends ProcessingContext where
   /-- Position of the first file difference if there was a previous invocation. -/
@@ -513,7 +519,6 @@ where
         diagnostics := .empty, stx := .missing, parserState
         elabSnap := .pure <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
         finishedSnap := .pure { diagnostics := .empty, cmdState }
-        reportSnap := default
         tacticCache := (← IO.mkRef {})
         nextCmdSnap? := none
       }
@@ -524,7 +529,6 @@ where
       -- definitely resolved in `doElab` task
       let elabPromise ← IO.Promise.new
       let finishedPromise ← IO.Promise.new
-      let reportPromise ← IO.Promise.new
       -- (Try to) use last line of command as range for final snapshot task. This ensures we do not
       -- retract the progress bar to a previous position in case the command support incremental
       -- reporting but has significant work after resolving its last incremental promise, such as
@@ -543,46 +547,22 @@ where
       let nextCmdSnap? := next?.map
         ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })
       let diagnostics ← Snapshot.Diagnostics.ofMessageLog msgLog
-      let (stx', parserState') := if minimalSnapshots && !Parser.isTerminalCommand stx then
-        (default, default)
+      if minimalSnapshots && !Parser.isTerminalCommand stx then
+        prom.resolve {
+          diagnostics, finishedSnap, tacticCache, nextCmdSnap?
+          stx := .missing
+          parserState := {}
+          elabSnap := { range? := stx.getRange?, task := elabPromise.result }
+        }
       else
-        (stx, parserState)
-      prom.resolve {
-        diagnostics, finishedSnap, tacticCache, nextCmdSnap?
-        stx := stx', parserState := parserState'
-        elabSnap := { range? := stx.getRange?, task := elabPromise.result }
-        reportSnap := { range? := endRange?, task := reportPromise.result }
-      }
+        prom.resolve {
+          diagnostics, stx, parserState, tacticCache, nextCmdSnap?
+          elabSnap := { range? := stx.getRange?, task := elabPromise.result }
+          finishedSnap
+        }
       let cmdState ← doElab stx cmdState beginPos
         { old? := old?.map fun old => ⟨old.stx, old.elabSnap⟩, new := elabPromise }
         finishedPromise tacticCache ctx
-      let traceTask ←
-        if (← isTracingEnabledForCore `Elab.snapshotTree cmdState.scopes.head!.opts) then
-          -- We want to trace all of `CommandParsedSnapshot` but `traceTask` is part of it, so let's
-          -- create a temporary snapshot tree containing all tasks but it
-          let snaps := #[
-            { range? := none, task := elabPromise.result.map (sync := true) toSnapshotTree },
-            { range? := none, task := finishedPromise.result.map (sync := true) toSnapshotTree }] ++
-            cmdState.snapshotTasks
-          let tree := SnapshotTree.mk { diagnostics := .empty } snaps
-          BaseIO.bindTask (← tree.waitAll) fun _ => do
-            let .ok (_, s) ← EIO.toBaseIO <| tree.trace |>.run
-              { ctx with options := cmdState.scopes.head!.opts } { env := cmdState.env }
-              | pure <| .pure <| .mk { diagnostics := .empty } #[]
-            let mut msgLog := MessageLog.empty
-            for trace in s.traceState.traces do
-              msgLog := msgLog.add {
-                fileName := ctx.fileName
-                severity := MessageSeverity.information
-                pos      := ctx.fileMap.toPosition beginPos
-                data     := trace.msg
-              }
-            return .pure <| .mk { diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog) } #[]
-        else
-          pure <| .pure <| .mk { diagnostics := .empty } #[]
-      reportPromise.resolve <|
-        .mk { diagnostics := .empty } <|
-          cmdState.snapshotTasks.push { range? := endRange?, task := traceTask }
       if let some next := next? then
         -- We're definitely off the fast-forwarding path now
         parseCmd none parserState cmdState next (sync := false) ctx
@@ -593,9 +573,7 @@ where
       LeanProcessingM Command.State := do
     let ctx ← read
     let scope := cmdState.scopes.head!
-    -- reset per-command state
-    let cmdStateRef ← IO.mkRef { cmdState with
-      messages := .empty, traceState := {}, snapshotTasks := #[] }
+    let cmdStateRef ← IO.mkRef { cmdState with messages := .empty, traceState := {} }
     /-
     The same snapshot may be executed by different tasks. So, to make sure `elabCommandTopLevel`
     has exclusive access to the cache, we create a fresh reference here. Before this change, the
@@ -610,8 +588,8 @@ where
       cancelTk?    := some ctx.newCancelTk
     }
     let (output, _) ←
-      IO.FS.withIsolatedStreams (isolateStderr := Core.stderrAsMessages.get scope.opts) do
-        EIO.toBaseIO do
+      IO.FS.withIsolatedStreams (isolateStderr := stderrAsMessages.get scope.opts) do
+        liftM (m := BaseIO) do
           withLoggingExceptions
             (getResetInfoTrees *> Elab.Command.elabCommandTopLevel stx)
             cmdCtx cmdStateRef

src/Lean/Language/Lean/Types.lean

@@ -46,8 +46,6 @@ structure CommandParsedSnapshot extends Snapshot where
   elabSnap : SnapshotTask DynamicSnapshot
   /-- State after processing is finished. -/
   finishedSnap : SnapshotTask CommandFinishedSnapshot
-  /-- Additional, untyped snapshots used for reporting, not reuse. -/
-  reportSnap : SnapshotTask SnapshotTree
   /-- Cache for `save`; to be replaced with incrementality. -/
   tacticCache : IO.Ref Tactic.Cache
   /-- Next command, unless this is a terminal command. -/
@@ -57,8 +55,7 @@ partial instance : ToSnapshotTree CommandParsedSnapshot where
   toSnapshotTree := go where
     go s := ⟨s.toSnapshot,
       #[s.elabSnap.map (sync := true) toSnapshotTree,
-        s.finishedSnap.map (sync := true) toSnapshotTree,
-        s.reportSnap] |>
+        s.finishedSnap.map (sync := true) toSnapshotTree] |>
         pushOpt (s.nextCmdSnap?.map (·.map (sync := true) go))⟩
 
 /-- State after successful importing. -/

src/Lean/Language/Util.lean

@@ -1,29 +0,0 @@
-/-
-Copyright (c) 2023 Lean FRO. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Additional snapshot functionality that needs further imports.
-
-Authors: Sebastian Ullrich
--/
-
-prelude
-import Lean.Language.Basic
-import Lean.CoreM
-import Lean.Elab.InfoTree
-
-namespace Lean.Language
-
-/-- Produces trace of given snapshot tree, synchronously waiting on all children. -/
-partial def SnapshotTree.trace (s : SnapshotTree) : CoreM Unit :=
-  go none s
-where go range? s := do
-  let file ← getFileMap
-  let mut desc := f!"{s.element.desc}"
-  if let some range := range? then
-    desc := desc ++ f!"{file.toPosition range.start}-{file.toPosition range.stop} "
-  desc := desc ++ .prefixJoin "\n• " (← s.element.diagnostics.msgLog.toList.mapM (·.toString))
-  if let some t := s.element.infoTree? then
-    trace[Elab.info] (← t.format)
-  withTraceNode `Elab.snapshotTree (fun _ => pure desc) do
-    s.children.toList.forM fun c => go c.range? c.get

src/Lean/LocalContext.lean

@@ -406,8 +406,8 @@ def isSubPrefixOf (lctx₁ lctx₂ : LocalContext) (exceptFVars : Array Expr :=
 
 @[inline] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=
   let b := b.abstract xs
-  xs.size.foldRev (init := b) fun i _ b =>
-    let x := xs[i]
+  xs.size.foldRev (init := b) fun i b =>
+    let x := xs[i]!
     match lctx.findFVar? x with
     | some (.cdecl _ _ n ty bi _)  =>
       let ty := ty.abstractRange i xs;
@@ -457,7 +457,7 @@ def sanitizeNames (lctx : LocalContext) : StateM NameSanitizerState LocalContext
   let st ← get
   if !getSanitizeNames st.options then pure lctx else
     StateT.run' (s := ({} : NameSet)) <|
-      lctx.decls.size.foldRevM (init := lctx) fun i _ lctx => do
+      lctx.decls.size.foldRevM (init := lctx) fun i lctx => do
         match lctx.decls[i]! with
         | none      => pure lctx
         | some decl =>

src/Lean/Meta/Basic.lean

@@ -825,7 +825,7 @@ def mkFreshExprMVarWithId (mvarId : MVarId) (type? : Option Expr := none) (kind
     mkFreshExprMVarWithIdCore mvarId type kind userName
 
 def mkFreshLevelMVars (num : Nat) : MetaM (List Level) :=
-  num.foldM (init := []) fun _ _ us =>
+  num.foldM (init := []) fun _ us =>
     return (← mkFreshLevelMVar)::us
 
 def mkFreshLevelMVarsFor (info : ConstantInfo) : MetaM (List Level) :=

src/Lean/Meta/Closure.lean

@@ -286,8 +286,8 @@ partial def process : ClosureM Unit := do
 @[inline] def mkBinding (isLambda : Bool) (decls : Array LocalDecl) (b : Expr) : Expr :=
   let xs := decls.map LocalDecl.toExpr
   let b  := b.abstract xs
-  decls.size.foldRev (init := b) fun i _ b =>
-    let decl := decls[i]
+  decls.size.foldRev (init := b) fun i b =>
+    let decl := decls[i]!
     match decl with
     | .cdecl _ _ n ty bi _ =>
       let ty := ty.abstractRange i xs

src/Lean/Meta/LazyDiscrTree.lean

@@ -566,9 +566,9 @@ Append results to array
 partial def appendResultsAux (mr : MatchResult α) (a : Array β) (f : Nat → α → β) : Array β :=
   let aa := mr.elts
   let n := aa.size
-  Nat.fold (n := n) (init := a) fun i _ r =>
+  Nat.fold (n := n) (init := a) fun i r =>
     let j := n-1-i
-    let b := aa[j]
+    let b := aa[j]!
     b.foldl (init := r) (· ++ ·.map (f j))
 
 partial def appendResults (mr : MatchResult α) (a : Array α) : Array α :=

src/Lean/Meta/Match/Match.lean

@@ -882,7 +882,7 @@ def mkMatcher (input : MkMatcherInput) (exceptionIfContainsSorry := false) : Met
       | none => pure ()
 
     trace[Meta.Match.debug] "matcher: {matcher}"
-    let unusedAltIdxs := lhss.length.fold (init := []) fun i _ r =>
+    let unusedAltIdxs := lhss.length.fold (init := []) fun i r =>
       if s.used.contains i then r else i::r
     return {
       matcher,

src/Lean/Meta/Match/MatchEqs.lean

@@ -222,16 +222,16 @@ private def contradiction (mvarId : MVarId) : MetaM Bool :=
   Auxiliary tactic that tries to replace as many variables as possible and then apply `contradiction`.
   We use it to discard redundant hypotheses.
 -/
-partial def trySubstVarsAndContradiction (mvarId : MVarId) (forbidden : FVarIdSet := {}) : MetaM Bool :=
+partial def trySubstVarsAndContradiction (mvarId : MVarId) : MetaM Bool :=
   commitWhen do
     let mvarId ← substVars mvarId
-    match (← injections mvarId (forbidden := forbidden)) with
+    match (← injections mvarId) with
     | .solved => return true -- closed goal
-    | .subgoal mvarId' _ forbidden =>
+    | .subgoal mvarId' _ =>
       if mvarId' == mvarId then
         contradiction mvarId
       else
-        trySubstVarsAndContradiction mvarId' forbidden
+        trySubstVarsAndContradiction mvarId'
 
 private def processNextEq : M Bool := do
   let s ← get
@@ -375,8 +375,7 @@ private partial def withSplitterAlts (altTypes : Array Expr) (f : Array Expr →
 inductive InjectionAnyResult where
   | solved
   | failed
-  /-- `fvarId` refers to the local declaration selected for the application of the `injection` tactic. -/
-  | subgoal (fvarId : FVarId) (mvarId : MVarId)
+  | subgoal (mvarId : MVarId)
 
 private def injectionAnyCandidate? (type : Expr) : MetaM (Option (Expr × Expr)) := do
   if let some (_, lhs, rhs) ← matchEq? type then
@@ -386,28 +385,21 @@ private def injectionAnyCandidate? (type : Expr) : MetaM (Option (Expr × Expr))
       return some (lhs, rhs)
   return none
 
-/--
-Try applying `injection` to a local declaration that is not in `forbidden`.
-
-We use `forbidden` because the `injection` tactic might fail to clear the variable if there are forward dependencies.
-See `proveSubgoalLoop` for additional details.
--/
-private def injectionAny (mvarId : MVarId) (forbidden : FVarIdSet := {}) : MetaM InjectionAnyResult := do
+private def injectionAny (mvarId : MVarId) : MetaM InjectionAnyResult := do
   mvarId.withContext do
     for localDecl in (← getLCtx) do
-      unless forbidden.contains localDecl.fvarId do
-        if let some (lhs, rhs) ← injectionAnyCandidate? localDecl.type then
-          unless (← isDefEq lhs rhs) do
-            let lhs ← whnf lhs
-            let rhs ← whnf rhs
-            unless lhs.isRawNatLit && rhs.isRawNatLit do
-              try
-                match (← injection mvarId localDecl.fvarId) with
-                | InjectionResult.solved  => return InjectionAnyResult.solved
-                | InjectionResult.subgoal mvarId .. => return InjectionAnyResult.subgoal localDecl.fvarId mvarId
-              catch ex =>
-                trace[Meta.Match.matchEqs] "injectionAnyFailed at {localDecl.userName}, error\n{ex.toMessageData}"
-                pure ()
+      if let some (lhs, rhs) ← injectionAnyCandidate? localDecl.type then
+        unless (← isDefEq lhs rhs) do
+          let lhs ← whnf lhs
+          let rhs ← whnf rhs
+          unless lhs.isRawNatLit && rhs.isRawNatLit do
+            try
+              match (← injection mvarId localDecl.fvarId) with
+              | InjectionResult.solved  => return InjectionAnyResult.solved
+              | InjectionResult.subgoal mvarId .. => return InjectionAnyResult.subgoal mvarId
+            catch ex =>
+              trace[Meta.Match.matchEqs] "injectionAnyFailed at {localDecl.userName}, error\n{ex.toMessageData}"
+              pure ()
     return InjectionAnyResult.failed
 
 
@@ -609,32 +601,27 @@ where
         let eNew := mkAppN eNew mvars
         return TransformStep.done eNew
 
-  /-
-  `forbidden` tracks variables that we have already applied `injection`.
-  Recall that the `injection` tactic may not be able to eliminate them when
-  they have forward dependencies.
-  -/
-  proveSubgoalLoop (mvarId : MVarId) (forbidden : FVarIdSet) : MetaM Unit := do
+  proveSubgoalLoop (mvarId : MVarId) : MetaM Unit := do
     trace[Meta.Match.matchEqs] "proveSubgoalLoop\n{mvarId}"
     if (← mvarId.contradictionQuick) then
       return ()
-    match (← injectionAny mvarId forbidden) with
-    | .solved => return ()
-    | .failed =>
+    match (← injectionAny mvarId) with
+    | InjectionAnyResult.solved => return ()
+    | InjectionAnyResult.failed =>
       let mvarId' ← substVars mvarId
       if mvarId' == mvarId then
         if (← mvarId.contradictionCore {}) then
           return ()
         throwError "failed to generate splitter for match auxiliary declaration '{matchDeclName}', unsolved subgoal:\n{MessageData.ofGoal mvarId}"
       else
-        proveSubgoalLoop mvarId' forbidden
-    | .subgoal fvarId mvarId => proveSubgoalLoop mvarId (forbidden.insert fvarId)
+        proveSubgoalLoop mvarId'
+    | InjectionAnyResult.subgoal mvarId => proveSubgoalLoop mvarId
 
   proveSubgoal (mvarId : MVarId) : MetaM Unit := do
     trace[Meta.Match.matchEqs] "subgoal {mkMVar mvarId}, {repr (← mvarId.getDecl).kind}, {← mvarId.isAssigned}\n{MessageData.ofGoal mvarId}"
     let (_, mvarId) ← mvarId.intros
     let mvarId ← mvarId.tryClearMany (alts.map (·.fvarId!))
-    proveSubgoalLoop mvarId {}
+    proveSubgoalLoop mvarId
 
 /--
   Create new alternatives (aka minor premises) by replacing `discrs` with `patterns` at `alts`.
@@ -659,7 +646,7 @@ where
 /--
   Create conditional equations and splitter for the given match auxiliary declaration. -/
 private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns := withLCtx {} {} do
-  withTraceNode `Meta.Match.matchEqs (fun _ => return m!"mkEquationsFor '{matchDeclName}'") do
+  trace[Meta.Match.matchEqs] "mkEquationsFor '{matchDeclName}'"
   withConfig (fun c => { c with etaStruct := .none }) do
   /-
   Remark: user have requested the `split` tactic to be available for writing code.

src/Lean/Meta/Match/MatcherApp/Transform.lean

@@ -59,9 +59,9 @@ def addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp :=
       -- This error can only happen if someone implemented a transformation that rewrites the motive created by `mkMatcher`.
       throwError "unexpected matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments"
     let eType ← inferType e
-    let eTypeAbst ← matcherApp.discrs.size.foldRevM (init := eType) fun i _ eTypeAbst => do
+    let eTypeAbst ← matcherApp.discrs.size.foldRevM (init := eType) fun i eTypeAbst => do
       let motiveArg := motiveArgs[i]!
-      let discr     := matcherApp.discrs[i]
+      let discr     := matcherApp.discrs[i]!
       let eTypeAbst ← kabstract eTypeAbst discr
       return eTypeAbst.instantiate1 motiveArg
     let motiveBody ← mkArrow eTypeAbst motiveBody
@@ -118,9 +118,9 @@ def refineThrough (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Expr) :=
       -- This error can only happen if someone implemented a transformation that rewrites the motive created by `mkMatcher`.
       throwError "failed to transfer argument through matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments"
 
-    let eAbst ← matcherApp.discrs.size.foldRevM (init := e) fun i _ eAbst => do
+    let eAbst ← matcherApp.discrs.size.foldRevM (init := e) fun i eAbst => do
       let motiveArg := motiveArgs[i]!
-      let discr     := matcherApp.discrs[i]
+      let discr     := matcherApp.discrs[i]!
       let eTypeAbst ← kabstract eAbst discr
       return eTypeAbst.instantiate1 motiveArg
     -- Let's create something that’s a `Sort` and mentions `e`

src/Lean/Meta/Tactic/Apply.lean

@@ -104,8 +104,8 @@ def appendParentTag (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Arr
     newMVars[0]!.mvarId!.setTag parentTag
   else
     unless parentTag.isAnonymous do
-      newMVars.size.forM fun i _ => do
-        let mvarIdNew := newMVars[i].mvarId!
+      newMVars.size.forM fun i => do
+        let mvarIdNew := newMVars[i]!.mvarId!
         unless (← mvarIdNew.isAssigned) do
           unless binderInfos[i]!.isInstImplicit do
             let currTag ← mvarIdNew.getTag

src/Lean/Meta/Tactic/Cases.lean

@@ -168,7 +168,7 @@ private def hasIndepIndices (ctx : Context) : MetaM Bool := do
   else if ctx.majorTypeIndices.any fun idx => !idx.isFVar then
     /- One of the indices is not a free variable. -/
     return false
-  else if ctx.majorTypeIndices.size.any fun i _ => i.any fun j _ => ctx.majorTypeIndices[i] == ctx.majorTypeIndices[j] then
+  else if ctx.majorTypeIndices.size.any fun i => i.any fun j => ctx.majorTypeIndices[i]! == ctx.majorTypeIndices[j]! then
     /- An index occurs more than once -/
     return false
   else

src/Lean/Meta/Tactic/FunInd.lean

@@ -283,9 +283,9 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
           (onMotive := fun xs _body => do
             -- Remove the old IH that was added in mkFix
             let eType ← newIH.getType
-            let eTypeAbst ← matcherApp.discrs.size.foldRevM (init := eType) fun i _ eTypeAbst => do
+            let eTypeAbst ← matcherApp.discrs.size.foldRevM (init := eType) fun i eTypeAbst => do
               let motiveArg := xs[i]!
-              let discr     := matcherApp.discrs[i]
+              let discr     := matcherApp.discrs[i]!
               let eTypeAbst ← kabstract eTypeAbst discr
               return eTypeAbst.instantiate1 motiveArg
 

src/Lean/Meta/Tactic/Induction.lean

@@ -105,10 +105,10 @@ private partial def finalize
             let mvarId' ← mvar.mvarId!.tryClear major.fvarId!
             let (fields, mvarId') ←  mvarId'.introN nparams minorGivenNames.varNames (useNamesForExplicitOnly := !minorGivenNames.explicit)
             let (extra,  mvarId') ← mvarId'.introNP nextra
-            let subst := reverted.size.fold (init := baseSubst) fun i _ (subst : FVarSubst) =>
+            let subst := reverted.size.fold (init := baseSubst) fun i (subst : FVarSubst) =>
               if i < indices.size + 1 then subst
               else
-                let revertedFVarId := reverted[i]
+                let revertedFVarId := reverted[i]!
                 let newFVarId      := extra[i - indices.size - 1]!
                 subst.insert revertedFVarId (mkFVar newFVarId)
             let fields := fields.map mkFVar
@@ -134,8 +134,8 @@ def getMajorTypeIndices (mvarId : MVarId) (tacticName : Name) (recursorInfo : Re
     if idxPos ≥ majorTypeArgs.size then throwTacticEx tacticName mvarId m!"major premise type is ill-formed{indentExpr majorType}"
     let idx := majorTypeArgs.get! idxPos
     unless idx.isFVar do throwTacticEx tacticName mvarId m!"major premise type index {idx} is not a variable{indentExpr majorType}"
-    majorTypeArgs.size.forM fun i _ => do
-      let arg := majorTypeArgs[i]
+    majorTypeArgs.size.forM fun i => do
+      let arg := majorTypeArgs[i]!
       if i != idxPos && arg == idx then
         throwTacticEx tacticName mvarId m!"'{idx}' is an index in major premise, but it occurs more than once{indentExpr majorType}"
       if i < idxPos then

src/Lean/Meta/Tactic/Injection.lean

@@ -94,48 +94,31 @@ def injection (mvarId : MVarId) (fvarId : FVarId) (newNames : List Name := []) :
   | .subgoal mvarId numEqs => injectionIntro mvarId numEqs newNames
 
 inductive InjectionsResult where
-  /-- `injections` closed the input goal. -/
   | solved
-  /--
-  `injections` produces a new goal `mvarId`. `remainingNames` contains the user-facing names that have not been used.
-  `forbidden` contains all local declarations to which `injection` has been applied.
-  Recall that some of these declarations may not have been eliminated from the local context due to forward dependencies, and
-  we use `forbidden` to avoid non-termination when using `injections` in a loop.
-  -/
-  | subgoal (mvarId : MVarId) (remainingNames : List Name) (forbidden : FVarIdSet)
+  | subgoal (mvarId : MVarId) (remainingNames : List Name)
 
-/--
-Applies `injection` to local declarations in `mvarId`. It uses `newNames` to name the new local declarations.
-`maxDepth` is the maximum recursion depth. Only local declarations that are not in `forbidden` are considered.
-Recall that some of local declarations may not have been eliminated from the local context due to forward dependencies, and
-we use `forbidden` to avoid non-termination when using `injections` in a loop.
--/
-partial def injections (mvarId : MVarId) (newNames : List Name := []) (maxDepth : Nat := 5) (forbidden : FVarIdSet := {}) : MetaM InjectionsResult :=
+partial def injections (mvarId : MVarId) (newNames : List Name := []) (maxDepth : Nat := 5) : MetaM InjectionsResult :=
   mvarId.withContext do
     let fvarIds := (← getLCtx).getFVarIds
-    go maxDepth fvarIds.toList mvarId newNames forbidden
+    go maxDepth fvarIds.toList mvarId newNames
 where
-  go (depth : Nat) (fvarIds : List FVarId) (mvarId : MVarId) (newNames : List Name) (forbidden : FVarIdSet) : MetaM InjectionsResult := do
-    match depth, fvarIds with
-    | 0,   _                 => throwTacticEx `injections mvarId "recursion depth exceeded"
-    | _,   []                => return .subgoal mvarId newNames forbidden
-    | d+1, fvarId :: fvarIds => do
+  go : Nat → List FVarId → MVarId → List Name → MetaM InjectionsResult
+    | 0,   _,  _,      _        => throwTacticEx `injections mvarId "recursion depth exceeded"
+    | _,   [], mvarId, newNames => return .subgoal mvarId newNames
+    | d+1, fvarId :: fvarIds, mvarId, newNames => do
       let cont := do
-        go (d+1) fvarIds mvarId newNames forbidden
-      if forbidden.contains fvarId then
-        cont
-      else if let some (_, lhs, rhs) ← matchEqHEq? (← fvarId.getType) then
+        go (d+1) fvarIds mvarId newNames
+      if let some (_, lhs, rhs) ← matchEqHEq? (← fvarId.getType) then
         let lhs ← whnf lhs
         let rhs ← whnf rhs
-        if lhs.isRawNatLit && rhs.isRawNatLit then
-          cont
+        if lhs.isRawNatLit && rhs.isRawNatLit then cont
         else
           try
             commitIfNoEx do
               match (← injection mvarId fvarId newNames) with
               | .solved  => return .solved
               | .subgoal mvarId newEqs remainingNames =>
-                mvarId.withContext <| go d (newEqs.toList ++ fvarIds) mvarId remainingNames (forbidden.insert fvarId)
+                mvarId.withContext <| go d (newEqs.toList ++ fvarIds) mvarId remainingNames
           catch _ => cont
       else cont
 

src/Lean/Meta/Tactic/Revert.lean

@@ -43,7 +43,6 @@ def _root_.Lean.MVarId.revert (mvarId : MVarId) (fvarIds : Array FVarId) (preser
       finally
         mvarId.setKind .syntheticOpaque
     let mvar := e.getAppFn
-    mvar.mvarId!.setKind .syntheticOpaque
     mvar.mvarId!.setTag tag
     return (toRevert.map Expr.fvarId!, mvar.mvarId!)
 

src/Lean/Meta/Tactic/Rewrite.lean

@@ -45,26 +45,12 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           let eNew ← instantiateMVars eNew
           let eType ← inferType e
           let motive := Lean.mkLambda `_a BinderInfo.default α eAbst
-          try
-            check motive
-          catch ex =>
-            throwTacticEx `rewrite mvarId m!"\
-              motive is not type correct:{indentD motive}\nError: {ex.toMessageData}\
-              \n\n\
-              Explanation: The rewrite tactic rewrites an expression 'e' using an equality 'a = b' by the following process. \
-              First, it looks for all 'a' in 'e'. Second, it tries to abstract these occurrences of 'a' to create a function 'm := fun _a => ...', called the *motive*, \
-              with the property that 'm a' is definitionally equal to 'e'. \
-              Third, we observe that '{.ofConstName ``congrArg}' implies that 'm a = m b', which can be used with lemmas such as '{.ofConstName ``Eq.mpr}' to change the goal. \
-              However, if 'e' depends on specific properties of 'a', then the motive 'm' might not typecheck.\
-              \n\n\
-              Possible solutions: use rewrite's 'occs' configuration option to limit which occurrences are rewritten, \
-              or use 'simp' or 'conv' mode, which have strategies for certain kinds of dependencies \
-              (these tactics can handle proofs and '{.ofConstName ``Decidable}' instances whose types depend on the rewritten term, \
-              and 'simp' can apply user-defined '@[congr]' theorems as well)."
+          unless (← isTypeCorrect motive) do
+            throwTacticEx `rewrite mvarId "motive is not type correct"
           unless (← withLocalDeclD `_a α fun a => do isDefEq (← inferType (eAbst.instantiate1 a)) eType) do
             -- NB: using motive.arrow? would disallow motives where the dependency
             -- can be reduced away
-            throwTacticEx `rewrite mvarId m!"motive is dependent{indentD motive}"
+            throwTacticEx `rewrite mvarId "motive is dependent"
           let u1 ← getLevel α
           let u2 ← getLevel eType
           let eqPrf := mkApp6 (.const ``congrArg [u1, u2]) α eType lhs rhs motive heq

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -146,8 +146,12 @@ def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) (
     indexConfig := mkIndexConfig config
   }
 
-def Context.setConfig (context : Context) (config : Config) : Context :=
-  { context with config }
+def Context.setConfig (context : Context) (config : Config) : MetaM Context := do
+  return { context with
+    config
+    metaConfig := (← mkMetaConfig config)
+    indexConfig := (← mkIndexConfig config)
+  }
 
 def Context.setSimpTheorems (c : Context) (simpTheorems : SimpTheoremsArray) : Context :=
   { c with simpTheorems }

src/Lean/Meta/Tactic/Subst.lean

@@ -80,9 +80,9 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
                   pure mvarId
                 let (newFVars, mvarId) ← mvarId.introNP (vars.size - 2)
                 trace[Meta.Tactic.subst] "after intro rest {vars.size - 2} {MessageData.ofGoal mvarId}"
-                let fvarSubst ← newFVars.size.foldM (init := fvarSubst) fun i _ (fvarSubst : FVarSubst) =>
+                let fvarSubst ← newFVars.size.foldM (init := fvarSubst) fun i (fvarSubst : FVarSubst) =>
                     let var     := vars[i+2]!
-                    let newFVar := newFVars[i]
+                    let newFVar := newFVars[i]!
                     pure $ fvarSubst.insert var (mkFVar newFVar)
                 let fvarSubst := fvarSubst.insert aFVarIdOriginal (if clearH then b else mkFVar aFVarId)
                 let fvarSubst := fvarSubst.insert hFVarIdOriginal (mkFVar hFVarId)

src/Lean/MetavarContext.lean

@@ -979,10 +979,10 @@ def collectForwardDeps (lctx : LocalContext) (toRevert : Array Expr) : M (Array
   else
     if (← preserveOrder) then
       -- Make sure toRevert[j] does not depend on toRevert[i] for j < i
-      toRevert.size.forM fun i _ => do
-        let fvar := toRevert[i]
-        i.forM fun j _ => do
-          let prevFVar := toRevert[j]
+      toRevert.size.forM fun i => do
+        let fvar := toRevert[i]!
+        i.forM fun j => do
+          let prevFVar := toRevert[j]!
           let prevDecl := lctx.getFVar! prevFVar
           if (← localDeclDependsOn prevDecl fvar.fvarId!) then
             throw (Exception.revertFailure (← getMCtx) lctx toRevert prevDecl.userName.toString)
@@ -990,7 +990,7 @@ def collectForwardDeps (lctx : LocalContext) (toRevert : Array Expr) : M (Array
     let firstDeclToVisit := getLocalDeclWithSmallestIdx lctx toRevert
     let initSize         := newToRevert.size
     lctx.foldlM (init := newToRevert) (start := firstDeclToVisit.index) fun (newToRevert : Array Expr) decl => do
-      if initSize.any fun i _ => decl.fvarId == newToRevert[i]!.fvarId! then
+      if initSize.any fun i => decl.fvarId == newToRevert[i]!.fvarId! then
         return newToRevert
       else if toRevert.any fun x => decl.fvarId == x.fvarId! then
         return newToRevert.push decl.toExpr
@@ -1061,8 +1061,8 @@ mutual
   -/
   private partial def mkAuxMVarType (lctx : LocalContext) (xs : Array Expr) (kind : MetavarKind) (e : Expr) (usedLetOnly : Bool) : M Expr := do
     let e ← abstractRangeAux xs xs.size e
-    xs.size.foldRevM (init := e) fun i _ e => do
-      let x := xs[i]
+    xs.size.foldRevM (init := e) fun i e => do
+      let x := xs[i]!
       if x.isFVar then
         match lctx.getFVar! x with
         | LocalDecl.cdecl _ _ n type bi _ =>
@@ -1231,8 +1231,8 @@ private def mkLambda' (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) (etaRed
   If `usedLetOnly == true` then `let` expressions are created only for used (let-) variables. -/
 def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (e : Expr) (usedOnly : Bool) (usedLetOnly : Bool) (etaReduce : Bool) : M Expr := do
   let e ← abstractRange xs xs.size e
-  xs.size.foldRevM (init := e) fun i _ e => do
-      let x := xs[i]
+  xs.size.foldRevM (init := e) fun i e => do
+      let x := xs[i]!
       if x.isFVar then
         match lctx.getFVar! x with
         | LocalDecl.cdecl _ _ n type bi _ =>

src/Lean/PrettyPrinter.lean

@@ -91,12 +91,9 @@ open Delaborator in
 /-- Pretty-prints a declaration `c` as `c.{<levels>} <params> : <type>`. -/
 def ppSignature (c : Name) : MetaM FormatWithInfos := do
   let decl ← getConstInfo c
-  let e := Expr.const c (decl.levelParams.map mkLevelParam)
-  if pp.raw.get (← getOptions) then
-    return s!"{e} : {decl.type}"
-  else
-    let (stx, infos) ← delabCore e (delab := delabConstWithSignature)
-    return ⟨← ppTerm ⟨stx⟩, infos⟩  -- HACK: not a term
+  let e := .const c (decl.levelParams.map mkLevelParam)
+  let (stx, infos) ← delabCore e (delab := delabConstWithSignature)
+  return ⟨← ppTerm ⟨stx⟩, infos⟩  -- HACK: not a term
 
 private partial def noContext : MessageData → MessageData
   | MessageData.withContext _   msg => noContext msg

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1115,18 +1115,17 @@ def coeDelaborator : Delab := whenPPOption getPPCoercions do
     delabAppCore nargs (delabHead info nargs) (unexpand := false)
 where
   delabHead (info : CoeFnInfo) (nargs : Nat) (insertExplicit : Bool) : Delab := do
-    withTypeAscription (cond := ← getPPOption getPPCoercionsTypes) 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))
+    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))
 
 @[builtin_delab app.dite]
 def delabDIte : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 5 do

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -44,11 +44,6 @@ register_builtin_option pp.coercions : Bool := {
   group    := "pp"
   descr    := "(pretty printer) hide coercion applications"
 }
-register_builtin_option pp.coercions.types : Bool := {
-  defValue := false
-  group    := "pp"
-  descr    := "(pretty printer) display coercion applications with a type ascription"
-}
 register_builtin_option pp.universes : Bool := {
   defValue := false
   group    := "pp"
@@ -256,7 +251,6 @@ def getPPLetVarTypes (o : Options) : Bool := o.get pp.letVarTypes.name (getPPAll
 def getPPNumericTypes (o : Options) : Bool := o.get pp.numericTypes.name pp.numericTypes.defValue
 def getPPNatLit (o : Options) : Bool := o.get pp.natLit.name (getPPNumericTypes o && !getPPAll o)
 def getPPCoercions (o : Options) : Bool := o.get pp.coercions.name (!getPPAll o)
-def getPPCoercionsTypes (o : Options) : Bool := o.get pp.coercions.types.name pp.coercions.types.defValue
 def getPPExplicit (o : Options) : Bool := o.get pp.explicit.name (getPPAll o)
 def getPPNotation (o : Options) : Bool := o.get pp.notation.name (!getPPAll o)
 def getPPParens (o : Options) : Bool := o.get pp.parens.name pp.parens.defValue

src/Lean/PrettyPrinter/Formatter.lean

@@ -467,7 +467,7 @@ def visitAtom (k : SyntaxNodeKind) : Formatter := do
 @[combinator_formatter manyNoAntiquot]
 def manyNoAntiquot.formatter (p : Formatter) : Formatter := do
   let stx ← getCur
-  visitArgs $ stx.getArgs.size.forM fun _ _ => p
+  visitArgs $ stx.getArgs.size.forM fun _ => p
 
 @[combinator_formatter many1NoAntiquot] def many1NoAntiquot.formatter (p : Formatter) : Formatter := manyNoAntiquot.formatter p
 
@@ -487,7 +487,7 @@ def many1Unbox.formatter (p : Formatter) : Formatter := do
 @[combinator_formatter sepByNoAntiquot]
 def sepByNoAntiquot.formatter (p pSep : Formatter) : Formatter := do
   let stx ← getCur
-  visitArgs <| stx.getArgs.size.forRevM fun i _ => if i % 2 == 0 then p else pSep
+  visitArgs <| stx.getArgs.size.forRevM fun i => if i % 2 == 0 then p else pSep
 
 @[combinator_formatter sepBy1NoAntiquot] def sepBy1NoAntiquot.formatter := sepByNoAntiquot.formatter
 

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -268,7 +268,7 @@ def visitToken : Parenthesizer := do
   let stx ← getCur
   -- `orelse` may produce `choice` nodes for antiquotations
   if stx.getKind == `choice then
-    visitArgs $ stx.getArgs.size.forM fun _ _ => do
+    visitArgs $ stx.getArgs.size.forM fun _ => do
       orelse.parenthesizer p1 p2
   else
     -- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try
@@ -332,7 +332,7 @@ partial def parenthesizeCategoryCore (cat : Name) (_prec : Nat) : Parenthesizer
   withReader (fun ctx => { ctx with cat := cat }) do
     let stx ← getCur
     if stx.getKind == `choice then
-      visitArgs $ stx.getArgs.size.forM fun _ _ => do
+      visitArgs $ stx.getArgs.size.forM fun _ => do
         parenthesizeCategoryCore cat _prec
     else
       withAntiquot.parenthesizer (mkAntiquot.parenthesizer' cat.toString cat (isPseudoKind := true)) (parenthesizerForKind stx.getKind)
@@ -470,7 +470,7 @@ def trailingNode.parenthesizer (k : SyntaxNodeKind) (prec lhsPrec : Nat) (p : Pa
 @[combinator_parenthesizer manyNoAntiquot]
 def manyNoAntiquot.parenthesizer (p : Parenthesizer) : Parenthesizer := do
   let stx ← getCur
-  visitArgs $ stx.getArgs.size.forM fun _ _ => p
+  visitArgs $ stx.getArgs.size.forM fun _ => p
 
 @[combinator_parenthesizer many1NoAntiquot]
 def many1NoAntiquot.parenthesizer (p : Parenthesizer) : Parenthesizer := do

src/Lean/Util/Trace.lean

@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Leonardo de Moura
 -/
 prelude
-import Lean.Elab.Exception
-import Lean.Log
+import Lean.Exception
 
 /-!
 # Trace messages
@@ -102,12 +101,9 @@ where
     else
       false
 
-def isTracingEnabledForCore (cls : Name) (opts : Options) : BaseIO Bool := do
-  let inherited ← inheritedTraceOptions.get
-  return checkTraceOption inherited opts cls
-
 def isTracingEnabledFor (cls : Name) : m Bool := do
-  (isTracingEnabledForCore cls (← getOptions) : IO _)
+  let inherited ← (inheritedTraceOptions.get : IO _)
+  pure (checkTraceOption inherited (← getOptions) cls)
 
 @[inline] def getTraces : m (PersistentArray TraceElem) := do
   let s ← getTraceState
@@ -361,23 +357,4 @@ def withTraceNodeBefore [MonadRef m] [AddMessageContext m] [MonadOptions m]
   addTraceNode oldTraces data ref msg
   MonadExcept.ofExcept res
 
-def addTraceAsMessages [Monad m] [MonadRef m] [MonadLog m] [MonadTrace m] : m Unit := do
-  if trace.profiler.output.get? (← getOptions) |>.isSome then
-    -- do not add trace messages if `trace.profiler.output` is set as it would be redundant and
-    -- pretty printing the trace messages is expensive
-    return
-  let traces ← getResetTraces
-  if traces.isEmpty then
-    return
-  let mut pos2traces : Std.HashMap (String.Pos × String.Pos) (Array MessageData) := ∅
-  for traceElem in traces do
-    let ref := replaceRef traceElem.ref (← getRef)
-    let pos := ref.getPos?.getD 0
-    let endPos := ref.getTailPos?.getD pos
-    pos2traces := pos2traces.insert (pos, endPos) <| pos2traces.getD (pos, endPos) #[] |>.push traceElem.msg
-  let traces' := pos2traces.toArray.qsort fun ((a, _), _) ((b, _), _) => a < b
-  for ((pos, endPos), traceMsg) in traces' do
-    let data := .tagged `trace <| .joinSep traceMsg.toList "\n"
-    logMessage <| Elab.mkMessageCore (← getFileName) (← getFileMap) data .information pos endPos
-
 end Lean

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

@@ -481,7 +481,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
           exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
         rcases hf with hf | hf
         · apply Or.inl
-          simp only [Array.set!, Array.setIfInBounds]
+          simp only [Array.set!, Array.setD]
           split
           · rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩
             simp only [← hidx, Array.toList_set]
@@ -514,7 +514,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
           exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
         rcases hf with hf | hf
         · apply Or.inl
-          simp only [Array.set!, Array.setIfInBounds]
+          simp only [Array.set!, Array.setD]
           split
           · rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩
             simp only [← hidx, Array.toList_set]
@@ -574,7 +574,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
           exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
         rcases hf with hf | hf
         · apply Or.inl
-          simp only [Array.set!, Array.setIfInBounds]
+          simp only [Array.set!, Array.setD]
           split
           · rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩
             simp only [← hidx, Array.toList_set]
@@ -644,7 +644,7 @@ theorem deleteOne_subset (f : DefaultFormula n) (id : Nat) (c : DefaultClause n)
     · apply Or.inl
       simp only [List.mem_filterMap, id_eq, exists_eq_right] at h1
       simp only [List.mem_filterMap, id_eq, exists_eq_right]
-      rw [Array.set!, Array.setIfInBounds] at h1
+      rw [Array.set!, Array.setD] at h1
       split at h1
       · simp only [Array.toList_set] at h1
         rcases List.getElem_of_mem h1 with ⟨i, h, h4⟩

src/runtime/io.cpp

@@ -1140,7 +1140,6 @@ extern "C" LEAN_EXPORT obj_res lean_io_create_tempfile(lean_object * /* w */) {
     strcat(path, file_pattern);
 
     uv_fs_t req;
-    // Differences from lean_io_create_tempdir start here
     ret = uv_fs_mkstemp(NULL, &req, path, NULL);
     if (ret < 0) {
         // If mkstemp throws an error we cannot rely on path to contain a proper file name.
@@ -1152,48 +1151,6 @@ extern "C" LEAN_EXPORT obj_res lean_io_create_tempfile(lean_object * /* w */) {
     }
 }
 
-/* createTempDir : IO FilePath */
-extern "C" LEAN_EXPORT obj_res lean_io_create_tempdir(lean_object * /* w */) {
-    char path[PATH_MAX];
-    size_t base_len = PATH_MAX;
-    int ret = uv_os_tmpdir(path, &base_len);
-    if (ret < 0) {
-        return io_result_mk_error(decode_uv_error(ret, nullptr));
-    } else if (base_len == 0) {
-        return lean_io_result_mk_error(decode_uv_error(UV_ENOENT, mk_string("")));
-    }
-
-#if defined(LEAN_WINDOWS)
-    // On Windows `GetTempPathW` always returns a path ending in \, but libuv removes it.
-    // https://learn.microsoft.com/en-us/windows/win32/fileio/creating-and-using-a-temporary-file
-    if (path[base_len - 1] != '\\') {
-        lean_always_assert(PATH_MAX >= base_len + 1 + 1);
-        strcat(path, "\\");
-    }
-#else
-    // No guarantee that we have a trailing / in TMPDIR.
-    if (path[base_len - 1] != '/') {
-        lean_always_assert(PATH_MAX >= base_len + 1 + 1);
-        strcat(path, "/");
-    }
-#endif
-
-    const char* file_pattern = "tmp.XXXXXXXX";
-    const size_t file_pattern_size = strlen(file_pattern);
-    lean_always_assert(PATH_MAX >= strlen(path) + file_pattern_size + 1);
-    strcat(path, file_pattern);
-
-    uv_fs_t req;
-    // Differences from lean_io_create_tempfile start here
-    ret = uv_fs_mkdtemp(NULL, &req, path, NULL);
-    if (ret < 0) {
-        // If mkdtemp throws an error we cannot rely on path to contain a proper file name.
-        return io_result_mk_error(decode_uv_error(ret, nullptr));
-    } else {
-        return lean_io_result_mk_ok(mk_string(req.path));
-    }
-}
-
 extern "C" LEAN_EXPORT obj_res lean_io_remove_file(b_obj_arg fname, obj_arg) {
     if (std::remove(string_cstr(fname)) == 0) {
         return io_result_mk_ok(box(0));

src/runtime/stackinfo.cpp

@@ -73,23 +73,6 @@ size_t get_stack_size(bool main) {
 }
 #endif
 
-#ifndef __has_builtin
-#define __has_builtin(x) 0 /* for non-clang compilers */
-#endif
-
-// taken from https://github.com/llvm/llvm-project/blob/llvmorg-10.0.0-rc1/clang/lib/Basic/Stack.cpp#L24
-static void *get_stack_pointer() {
-#if __GNUC__ || __has_builtin(__builtin_frame_address)
-    return __builtin_frame_address(0);
-#elif defined(_MSC_VER)
-    return _AddressOfReturnAddress();
-#else
-    char x = 0;
-    char *volatile ptr = &x;
-    return ptr;
-#endif
-}
-
 LEAN_THREAD_VALUE(bool, g_stack_info_init, false);
 LEAN_THREAD_VALUE(size_t, g_stack_size, 0);
 LEAN_THREAD_VALUE(size_t, g_stack_base, 0);
@@ -98,7 +81,8 @@ LEAN_THREAD_VALUE(size_t, g_stack_threshold, 0);
 void save_stack_info(bool main) {
     g_stack_info_init = true;
     g_stack_size = get_stack_size(main);
-    g_stack_base = reinterpret_cast<size_t>(get_stack_pointer());
+    char x;
+    g_stack_base = reinterpret_cast<size_t>(&x);
     /* g_stack_threshold is a redundant value used to optimize check_stack */
     g_stack_threshold = g_stack_base + LEAN_STACK_BUFFER_SPACE - g_stack_size;
     if (g_stack_threshold > g_stack_base + LEAN_STACK_BUFFER_SPACE) {
@@ -108,7 +92,8 @@ void save_stack_info(bool main) {
 }
 
 size_t get_used_stack_size() {
-    size_t curr_stack = reinterpret_cast<size_t>(get_stack_pointer());
+    char y;
+    size_t curr_stack = reinterpret_cast<size_t>(&y);
     return g_stack_base - curr_stack;
 }
 
@@ -128,7 +113,8 @@ void throw_stack_space_exception(char const * component_name) {
 void check_stack(char const * component_name) {
     if (!g_stack_info_init)
         save_stack_info(false);
-    size_t curr_stack = reinterpret_cast<size_t>(get_stack_pointer());
+    char y;
+    size_t curr_stack = reinterpret_cast<size_t>(&y);
     if (curr_stack < g_stack_threshold)
         throw_stack_space_exception(component_name);
 }