fix: add workaround for MessageData limitations

This PR adds a workaround for the discrepancy between Terminal/Emacs and VS Code when displaying info trees.

src/CMakeLists.txt

@@ -699,12 +699,12 @@ else()
 endif()
 
 if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  add_custom_target(lake_lib
+  add_custom_target(lake_lib ALL
     WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
     DEPENDS leanshared
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Lake
     VERBATIM)
-  add_custom_target(lake_shared
+  add_custom_target(lake_shared ALL
     WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
     DEPENDS lake_lib
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make libLake_shared

src/Init/Data/Array/Basic.lean

@@ -455,7 +455,7 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
 /-- Variant of `mapIdxM` which receives the index as a `Fin as.size`. -/
 @[inline]
 def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
-    (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → m β) : m (Array β) :=
+    (as : Array α) (f : Fin as.size → α → m β) : m (Array β) :=
   let rec @[specialize] map (i : Nat) (j : Nat) (inv : i + j = as.size) (bs : Array β) : m (Array β) := do
     match i, inv with
     | 0,    _  => pure bs
@@ -464,12 +464,12 @@ def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
         rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_comm]
         apply Nat.le_add_right
       have : i + (j + 1) = as.size := by rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
-      map i (j+1) this (bs.push (← f j (as.get j j_lt) j_lt))
+      map i (j+1) this (bs.push (← f ⟨j, j_lt⟩ (as.get j j_lt)))
   map as.size 0 rfl (mkEmpty as.size)
 
 @[inline]
 def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (as : Array α) : m (Array β) :=
-  as.mapFinIdxM fun i a _ => f i a
+  as.mapFinIdxM fun i a => f i a
 
 @[inline]
 def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β) := do
@@ -588,7 +588,7 @@ def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β :
 
 /-- Variant of `mapIdx` which receives the index as a `Fin as.size`. -/
 @[inline]
-def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → β) : Array β :=
+def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → α → β) : Array β :=
   Id.run <| as.mapFinIdxM f
 
 @[inline]

src/Init/Data/Array/Lemmas.lean

@@ -1379,6 +1379,8 @@ theorem filter_eq_push_iff {p : α → Bool} {l l' : Array α} {a : α} :
   · rintro ⟨⟨l₁⟩, ⟨l₂⟩, h₁, h₂, h₃, h₄⟩
     refine ⟨l₂.reverse, l₁.reverse, by simp_all⟩
 
+@[deprecated filter_map (since := "2024-06-15")] abbrev map_filter := @filter_map
+
 theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l :=
   (mem_filter.mp h).1
 
@@ -2267,7 +2269,7 @@ theorem flatMap_mkArray {β} (f : α → Array β) : (mkArray n a).flatMap f = (
   rw [← toList_inj]
   simp [flatMap_toList, List.flatMap_replicate]
 
-@[simp] theorem isEmpty_mkArray : (mkArray n a).isEmpty = decide (n = 0) := by
+@[simp] theorem isEmpty_replicate : (mkArray n a).isEmpty = decide (n = 0) := by
   rw [← List.toArray_replicate, List.isEmpty_toArray]
   simp
 
@@ -2275,168 +2277,6 @@ theorem flatMap_mkArray {β} (f : α → Array β) : (mkArray n a).flatMap f = (
   rw [← List.toArray_replicate, List.sum_toArray]
   simp
 
-/-! ### Preliminaries about `swap` needed for `reverse`. -/
-
-theorem swap_def (a : Array α) (i j : Nat) (hi hj) :
-    a.swap i j hi hj = (a.set i a[j]).set j a[i] (by simpa using hj) := by
-  simp [swap]
-
-theorem getElem?_swap (a : Array α) (i j : Nat) (hi hj) (k : Nat) : (a.swap i j hi hj)[k]? =
-    if j = k then some a[i] else if i = k then some a[j] else a[k]? := by
-  simp [swap_def, getElem?_set]
-
-/-! ### reverse -/
-
-@[simp] theorem size_reverse (a : Array α) : a.reverse.size = a.size := by
-  let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by
-    rw [reverse.loop]
-    if h : i < j then
-      simp [(go · (i+1) ⟨j-1, ·⟩), h]
-    else simp [h]
-    termination_by j - i
-  simp only [reverse]; split <;> simp [go]
-
-@[simp] theorem toList_reverse (a : Array α) : a.reverse.toList = a.toList.reverse := by
-  let rec go (as : Array α) (i j hj)
-      (h : i + j + 1 = a.size) (h₂ : as.size = a.size)
-      (H : ∀ k, as.toList[k]? = if i ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?)
-      (k : Nat) : (reverse.loop as i ⟨j, hj⟩).toList[k]? = a.toList.reverse[k]? := by
-    rw [reverse.loop]; dsimp only; split <;> rename_i h₁
-    · match j with | j+1 => ?_
-      simp only [Nat.add_sub_cancel]
-      rw [(go · (i+1) j)]
-      · rwa [Nat.add_right_comm i]
-      · simp [size_swap, h₂]
-      · intro k
-        rw [getElem?_toList, getElem?_swap]
-        simp only [H, ← getElem_toList, ← List.getElem?_eq_getElem, Nat.le_of_lt h₁,
-          ← getElem?_toList]
-        split <;> rename_i h₂
-        · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
-          exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
-        split <;> rename_i h₃
-        · simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and]
-          exact (List.getElem?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
-        simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
-          Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
-    · rw [H]; split <;> rename_i h₂
-      · cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2)
-        cases Nat.le_antisymm h₂.1 h₂.2
-        exact (List.getElem?_reverse' _ _ h).symm
-      · rfl
-    termination_by j - i
-  simp only [reverse]
-  split
-  · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl
-  · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›)
-    refine List.ext_getElem? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
-    split
-    · rfl
-    · rename_i h
-      simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this, Nat.zero_le,
-        true_and, Nat.not_lt] at h
-      rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]
-
-@[simp] theorem _root_.List.reverse_toArray (l : List α) : l.toArray.reverse = l.reverse.toArray := by
-  apply ext'
-  simp only [toList_reverse]
-
-@[simp] theorem reverse_push (as : Array α) (a : α) : (as.push a).reverse = #[a] ++ as.reverse := by
-  cases as
-  simp
-
-@[simp] theorem mem_reverse {x : α} {as : Array α} : x ∈ as.reverse ↔ x ∈ as := by
-  cases as
-  simp
-
-@[simp] theorem getElem_reverse (as : Array α) (i : Nat) (hi : i < as.reverse.size) :
-    (as.reverse)[i] = as[as.size - 1 - i]'(by simp at hi; omega) := by
-  cases as
-  simp
-
-@[simp] theorem reverse_eq_empty_iff {xs : Array α} : xs.reverse = #[] ↔ xs = #[] := by
-  cases xs
-  simp
-
-theorem reverse_ne_empty_iff {xs : Array α} : xs.reverse ≠ #[] ↔ xs ≠ #[] :=
-  not_congr reverse_eq_empty_iff
-
-/-- Variant of `getElem?_reverse` with a hypothesis giving the linear relation between the indices. -/
-theorem getElem?_reverse' {l : Array α} (i j) (h : i + j + 1 = l.size) : l.reverse[i]? = l[j]? := by
-  rcases l with ⟨l⟩
-  simp at h
-  simp only [List.reverse_toArray, List.getElem?_toArray]
-  rw [List.getElem?_reverse' (l := l) _ _ h]
-
-@[simp]
-theorem getElem?_reverse {l : Array α} {i} (h : i < l.size) :
-    l.reverse[i]? = l[l.size - 1 - i]? := by
-  cases l
-  simp_all
-
-@[simp] theorem reverse_reverse (as : Array α) : as.reverse.reverse = as := by
-  cases as
-  simp
-
-theorem reverse_eq_iff {as bs : Array α} : as.reverse = bs ↔ as = bs.reverse := by
-  constructor <;> (rintro rfl; simp)
-
-@[simp] theorem reverse_inj {xs ys : Array α} : xs.reverse = ys.reverse ↔ xs = ys := by
-  simp [reverse_eq_iff]
-
-@[simp] theorem reverse_eq_push_iff {xs : Array α} {ys : Array α} {a : α} :
-    xs.reverse = ys.push a ↔ xs = #[a] ++ ys.reverse := by
-  rw [reverse_eq_iff, reverse_push]
-
-@[simp] theorem map_reverse (f : α → β) (l : Array α) : l.reverse.map f = (l.map f).reverse := by
-  cases l <;> simp [*]
-
-@[simp] theorem filter_reverse (p : α → Bool) (l : Array α) : (l.reverse.filter p) = (l.filter p).reverse := by
-  cases l
-  simp
-
-@[simp] theorem filterMap_reverse (f : α → Option β) (l : Array α) : (l.reverse.filterMap f) = (l.filterMap f).reverse := by
-  cases l
-  simp
-
-@[simp] theorem reverse_append (as bs : Array α) : (as ++ bs).reverse = bs.reverse ++ as.reverse := by
-  cases as
-  cases bs
-  simp
-
-@[simp] theorem reverse_eq_append_iff {xs ys zs : Array α} :
-    xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse := by
-  cases xs
-  cases ys
-  cases zs
-  simp
-
-/-- Reversing a flatten is the same as reversing the order of parts and reversing all parts. -/
-theorem reverse_flatten (L : Array (Array α)) :
-    L.flatten.reverse = (L.map reverse).reverse.flatten := by
-  cases L using array₂_induction
-  simp [flatten_toArray, List.reverse_flatten, Function.comp_def]
-
-/-- Flattening a reverse is the same as reversing all parts and reversing the flattened result. -/
-theorem flatten_reverse (L : Array (Array α)) :
-    L.reverse.flatten = (L.map reverse).flatten.reverse := by
-  cases L using array₂_induction
-  simp [flatten_toArray, List.flatten_reverse, Function.comp_def]
-
-theorem reverse_flatMap {β} (l : Array α) (f : α → Array β) :
-    (l.flatMap f).reverse = l.reverse.flatMap (reverse ∘ f) := by
-  cases l
-  simp [List.reverse_flatMap, Function.comp_def]
-
-theorem flatMap_reverse {β} (l : Array α) (f : α → Array β) :
-    (l.reverse.flatMap f) = (l.flatMap (reverse ∘ f)).reverse := by
-  cases l
-  simp [List.flatMap_reverse, Function.comp_def]
-
-@[simp] theorem reverse_mkArray (n) (a : α) : reverse (mkArray n a) = mkArray n a := by
-  rw [← toList_inj]
-  simp
-
 /-! Content below this point has not yet been aligned with `List`. -/
 
 /-! ### sum -/
@@ -2628,7 +2468,6 @@ theorem getElem?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x
 
 @[deprecated getElem?_size (since := "2024-10-21")] abbrev get?_size := @getElem?_size
 
-@[deprecated getElem_set_self (since := "2025-01-17")]
 theorem get_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
     (a.set i v h)[i]'(by simp [h]) = v := by
   simp only [set, ← getElem_toList, List.getElem_set_self]
@@ -2652,9 +2491,17 @@ 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_toList, List.getElem_set_ne h]
 
+theorem swap_def (a : Array α) (i j : Nat) (hi hj) :
+    a.swap i j hi hj = (a.set i a[j]).set j a[i] (by simpa using hj) := by
+  simp [swap]
+
 @[simp] theorem toList_swap (a : Array α) (i j : Nat) (hi hj) :
     (a.swap i j hi hj).toList = (a.toList.set i a[j]).set j a[i] := by simp [swap_def]
 
+theorem getElem?_swap (a : Array α) (i j : Nat) (hi hj) (k : Nat) : (a.swap i j hi hj)[k]? =
+    if j = k then some a[i] else if i = k then some a[j] else a[k]? := by
+  simp [swap_def, get?_set]
+
 @[simp] theorem swapAt_def (a : Array α) (i : Nat) (v : α) (hi) :
     a.swapAt i v hi = (a[i], a.set i v) := rfl
 
@@ -2708,6 +2555,15 @@ theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rf
 
 @[deprecated size_swapIfInBounds (since := "2024-11-24")] abbrev size_swap! := @size_swapIfInBounds
 
+@[simp] theorem size_reverse (a : Array α) : a.reverse.size = a.size := by
+  let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by
+    rw [reverse.loop]
+    if h : i < j then
+      simp [(go · (i+1) ⟨j-1, ·⟩), h]
+    else simp [h]
+    termination_by j - i
+  simp only [reverse]; split <;> simp [go]
+
 @[simp] theorem size_range {n : Nat} : (range n).size = n := by
   induction n <;> simp [range]
 
@@ -2718,6 +2574,61 @@ theorem size_eq_length_toList (as : Array α) : as.size = as.toList.length := rf
 theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Array.range n)[x] = x := by
   simp [← getElem_toList]
 
+@[simp] theorem toList_reverse (a : Array α) : a.reverse.toList = a.toList.reverse := by
+  let rec go (as : Array α) (i j hj)
+      (h : i + j + 1 = a.size) (h₂ : as.size = a.size)
+      (H : ∀ k, as.toList[k]? = if i ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?)
+      (k : Nat) : (reverse.loop as i ⟨j, hj⟩).toList[k]? = a.toList.reverse[k]? := by
+    rw [reverse.loop]; dsimp only; split <;> rename_i h₁
+    · match j with | j+1 => ?_
+      simp only [Nat.add_sub_cancel]
+      rw [(go · (i+1) j)]
+      · rwa [Nat.add_right_comm i]
+      · simp [size_swap, h₂]
+      · intro k
+        rw [getElem?_toList, getElem?_swap]
+        simp only [H, ← getElem_toList, ← List.getElem?_eq_getElem, Nat.le_of_lt h₁,
+          ← getElem?_toList]
+        split <;> rename_i h₂
+        · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
+          exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
+        split <;> rename_i h₃
+        · simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and]
+          exact (List.getElem?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
+        simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
+          Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
+    · rw [H]; split <;> rename_i h₂
+      · cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2)
+        cases Nat.le_antisymm h₂.1 h₂.2
+        exact (List.getElem?_reverse' _ _ h).symm
+      · rfl
+    termination_by j - i
+  simp only [reverse]
+  split
+  · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl
+  · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›)
+    refine List.ext_getElem? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
+    split
+    · rfl
+    · rename_i h
+      simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this, Nat.zero_le,
+        true_and, Nat.not_lt] at h
+      rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]
+
+end Array
+
+open Array
+
+namespace List
+
+@[simp] theorem reverse_toArray (l : List α) : l.toArray.reverse = l.reverse.toArray := by
+  apply ext'
+  simp only [toList_reverse]
+
+end List
+
+namespace Array
+
 /-! ### foldlM and foldrM -/
 
 theorem foldlM_append [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l l' : Array α) :
@@ -3413,6 +3324,17 @@ theorem foldr_map' (g : α → β) (f : α → α → α) (f' : β → β → β
   | nil => simp
   | cons xs xss ih => simp [ih]
 
+/-! ### reverse -/
+
+@[simp] theorem mem_reverse {x : α} {as : Array α} : x ∈ as.reverse ↔ x ∈ as := by
+  cases as
+  simp
+
+@[simp] theorem getElem_reverse (as : Array α) (i : Nat) (hi : i < as.reverse.size) :
+    (as.reverse)[i] = as[as.size - 1 - i]'(by simp at hi; omega) := by
+  cases as
+  simp [Array.getElem_reverse]
+
 /-! ### findSomeRevM?, findRevM?, findSomeRev?, findRev? -/
 
 @[simp] theorem findSomeRevM?_eq_findSomeM?_reverse

src/Init/Data/Array/MapIdx.lean

@@ -12,82 +12,81 @@ namespace Array
 /-! ### mapFinIdx -/
 
 -- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
-theorem mapFinIdx_induction (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → β)
+theorem mapFinIdx_induction (as : Array α) (f : Fin as.size → α → β)
     (motive : Nat → Prop) (h0 : motive 0)
-    (p : (i : Nat) → β → (h : i < as.size) → Prop)
-    (hs : ∀ i h, motive i → p i (f i as[i] h) h ∧ motive (i + 1)) :
+    (p : Fin as.size → β → Prop)
+    (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
     motive as.size ∧ ∃ eq : (Array.mapFinIdx as f).size = as.size,
-      ∀ i h, p i ((Array.mapFinIdx as f)[i]) h := by
-  let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p i bs[i] h) (hm : motive j) :
+      ∀ i h, p ⟨i, h⟩ ((Array.mapFinIdx as f)[i]) := by
+  let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) :
     let arr : Array β := Array.mapFinIdxM.map (m := Id) as f i j h bs
-    motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p i arr[i] h := by
+    motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i] := by
     induction i generalizing j bs with simp [mapFinIdxM.map]
     | zero =>
       have := (Nat.zero_add _).symm.trans h
       exact ⟨this ▸ hm, h₁ ▸ this, fun _ _ => h₂ ..⟩
     | succ i ih =>
-      apply @ih (bs.push (f j as[j] (by omega))) (j + 1) (by omega) (by simp; omega)
+      apply @ih (bs.push (f ⟨j, by omega⟩ as[j])) (j + 1) (by omega) (by simp; omega)
       · intro i i_lt h'
         rw [getElem_push]
         split
         · apply h₂
         · simp only [size_push] at h'
           obtain rfl : i = j := by omega
-          apply (hs i (by omega) hm).1
-      · exact (hs j (by omega) hm).2
+          apply (hs ⟨i, by omega⟩ hm).1
+      · exact (hs ⟨j, by omega⟩ hm).2
   simp [mapFinIdx, mapFinIdxM]; exact go rfl nofun h0
 
-theorem mapFinIdx_spec (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → β)
-    (p : (i : Nat) → β → (h : i < as.size) → Prop) (hs : ∀ i h, p i (f i as[i] h) h) :
+theorem mapFinIdx_spec (as : Array α) (f : Fin as.size → α → β)
+    (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
     ∃ eq : (Array.mapFinIdx as f).size = as.size,
-      ∀ i h, p i ((Array.mapFinIdx as f)[i]) h :=
-  (mapFinIdx_induction _ _ (fun _ => True) trivial p fun _ _ _ => ⟨hs .., trivial⟩).2
+      ∀ i h, p ⟨i, h⟩ ((Array.mapFinIdx as f)[i]) :=
+  (mapFinIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
 
-@[simp] theorem size_mapFinIdx (a : Array α) (f : (i : Nat) → α → (h : i < a.size) → β) :
-    (a.mapFinIdx f).size = a.size :=
-  (mapFinIdx_spec (p := fun _ _ _ => True) (hs := fun _ _ => trivial)).1
+@[simp] theorem size_mapFinIdx (a : Array α) (f : Fin a.size → α → β) : (a.mapFinIdx f).size = a.size :=
+  (mapFinIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
 
 @[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
   Array.size_mapFinIdx _ _
 
-@[simp] theorem getElem_mapFinIdx (a : Array α) (f : (i : Nat) → α → (h : i < a.size) → β) (i : Nat)
+@[simp] theorem getElem_mapFinIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
     (h : i < (mapFinIdx a f).size) :
-    (a.mapFinIdx f)[i] = f i (a[i]'(by simp_all))  (by simp_all) :=
-  (mapFinIdx_spec _ _ (fun i b h => b = f i a[i] h) fun _ _ => rfl).2 i _
+    (a.mapFinIdx f)[i] = f ⟨i, by simp_all⟩ (a[i]'(by simp_all)) :=
+  (mapFinIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
 
-@[simp] theorem getElem?_mapFinIdx (a : Array α) (f : (i : Nat) → α → (h : i < a.size) → β) (i : Nat) :
+@[simp] theorem getElem?_mapFinIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) :
     (a.mapFinIdx f)[i]? =
-      a[i]?.pbind fun b h => f i b (getElem?_eq_some_iff.1 h).1 := by
+      a[i]?.pbind fun b h => f ⟨i, (getElem?_eq_some_iff.1 h).1⟩ b := by
   simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx]
   split <;> simp_all
 
-@[simp] theorem toList_mapFinIdx (a : Array α) (f : (i : Nat) → α → (h : i < a.size) → β) :
-    (a.mapFinIdx f).toList = a.toList.mapFinIdx (fun i a h => f i a (by simpa)) := by
+@[simp] theorem toList_mapFinIdx (a : Array α) (f : Fin a.size → α → β) :
+    (a.mapFinIdx f).toList = a.toList.mapFinIdx (fun i a => f ⟨i, by simp⟩ a) := by
   apply List.ext_getElem <;> simp
 
 /-! ### mapIdx -/
 
 theorem mapIdx_induction (f : Nat → α → β) (as : Array α)
     (motive : Nat → Prop) (h0 : motive 0)
-    (p : (i : Nat) → β → (h : i < as.size) → Prop)
-    (hs : ∀ i h, motive i → p i (f i as[i]) h ∧ motive (i + 1)) :
+    (p : Fin as.size → β → Prop)
+    (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
     motive as.size ∧ ∃ eq : (as.mapIdx f).size = as.size,
-      ∀ i h, p i ((as.mapIdx f)[i]) h :=
-  mapFinIdx_induction as (fun i a _ => f i a) motive h0 p hs
+      ∀ i h, p ⟨i, h⟩ ((as.mapIdx f)[i]) :=
+  mapFinIdx_induction as (fun i a => f i a) motive h0 p hs
 
 theorem mapIdx_spec (f : Nat → α → β) (as : Array α)
-    (p : (i : Nat) → β → (h : i < as.size) → Prop) (hs : ∀ i h, p i (f i as[i]) h) :
+    (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
     ∃ eq : (as.mapIdx f).size = as.size,
-      ∀ i h, p i ((as.mapIdx f)[i]) h :=
-  (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ _ => ⟨hs .., trivial⟩).2
+      ∀ i h, p ⟨i, h⟩ ((as.mapIdx f)[i]) :=
+  (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
 
 @[simp] theorem size_mapIdx (f : Nat → α → β) (as : Array α) : (as.mapIdx f).size = as.size :=
-  (mapIdx_spec (p := fun _ _ _ => True) (hs := fun _ _ => trivial)).1
+  (mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
 
 @[simp] theorem getElem_mapIdx (f : Nat → α → β) (as : Array α) (i : Nat)
     (h : i < (as.mapIdx f).size) :
     (as.mapIdx f)[i] = f i (as[i]'(by simp_all)) :=
-  (mapIdx_spec _ _ (fun i b h => b = f i as[i]) fun _ _ => rfl).2 i (by simp_all)
+  (mapIdx_spec _ _ (fun i b => b = f i as[i]) fun _ => rfl).2 i (by simp_all)
 
 @[simp] theorem getElem?_mapIdx (f : Nat → α → β) (as : Array α) (i : Nat) :
     (as.mapIdx f)[i]? =
@@ -102,7 +101,7 @@ end Array
 
 namespace List
 
-@[simp] theorem mapFinIdx_toArray (l : List α) (f : (i : Nat) → α → (h : i < l.length) → β) :
+@[simp] theorem mapFinIdx_toArray (l : List α) (f : Fin l.length → α → β) :
     l.toArray.mapFinIdx f = (l.mapFinIdx f).toArray := by
   ext <;> simp
 

src/Init/Data/BitVec/Lemmas.lean

@@ -1294,6 +1294,11 @@ theorem allOnes_shiftLeft_or_shiftLeft {x : BitVec w} {n : Nat} :
     BitVec.allOnes w <<< n ||| x <<< n = BitVec.allOnes w <<< n := by
   simp [← shiftLeft_or_distrib]
 
+@[deprecated shiftLeft_add (since := "2024-06-02")]
+theorem shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) :
+    (x <<< n) <<< m = x <<< (n + m) := by
+  rw [shiftLeft_add]
+
 /-! ### shiftLeft reductions from BitVec to Nat -/
 
 @[simp]
@@ -1941,6 +1946,11 @@ theorem msb_shiftLeft {x : BitVec w} {n : Nat} :
     (x <<< n).msb = x.getMsbD n := by
   simp [BitVec.msb]
 
+@[deprecated shiftRight_add (since := "2024-06-02")]
+theorem shiftRight_shiftRight {w : Nat} (x : BitVec w) (n m : Nat) :
+    (x >>> n) >>> m = x >>> (n + m) := by
+  rw [shiftRight_add]
+
 /-! ### rev -/
 
 theorem getLsbD_rev (x : BitVec w) (i : Fin w) :

src/Init/Data/Char/Lemmas.lean

@@ -70,3 +70,5 @@ theorem utf8Size_eq (c : Char) : c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Siz
   rfl
 
 end Char
+
+@[deprecated Char.utf8Size (since := "2024-06-04")] abbrev String.csize := Char.utf8Size

src/Init/Data/List/Basic.lean

@@ -258,6 +258,9 @@ theorem ext_get? : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n)
     have h0 : some a = some a' := h 0
     injection h0 with aa; simp only [aa, ext_get? fun n => h (n+1)]
 
+/-- Deprecated alias for `ext_get?`. The preferred extensionality theorem is now `ext_getElem?`. -/
+@[deprecated ext_get? (since := "2024-06-07")] abbrev ext := @ext_get?
+
 /-! ### getD -/
 
 /--
@@ -616,6 +619,11 @@ set_option linter.missingDocs false in
 set_option linter.missingDocs false in
 @[deprecated flatMap_cons (since := "2024-10-16")] abbrev cons_flatMap := @flatMap_cons
 
+set_option linter.missingDocs false in
+@[deprecated flatMap_nil (since := "2024-06-15")] abbrev nil_bind := @flatMap_nil
+set_option linter.missingDocs false in
+@[deprecated flatMap_cons (since := "2024-06-15")] abbrev cons_bind := @flatMap_cons
+
 /-! ### replicate -/
 
 /--
@@ -705,6 +713,11 @@ def elem [BEq α] (a : α) : List α → Bool
 theorem elem_cons [BEq α] {a : α} :
     (b::bs).elem a = match a == b with | true => true | false => bs.elem a := rfl
 
+/-- `notElem a l` is `!(elem a l)`. -/
+@[deprecated "Use `!(elem a l)` instead."(since := "2024-06-15")]
+def notElem [BEq α] (a : α) (as : List α) : Bool :=
+  !(as.elem a)
+
 /-! ### contains -/
 
 @[inherit_doc elem] abbrev contains [BEq α] (as : List α) (a : α) : Bool :=

src/Init/Data/List/Lemmas.lean

@@ -813,6 +813,11 @@ theorem getElem_cons_length (x : α) (xs : List α) (i : Nat) (h : i = xs.length
     (x :: xs)[i]'(by simp [h]) = (x :: xs).getLast (cons_ne_nil x xs) := by
   rw [getLast_eq_getElem]; cases h; rfl
 
+@[deprecated getElem_cons_length (since := "2024-06-12")]
+theorem get_cons_length (x : α) (xs : List α) (n : Nat) (h : n = xs.length) :
+    (x :: xs).get ⟨n, by simp [h]⟩ = (x :: xs).getLast (cons_ne_nil x xs) := by
+  simp [getElem_cons_length, h]
+
 /-! ### getLast? -/
 
 @[simp] theorem getLast?_singleton (a : α) : getLast? [a] = a := rfl
@@ -1021,10 +1026,21 @@ theorem getLast?_tail (l : List α) : (tail l).getLast? = if l.length = 1 then n
   | _ :: _, 0 => by simp
   | _ :: l, i+1 => by simp [getElem?_map f l i]
 
+@[deprecated getElem?_map (since := "2024-06-12")]
+theorem get?_map (f : α → β) : ∀ l i, (map f l).get? i = (l.get? i).map f
+  | [], _ => rfl
+  | _ :: _, 0 => rfl
+  | _ :: l, i+1 => get?_map f l i
+
 @[simp] theorem getElem_map (f : α → β) {l} {i : Nat} {h : i < (map f l).length} :
     (map f l)[i] = f (l[i]'(length_map l f ▸ h)) :=
   Option.some.inj <| by rw [← getElem?_eq_getElem, getElem?_map, getElem?_eq_getElem]; rfl
 
+@[deprecated getElem_map (since := "2024-06-12")]
+theorem get_map (f : α → β) {l i} :
+    get (map f l) i = f (get l ⟨i, length_map l f ▸ i.2⟩) := by
+  simp
+
 @[simp] theorem map_id_fun : map (id : α → α) = id := by
   funext l
   induction l <;> simp_all
@@ -1270,6 +1286,8 @@ theorem filter_map (f : β → α) (l : List β) : filter p (map f l) = map f (f
   | nil => rfl
   | cons a l IH => by_cases h : p (f a) <;> simp [*]
 
+@[deprecated filter_map (since := "2024-06-15")] abbrev map_filter := @filter_map
+
 theorem map_filter_eq_foldr (f : α → β) (p : α → Bool) (as : List α) :
     map f (filter p as) = foldr (fun a bs => bif p a then f a :: bs else bs) [] as := by
   induction as with
@@ -1314,6 +1332,8 @@ theorem filter_congr {p q : α → Bool} :
     · simp [pa, h.1 ▸ pa, filter_congr h.2]
     · simp [pa, h.1 ▸ pa, filter_congr h.2]
 
+@[deprecated filter_congr (since := "2024-06-20")] abbrev filter_congr' := @filter_congr
+
 theorem head_filter_of_pos {p : α → Bool} {l : List α} (w : l ≠ []) (h : p (l.head w)) :
     (filter p l).head ((ne_nil_of_mem (mem_filter.2 ⟨head_mem w, h⟩))) = l.head w := by
   cases l with
@@ -1541,6 +1561,11 @@ theorem getElem?_append {l₁ l₂ : List α} {i : Nat} :
   · exact getElem?_append_left h
   · exact getElem?_append_right (by simpa using h)
 
+@[deprecated getElem?_append_right (since := "2024-06-12")]
+theorem get?_append_right {l₁ l₂ : List α} {i : Nat} (h : l₁.length ≤ i) :
+    (l₁ ++ l₂).get? i = l₂.get? (i - l₁.length) := by
+  simp [getElem?_append_right, h]
+
 /-- Variant of `getElem_append_left` useful for rewriting from the small list to the big list. -/
 theorem getElem_append_left' (l₂ : List α) {l₁ : List α} {i : Nat} (hi : i < l₁.length) :
     l₁[i] = (l₁ ++ l₂)[i]'(by simpa using Nat.lt_add_right l₂.length hi) := by
@@ -1551,11 +1576,33 @@ theorem getElem_append_right' (l₁ : List α) {l₂ : List α} {i : Nat} (hi :
     l₂[i] = (l₁ ++ l₂)[i + l₁.length]'(by simpa [Nat.add_comm] using Nat.add_lt_add_left hi _) := by
   rw [getElem_append_right] <;> simp [*, le_add_left]
 
+@[deprecated "Deprecated without replacement." (since := "2024-06-12")]
+theorem get_append_right_aux {l₁ l₂ : List α} {i : Nat}
+  (h₁ : l₁.length ≤ i) (h₂ : i < (l₁ ++ l₂).length) : i - l₁.length < l₂.length := by
+  rw [length_append] at h₂
+  exact Nat.sub_lt_left_of_lt_add h₁ h₂
+
+set_option linter.deprecated false in
+@[deprecated getElem_append_right (since := "2024-06-12")]
+theorem get_append_right' {l₁ l₂ : List α} {i : Nat} (h₁ : l₁.length ≤ i) (h₂) :
+    (l₁ ++ l₂).get ⟨i, h₂⟩ = l₂.get ⟨i - l₁.length, get_append_right_aux h₁ h₂⟩ :=
+  Option.some.inj <| by rw [← get?_eq_get, ← get?_eq_get, get?_append_right h₁]
+
 theorem getElem_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = i) :
     l[i]'(eq ▸ h ▸ by simp_arith) = a := Option.some.inj <| by
   rw [← getElem?_eq_getElem, eq, getElem?_append_right (h ▸ Nat.le_refl _), h]
   simp
 
+@[deprecated "Deprecated without replacement." (since := "2024-06-12")]
+theorem get_of_append_proof {l : List α}
+    (eq : l = l₁ ++ a :: l₂) (h : l₁.length = i) : i < length l := eq ▸ h ▸ by simp_arith
+
+set_option linter.deprecated false in
+@[deprecated getElem_of_append (since := "2024-06-12")]
+theorem get_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = i) :
+    l.get ⟨i, get_of_append_proof eq h⟩ = a := Option.some.inj <| by
+  rw [← get?_eq_get, eq, get?_append_right (h ▸ Nat.le_refl _), h, Nat.sub_self]; rfl
+
 @[simp 1100] theorem singleton_append : [x] ++ l = x :: l := rfl
 
 theorem append_inj :
@@ -1606,6 +1653,26 @@ theorem getLast_concat {a : α} : ∀ (l : List α), getLast (l ++ [a]) (by simp
   | a::t => by
     simp [getLast_cons _, getLast_concat t]
 
+@[deprecated getElem_append (since := "2024-06-12")]
+theorem get_append {l₁ l₂ : List α} (n : Nat) (h : n < l₁.length) :
+    (l₁ ++ l₂).get ⟨n, length_append .. ▸ Nat.lt_add_right _ h⟩ = l₁.get ⟨n, h⟩ := by
+  simp [getElem_append, h]
+
+@[deprecated getElem_append_left (since := "2024-06-12")]
+theorem get_append_left (as bs : List α) (h : i < as.length) {h'} :
+    (as ++ bs).get ⟨i, h'⟩ = as.get ⟨i, h⟩ := by
+  simp [getElem_append_left, h, h']
+
+@[deprecated getElem_append_right (since := "2024-06-12")]
+theorem get_append_right (as bs : List α) (h : as.length ≤ i) {h' h''} :
+    (as ++ bs).get ⟨i, h'⟩ = bs.get ⟨i - as.length, h''⟩ := by
+  simp [getElem_append_right, h, h', h'']
+
+@[deprecated getElem?_append_left (since := "2024-06-12")]
+theorem get?_append {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) :
+    (l₁ ++ l₂).get? n = l₁.get? n := by
+  simp [getElem?_append_left hn]
+
 @[simp] theorem append_eq_nil_iff : p ++ q = [] ↔ p = [] ∧ q = [] := by
   cases p <;> simp
 
@@ -2132,6 +2199,10 @@ theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
     (replicate n a)[m] = a :=
   eq_of_mem_replicate (getElem_mem _)
 
+@[deprecated getElem_replicate (since := "2024-06-12")]
+theorem get_replicate (a : α) {n : Nat} (m : Fin _) : (replicate n a).get m = a := by
+  simp
+
 theorem getElem?_replicate : (replicate n a)[m]? = if m < n then some a else none := by
   by_cases h : m < n
   · rw [getElem?_eq_getElem (by simpa), getElem_replicate, if_pos h]
@@ -2367,6 +2438,10 @@ theorem getElem?_reverse' : ∀ {l : List α} (i j), i + j + 1 = length l →
     rw [getElem?_append_left, getElem?_reverse' _ _ this]
     rw [length_reverse, ← this]; apply Nat.lt_add_of_pos_right (Nat.succ_pos _)
 
+@[deprecated getElem?_reverse' (since := "2024-06-12")]
+theorem get?_reverse' {l : List α} (i j) (h : i + j + 1 = length l) : get? l.reverse i = get? l j := by
+  simp [getElem?_reverse' _ _ h]
+
 @[simp]
 theorem getElem?_reverse {l : List α} {i} (h : i < length l) :
     l.reverse[i]? = l[l.length - 1 - i]? :=
@@ -2381,6 +2456,11 @@ theorem getElem_reverse {l : List α} {i} (h : i < l.reverse.length) :
   rw [← getElem?_eq_getElem, ← getElem?_eq_getElem]
   rw [getElem?_reverse (by simpa using h)]
 
+@[deprecated getElem?_reverse (since := "2024-06-12")]
+theorem get?_reverse {l : List α} {i} (h : i < length l) :
+    get? l.reverse i = get? l (l.length - 1 - i) := by
+  simp [getElem?_reverse h]
+
 theorem reverseAux_reverseAux_nil (as bs : List α) : reverseAux (reverseAux as bs) [] = reverseAux bs as := by
   induction as generalizing bs with
   | nil => rfl
@@ -2421,6 +2501,10 @@ theorem mem_of_mem_getLast? {l : List α} {a : α} (h : a ∈ getLast? l) : a
 @[simp] theorem map_reverse (f : α → β) (l : List α) : l.reverse.map f = (l.map f).reverse := by
   induction l <;> simp [*]
 
+@[deprecated map_reverse (since := "2024-06-20")]
+theorem reverse_map (f : α → β) (l : List α) : (l.map f).reverse = l.reverse.map f := by
+  simp
+
 @[simp] theorem filter_reverse (p : α → Bool) (l : List α) : (l.reverse.filter p) = (l.filter p).reverse := by
   induction l with
   | nil => simp
@@ -2884,6 +2968,11 @@ are often used for theorems about `Array.pop`.
   | _::_::_, 0, _ => rfl
   | _::_::_, i+1, h => getElem_dropLast _ i (Nat.add_one_lt_add_one_iff.mp h)
 
+@[deprecated getElem_dropLast (since := "2024-06-12")]
+theorem get_dropLast (xs : List α) (i : Fin xs.dropLast.length) :
+    xs.dropLast.get i = xs.get ⟨i, Nat.lt_of_lt_of_le i.isLt (length_dropLast .. ▸ Nat.pred_le _)⟩ := by
+  simp
+
 theorem getElem?_dropLast (xs : List α) (i : Nat) :
     xs.dropLast[i]? = if i < xs.length - 1 then xs[i]? else none := by
   split
@@ -3421,6 +3510,29 @@ theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a :=
 
 /-! ### Deprecations -/
 
+@[deprecated getD_eq_getElem?_getD (since := "2024-06-12")]
+theorem getD_eq_get? : ∀ l n (a : α), getD l n a = (get? l n).getD a := by simp
+@[deprecated getElem_singleton (since := "2024-06-12")]
+theorem get_singleton (a : α) (n : Fin 1) : get [a] n = a := by simp
+@[deprecated getElem?_concat_length (since := "2024-06-12")]
+theorem get?_concat_length (l : List α) (a : α) : (l ++ [a]).get? l.length = some a := by simp
+@[deprecated getElem_set_self (since := "2024-06-12")]
+theorem get_set_eq {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) :
+    (l.set i a).get ⟨i, h⟩ = a := by
+  simp
+@[deprecated getElem_set_ne (since := "2024-06-12")]
+theorem get_set_ne {l : List α} {i j : Nat} (h : i ≠ j) {a : α}
+    (hj : j < (l.set i a).length) :
+    (l.set i a).get ⟨j, hj⟩ = l.get ⟨j, by simp at hj; exact hj⟩ := by
+  simp [h]
+@[deprecated getElem_set (since := "2024-06-12")]
+theorem get_set {l : List α} {m n} {a : α} (h) :
+    (set l m a).get ⟨n, h⟩ = if m = n then a else l.get ⟨n, length_set .. ▸ h⟩ := by
+  simp [getElem_set]
+@[deprecated cons_inj_right (since := "2024-06-15")] abbrev cons_inj := @cons_inj_right
+@[deprecated ne_nil_of_length_eq_add_one (since := "2024-06-16")]
+abbrev ne_nil_of_length_eq_succ := @ne_nil_of_length_eq_add_one
+
 @[deprecated "Deprecated without replacement." (since := "2024-07-09")]
 theorem get_cons_cons_one : (a₁ :: a₂ :: as).get (1 : Fin (as.length + 2)) = a₂ := rfl
 

src/Init/Data/List/MapIdx.lean

@@ -22,13 +22,13 @@ namespace List
 Given a list `as = [a₀, a₁, ...]` function `f : Fin as.length → α → β`, returns the list
 `[f 0 a₀, f 1 a₁, ...]`.
 -/
-@[inline] def mapFinIdx (as : List α) (f : (i : Nat) → α → (h : i < as.length) → β) : List β := go as #[] (by simp) where
+@[inline] def mapFinIdx (as : List α) (f : Fin as.length → α → β) : List β := go as #[] (by simp) where
   /-- Auxiliary for `mapFinIdx`:
   `mapFinIdx.go [a₀, a₁, ...] acc = acc.toList ++ [f 0 a₀, f 1 a₁, ...]` -/
   @[specialize] go : (bs : List α) → (acc : Array β) → bs.length + acc.size = as.length → List β
   | [], acc, h => acc.toList
   | a :: as, acc, h =>
-    go as (acc.push (f acc.size a (by simp at h; omega))) (by simp at h ⊢; omega)
+    go as (acc.push (f ⟨acc.size, by simp at h; omega⟩ a)) (by simp at h ⊢; omega)
 
 /--
 Given a function `f : Nat → α → β` and `as : List α`, `as = [a₀, a₁, ...]`, returns the list
@@ -44,7 +44,7 @@ Given a function `f : Nat → α → β` and `as : List α`, `as = [a₀, a₁,
 /-! ### mapFinIdx -/
 
 @[simp]
-theorem mapFinIdx_nil {f : (i : Nat) → α → (h : i < 0) → β} : mapFinIdx [] f = [] :=
+theorem mapFinIdx_nil {f : Fin 0 → α → β} : mapFinIdx [] f = [] :=
   rfl
 
 @[simp] theorem length_mapFinIdx_go :
@@ -53,16 +53,13 @@ theorem mapFinIdx_nil {f : (i : Nat) → α → (h : i < 0) → β} : mapFinIdx
   | nil => simpa using h
   | cons _ _ ih => simp [mapFinIdx.go, ih]
 
-@[simp] theorem length_mapFinIdx {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} :
+@[simp] theorem length_mapFinIdx {as : List α} {f : Fin as.length → α → β} :
     (as.mapFinIdx f).length = as.length := by
   simp [mapFinIdx, length_mapFinIdx_go]
 
-theorem getElem_mapFinIdx_go {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} {i : Nat} {h} {w} :
+theorem getElem_mapFinIdx_go {as : List α} {f : Fin as.length → α → β} {i : Nat} {h} {w} :
     (mapFinIdx.go as f bs acc h)[i] =
-      if w' : i < acc.size then
-        acc[i]
-      else
-        f i (bs[i - acc.size]'(by simp at w; omega)) (by simp at w; omega) := by
+      if w' : i < acc.size then acc[i] else f ⟨i, by simp at w; omega⟩ (bs[i - acc.size]'(by simp at w; omega)) := by
   induction bs generalizing acc with
   | nil =>
     simp only [length_mapFinIdx_go, length_nil, Nat.zero_add] at w h
@@ -81,30 +78,29 @@ theorem getElem_mapFinIdx_go {as : List α} {f : (i : Nat) → α → (h : i < a
     · have h₃ : i - acc.size = (i - (acc.size + 1)) + 1 := by omega
       simp [h₃]
 
-@[simp] theorem getElem_mapFinIdx {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} {i : Nat} {h} :
-    (as.mapFinIdx f)[i] = f i (as[i]'(by simp at h; omega)) (by simp at h; omega) := by
+@[simp] theorem getElem_mapFinIdx {as : List α} {f : Fin as.length → α → β} {i : Nat} {h} :
+    (as.mapFinIdx f)[i] = f ⟨i, by simp at h; omega⟩ (as[i]'(by simp at h; omega)) := by
   simp [mapFinIdx, getElem_mapFinIdx_go]
 
-theorem mapFinIdx_eq_ofFn {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} :
-    as.mapFinIdx f = List.ofFn fun i : Fin as.length => f i as[i] i.2 := by
+theorem mapFinIdx_eq_ofFn {as : List α} {f : Fin as.length → α → β} :
+    as.mapFinIdx f = List.ofFn fun i : Fin as.length => f i as[i] := by
   apply ext_getElem <;> simp
 
-@[simp] theorem getElem?_mapFinIdx {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {i : Nat} :
-    (l.mapFinIdx f)[i]? = l[i]?.pbind fun x m => f i x (by simp [getElem?_eq_some_iff] at m; exact m.1) := by
+@[simp] theorem getElem?_mapFinIdx {l : List α} {f : Fin l.length → α → β} {i : Nat} :
+    (l.mapFinIdx f)[i]? = l[i]?.pbind fun x m => f ⟨i, by simp [getElem?_eq_some_iff] at m; exact m.1⟩ x := by
   simp only [getElem?_def, length_mapFinIdx, getElem_mapFinIdx]
   split <;> simp
 
 @[simp]
-theorem mapFinIdx_cons {l : List α} {a : α} {f : (i : Nat) → α → (h : i < l.length + 1) → β} :
-    mapFinIdx (a :: l) f = f 0 a (by omega) :: mapFinIdx l (fun i a h => f (i + 1) a (by omega)) := by
+theorem mapFinIdx_cons {l : List α} {a : α} {f : Fin (l.length + 1) → α → β} :
+    mapFinIdx (a :: l) f = f 0 a :: mapFinIdx l (fun i => f i.succ) := by
   apply ext_getElem
   · simp
   · rintro (_|i) h₁ h₂ <;> simp
 
-theorem mapFinIdx_append {K L : List α} {f : (i : Nat) → α → (h : i < (K ++ L).length) → β} :
+theorem mapFinIdx_append {K L : List α} {f : Fin (K ++ L).length → α → β} :
     (K ++ L).mapFinIdx f =
-      K.mapFinIdx (fun i a h => f i a (by simp; omega)) ++
-        L.mapFinIdx (fun i a h => f (i + K.length) a (by simp; omega)) := by
+      K.mapFinIdx (fun i => f (i.castLE (by simp))) ++ L.mapFinIdx (fun i => f ((i.natAdd K.length).cast (by simp))) := by
   apply ext_getElem
   · simp
   · intro i h₁ h₂
@@ -112,57 +108,60 @@ theorem mapFinIdx_append {K L : List α} {f : (i : Nat) → α → (h : i < (K +
     simp only [getElem_mapFinIdx, length_mapFinIdx]
     split <;> rename_i h
     · rw [getElem_append_left]
+      congr
     · simp only [Nat.not_lt] at h
       rw [getElem_append_right h]
       congr
+      simp
       omega
 
-@[simp] theorem mapFinIdx_concat {l : List α} {e : α} {f : (i : Nat) → α → (h : i < (l ++ [e]).length) → β}:
-    (l ++ [e]).mapFinIdx f = l.mapFinIdx (fun i a h => f i a (by simp; omega)) ++ [f l.length e (by simp)] := by
+@[simp] theorem mapFinIdx_concat {l : List α} {e : α} {f : Fin (l ++ [e]).length → α → β}:
+    (l ++ [e]).mapFinIdx f = l.mapFinIdx (fun i => f (i.castLE (by simp))) ++ [f ⟨l.length, by simp⟩ e] := by
   simp [mapFinIdx_append]
+  congr
 
-theorem mapFinIdx_singleton {a : α} {f : (i : Nat) → α → (h : i < 1) → β} :
-    [a].mapFinIdx f = [f 0 a (by simp)] := by
+theorem mapFinIdx_singleton {a : α} {f : Fin 1 → α → β} :
+    [a].mapFinIdx f = [f ⟨0, by simp⟩ a] := by
   simp
 
-theorem mapFinIdx_eq_enum_map {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
+theorem mapFinIdx_eq_enum_map {l : List α} {f : Fin l.length → α → β} :
     l.mapFinIdx f = l.enum.attach.map
       fun ⟨⟨i, x⟩, m⟩ =>
-        f i x (by rw [mk_mem_enum_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1) := by
+        f ⟨i, by rw [mk_mem_enum_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1⟩ x := by
   apply ext_getElem <;> simp
 
 @[simp]
-theorem mapFinIdx_eq_nil_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
+theorem mapFinIdx_eq_nil_iff {l : List α} {f : Fin l.length → α → β} :
     l.mapFinIdx f = [] ↔ l = [] := by
   rw [mapFinIdx_eq_enum_map, map_eq_nil_iff, attach_eq_nil_iff, enum_eq_nil_iff]
 
-theorem mapFinIdx_ne_nil_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
+theorem mapFinIdx_ne_nil_iff {l : List α} {f : Fin l.length → α → β} :
     l.mapFinIdx f ≠ [] ↔ l ≠ [] := by
   simp
 
-theorem exists_of_mem_mapFinIdx {b : β} {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β}
-    (h : b ∈ l.mapFinIdx f) : ∃ (i : Nat) (h : i < l.length), f i l[i] h = b := by
+theorem exists_of_mem_mapFinIdx {b : β} {l : List α} {f : Fin l.length → α → β}
+    (h : b ∈ l.mapFinIdx f) : ∃ (i : Fin l.length), f i l[i] = b := by
   rw [mapFinIdx_eq_enum_map] at h
   replace h := exists_of_mem_map h
   simp only [mem_attach, true_and, Subtype.exists, Prod.exists, mk_mem_enum_iff_getElem?] at h
   obtain ⟨i, b, h, rfl⟩ := h
   rw [getElem?_eq_some_iff] at h
   obtain ⟨h', rfl⟩ := h
-  exact ⟨i, h', rfl⟩
+  exact ⟨⟨i, h'⟩, rfl⟩
 
-@[simp] theorem mem_mapFinIdx {b : β} {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
-    b ∈ l.mapFinIdx f ↔ ∃ (i : Nat) (h : i < l.length), f i l[i] h = b := by
+@[simp] theorem mem_mapFinIdx {b : β} {l : List α} {f : Fin l.length → α → β} :
+    b ∈ l.mapFinIdx f ↔ ∃ (i : Fin l.length), f i l[i] = b := by
   constructor
   · intro h
     exact exists_of_mem_mapFinIdx h
   · rintro ⟨i, h, rfl⟩
     rw [mem_iff_getElem]
-    exact ⟨i, by simpa using h, by simp⟩
+    exact ⟨i, by simp⟩
 
-theorem mapFinIdx_eq_cons_iff {l : List α} {b : β} {f : (i : Nat) → α → (h : i < l.length) → β} :
+theorem mapFinIdx_eq_cons_iff {l : List α} {b : β} {f : Fin l.length → α → β} :
     l.mapFinIdx f = b :: l₂ ↔
-      ∃ (a : α) (l₁ : List α) (w : l = a :: l₁),
-        f 0 a (by simp [w]) = b ∧ l₁.mapFinIdx (fun i a h => f (i + 1) a (by simp [w]; omega)) = l₂ := by
+      ∃ (a : α) (l₁ : List α) (h : l = a :: l₁),
+        f ⟨0, by simp [h]⟩ a = b ∧ l₁.mapFinIdx (fun i => f (i.succ.cast (by simp [h]))) = l₂ := by
   cases l with
   | nil => simp
   | cons x l' =>
@@ -170,48 +169,39 @@ theorem mapFinIdx_eq_cons_iff {l : List α} {b : β} {f : (i : Nat) → α → (
       exists_and_left]
     constructor
     · rintro ⟨rfl, rfl⟩
-      refine ⟨x, l', ⟨rfl, rfl⟩, by simp⟩
-    · rintro ⟨a, l', ⟨rfl, rfl⟩, ⟨rfl, rfl⟩⟩
-      exact ⟨rfl, by simp⟩
+      refine ⟨x, rfl, l', by simp⟩
+    · rintro ⟨a, ⟨rfl, h⟩, ⟨_, ⟨rfl, rfl⟩, h⟩⟩
+      exact ⟨rfl, h⟩
 
-theorem mapFinIdx_eq_cons_iff' {l : List α} {b : β} {f : (i : Nat) → α → (h : i < l.length) → β} :
+theorem mapFinIdx_eq_cons_iff' {l : List α} {b : β} {f : Fin l.length → α → β} :
     l.mapFinIdx f = b :: l₂ ↔
-      l.head?.pbind (fun x m => (f 0 x (by cases l <;> simp_all))) = some b ∧
-        l.tail?.attach.map (fun ⟨t, m⟩ => t.mapFinIdx fun i a h => f (i + 1) a (by cases l <;> simp_all)) = some l₂ := by
+      l.head?.pbind (fun x m => (f ⟨0, by cases l <;> simp_all⟩ x)) = some b ∧
+        l.tail?.attach.map (fun ⟨t, m⟩ => t.mapFinIdx fun i => f (i.succ.cast (by cases l <;> simp_all))) = some l₂ := by
   cases l <;> simp
 
-theorem mapFinIdx_eq_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
-    l.mapFinIdx f = l' ↔ ∃ h : l'.length = l.length, ∀ (i : Nat) (h : i < l.length), l'[i] = f i l[i] h := by
+theorem mapFinIdx_eq_iff {l : List α} {f : Fin l.length → α → β} :
+    l.mapFinIdx f = l' ↔ ∃ h : l'.length = l.length, ∀ (i : Nat) (h : i < l.length), l'[i] = f ⟨i, h⟩ l[i] := by
   constructor
   · rintro rfl
     simp
   · rintro ⟨h, w⟩
     apply ext_getElem <;> simp_all
 
-theorem mapFinIdx_eq_mapFinIdx_iff {l : List α} {f g : (i : Nat) → α → (h : i < l.length) → β} :
-    l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] h = g i l[i] h := by
+theorem mapFinIdx_eq_mapFinIdx_iff {l : List α} {f g : Fin l.length → α → β} :
+    l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Fin l.length), f i l[i] = g i l[i] := by
   rw [eq_comm, mapFinIdx_eq_iff]
   simp [Fin.forall_iff]
 
-@[simp] theorem mapFinIdx_mapFinIdx {l : List α}
-    {f : (i : Nat) → α → (h : i < l.length) → β}
-    {g : (i : Nat) → β → (h : i < (l.mapFinIdx f).length) → γ} :
-    (l.mapFinIdx f).mapFinIdx g = l.mapFinIdx (fun i a h => g i (f i a h) (by simpa)) := by
+@[simp] theorem mapFinIdx_mapFinIdx {l : List α} {f : Fin l.length → α → β} {g : Fin _ → β → γ} :
+    (l.mapFinIdx f).mapFinIdx g = l.mapFinIdx (fun i => g (i.cast (by simp)) ∘ f i) := by
   simp [mapFinIdx_eq_iff]
 
-theorem mapFinIdx_eq_replicate_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {b : β} :
-    l.mapFinIdx f = replicate l.length b ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] h = b := by
-  rw [eq_replicate_iff, length_mapFinIdx]
-  simp only [mem_mapFinIdx, forall_exists_index, true_and]
-  constructor
-  · intro w i h
-    exact w (f i l[i] h) i h rfl
-  · rintro w b i h rfl
-    exact w i h
+theorem mapFinIdx_eq_replicate_iff {l : List α} {f : Fin l.length → α → β} {b : β} :
+    l.mapFinIdx f = replicate l.length b ↔ ∀ (i : Fin l.length), f i l[i] = b := by
+  simp [eq_replicate_iff, length_mapFinIdx, mem_mapFinIdx, forall_exists_index, true_and]
 
-@[simp] theorem mapFinIdx_reverse {l : List α} {f : (i : Nat) → α → (h : i < l.reverse.length) → β} :
-    l.reverse.mapFinIdx f =
-      (l.mapFinIdx (fun i a h => f (l.length - 1 - i) a (by simp; omega))).reverse := by
+@[simp] theorem mapFinIdx_reverse {l : List α} {f : Fin l.reverse.length → α → β} :
+    l.reverse.mapFinIdx f = (l.mapFinIdx (fun i => f ⟨l.length - 1 - i, by simp; omega⟩)).reverse := by
   simp [mapFinIdx_eq_iff]
   intro i h
   congr
@@ -272,13 +262,13 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {arr : Array β} {i : Nat},
   rw [← getElem?_eq_getElem, getElem?_mapIdx, getElem?_eq_getElem (by simpa using h)]
   simp
 
-@[simp] theorem mapFinIdx_eq_mapIdx {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {g : Nat → α → β}
-    (h : ∀ (i : Nat) (h : i < l.length), f i l[i] h = g i l[i]) :
+@[simp] theorem mapFinIdx_eq_mapIdx {l : List α} {f : Fin l.length → α → β} {g : Nat → α → β}
+    (h : ∀ (i : Fin l.length), f i l[i] = g i l[i]) :
     l.mapFinIdx f = l.mapIdx g := by
   simp_all [mapFinIdx_eq_iff]
 
 theorem mapIdx_eq_mapFinIdx {l : List α} {f : Nat → α → β} :
-    l.mapIdx f = l.mapFinIdx (fun i a _ => f i a) := by
+    l.mapIdx f = l.mapFinIdx (fun i => f i) := by
   simp [mapFinIdx_eq_mapIdx]
 
 theorem mapIdx_eq_enum_map {l : List α} :

src/Init/Data/List/Nat/TakeDrop.lean

@@ -47,16 +47,41 @@ length `> i`. Version designed to rewrite from the small list to the big list. -
     L[i]'(Nat.lt_of_lt_of_le h (length_take_le' _ _)) := by
   rw [length_take, Nat.lt_min] at h; rw [getElem_take' L _ h.1]
 
+/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
+length `> i`. Version designed to rewrite from the big list to the small list. -/
+@[deprecated getElem_take' (since := "2024-06-12")]
+theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
+    get L ⟨i, hi⟩ = get (L.take j) ⟨i, length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩⟩ := by
+  simp
+
+/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
+length `> i`. Version designed to rewrite from the small list to the big list. -/
+@[deprecated getElem_take (since := "2024-06-12")]
+theorem get_take' (L : List α) {j i} :
+    get (L.take j) i =
+    get L ⟨i.1, Nat.lt_of_lt_of_le i.2 (length_take_le' _ _)⟩ := by
+  simp [getElem_take]
+
 theorem getElem?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
     (l.take n)[m]? = none :=
   getElem?_eq_none <| Nat.le_trans (length_take_le _ _) h
 
+@[deprecated getElem?_take_eq_none (since := "2024-06-12")]
+theorem get?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
+    (l.take n).get? m = none := by
+  simp [getElem?_take_eq_none h]
+
 theorem getElem?_take {l : List α} {n m : Nat} :
     (l.take n)[m]? = if m < n then l[m]? else none := by
   split
   · next h => exact getElem?_take_of_lt h
   · next h => exact getElem?_take_eq_none (Nat.le_of_not_lt h)
 
+@[deprecated getElem?_take (since := "2024-06-12")]
+theorem get?_take_eq_if {l : List α} {n m : Nat} :
+    (l.take n).get? m = if m < n then l.get? m else none := by
+  simp [getElem?_take]
+
 theorem head?_take {l : List α} {n : Nat} :
     (l.take n).head? = if n = 0 then none else l.head? := by
   simp [head?_eq_getElem?, getElem?_take]
@@ -201,6 +226,13 @@ theorem getElem_drop' (L : List α) {i j : Nat} (h : i + j < L.length) :
   · simp [Nat.min_eq_left this, Nat.add_sub_cancel_left]
   · simp [Nat.min_eq_left this, Nat.le_add_right]
 
+/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
+dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/
+@[deprecated getElem_drop' (since := "2024-06-12")]
+theorem get_drop (L : List α) {i j : Nat} (h : i + j < L.length) :
+    get L ⟨i + j, h⟩ = get (L.drop i) ⟨j, lt_length_drop L h⟩ := by
+  simp [getElem_drop']
+
 /-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
 dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/
 @[simp] theorem getElem_drop (L : List α) {i : Nat} {j : Nat} {h : j < (L.drop i).length} :
@@ -209,6 +241,15 @@ dropping the first `i` elements. Version designed to rewrite from the small list
       exact Nat.add_lt_of_lt_sub (length_drop i L ▸ h)) := by
   rw [getElem_drop']
 
+/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
+dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/
+@[deprecated getElem_drop' (since := "2024-06-12")]
+theorem get_drop' (L : List α) {i j} :
+    get (L.drop i) j = get L ⟨i + j, by
+      rw [Nat.add_comm]
+      exact Nat.add_lt_of_lt_sub (length_drop i L ▸ j.2)⟩ := by
+  simp
+
 @[simp]
 theorem getElem?_drop (L : List α) (i j : Nat) : (L.drop i)[j]? = L[i + j]? := by
   ext
@@ -220,6 +261,10 @@ theorem getElem?_drop (L : List α) (i j : Nat) : (L.drop i)[j]? = L[i + j]? :=
     rw [Nat.add_comm] at h
     apply Nat.lt_sub_of_add_lt h
 
+@[deprecated getElem?_drop (since := "2024-06-12")]
+theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) := by
+  simp
+
 theorem mem_take_iff_getElem {l : List α} {a : α} :
     a ∈ l.take n ↔ ∃ (i : Nat) (hm : i < min n l.length), l[i] = a := by
   rw [mem_iff_getElem]

src/Init/Data/List/TakeDrop.lean

@@ -67,9 +67,17 @@ theorem getElem_cons_drop : ∀ (l : List α) (i : Nat) (h : i < l.length),
   | _::_, 0, _ => rfl
   | _::_, i+1, h => getElem_cons_drop _ i (Nat.add_one_lt_add_one_iff.mp h)
 
+@[deprecated getElem_cons_drop (since := "2024-06-12")]
+theorem get_cons_drop (l : List α) (i) : get l i :: drop (i + 1) l = drop i l := by
+  simp
+
 theorem drop_eq_getElem_cons {n} {l : List α} (h : n < l.length) : drop n l = l[n] :: drop (n + 1) l :=
   (getElem_cons_drop _ n h).symm
 
+@[deprecated drop_eq_getElem_cons (since := "2024-06-12")]
+theorem drop_eq_get_cons {n} {l : List α} (h) : drop n l = get l ⟨n, h⟩ :: drop (n + 1) l := by
+  simp [drop_eq_getElem_cons]
+
 @[simp]
 theorem getElem?_take_of_lt {l : List α} {n m : Nat} (h : m < n) : (l.take n)[m]? = l[m]? := by
   induction n generalizing l m with
@@ -83,6 +91,10 @@ theorem getElem?_take_of_lt {l : List α} {n m : Nat} (h : m < n) : (l.take n)[m
       · simp
       · simpa using hn (Nat.lt_of_succ_lt_succ h)
 
+@[deprecated getElem?_take_of_lt (since := "2024-06-12")]
+theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.get? m := by
+  simp [getElem?_take_of_lt, h]
+
 theorem getElem?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l[n]? := by simp
 
 @[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (m + n) l
@@ -99,6 +111,10 @@ theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (t
   | _, _, [] => by simp
   | _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop ..
 
+@[deprecated drop_drop (since := "2024-06-15")]
+theorem drop_add (m n) (l : List α) : drop (m + n) l = drop n (drop m l) := by
+  simp [drop_drop]
+
 @[simp]
 theorem tail_drop (l : List α) (n : Nat) : (l.drop n).tail = l.drop (n + 1) := by
   induction l generalizing n with

src/Init/Data/List/Zip.lean

@@ -76,6 +76,15 @@ theorem getElem?_zip_eq_some {l₁ : List α} {l₂ : List β} {z : α × β} {i
   · rintro ⟨h₀, h₁⟩
     exact ⟨_, _, h₀, h₁, rfl⟩
 
+@[deprecated getElem?_zipWith (since := "2024-06-12")]
+theorem get?_zipWith {f : α → β → γ} :
+    (List.zipWith f as bs).get? i = match as.get? i, bs.get? i with
+      | some a, some b => some (f a b) | _, _ => none := by
+  simp [getElem?_zipWith]
+
+set_option linter.deprecated false in
+@[deprecated getElem?_zipWith (since := "2024-06-07")] abbrev zipWith_get? := @get?_zipWith
+
 theorem head?_zipWith {f : α → β → γ} :
     (List.zipWith f as bs).head? = match as.head?, bs.head? with
       | some a, some b => some (f a b) | _, _ => none := by
@@ -360,6 +369,15 @@ theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Nat} :
       cases i <;> simp_all
     | cons b bs => cases i <;> simp_all
 
+@[deprecated getElem?_zipWithAll (since := "2024-06-12")]
+theorem get?_zipWithAll {f : Option α → Option β → γ} :
+    (zipWithAll f as bs).get? i = match as.get? i, bs.get? i with
+      | none, none => .none | a?, b? => some (f a? b?) := by
+  simp [getElem?_zipWithAll]
+
+set_option linter.deprecated false in
+@[deprecated getElem?_zipWithAll (since := "2024-06-07")] abbrev zipWithAll_get? := @get?_zipWithAll
+
 theorem head?_zipWithAll {f : Option α → Option β → γ} :
     (zipWithAll f as bs).head? = match as.head?, bs.head? with
       | none, none => .none | a?, b? => some (f a? b?) := by

src/Init/Data/Nat/Basic.lean

@@ -788,6 +788,9 @@ theorem not_eq_zero_of_lt (h : b < a) : a ≠ 0 := by
 theorem pred_lt_of_lt {n m : Nat} (h : m < n) : pred n < n :=
   pred_lt (not_eq_zero_of_lt h)
 
+set_option linter.missingDocs false in
+@[deprecated pred_lt_of_lt (since := "2024-06-01")] abbrev pred_lt' := @pred_lt_of_lt
+
 theorem sub_one_lt_of_lt {n m : Nat} (h : m < n) : n - 1 < n :=
   sub_one_lt (not_eq_zero_of_lt h)
 
@@ -1071,6 +1074,9 @@ theorem pred_mul (n m : Nat) : pred n * m = n * m - m := by
   | zero   => simp
   | succ n => rw [Nat.pred_succ, succ_mul, Nat.add_sub_cancel]
 
+set_option linter.missingDocs false in
+@[deprecated pred_mul (since := "2024-06-01")] abbrev mul_pred_left := @pred_mul
+
 protected theorem sub_one_mul  (n m : Nat) : (n - 1) * m = n * m - m := by
   cases n with
   | zero   => simp
@@ -1080,6 +1086,9 @@ protected theorem sub_one_mul  (n m : Nat) : (n - 1) * m = n * m - m := by
 theorem mul_pred (n m : Nat) : n * pred m = n * m - n := by
   rw [Nat.mul_comm, pred_mul, Nat.mul_comm]
 
+set_option linter.missingDocs false in
+@[deprecated mul_pred (since := "2024-06-01")] abbrev mul_pred_right := @mul_pred
+
 theorem mul_sub_one (n m : Nat) : n * (m - 1) = n * m - n := by
   rw [Nat.mul_comm, Nat.sub_one_mul , Nat.mul_comm]
 

src/Init/Data/Nat/Lemmas.lean

@@ -1003,6 +1003,11 @@ theorem shiftLeft_add (m n : Nat) : ∀ k, m <<< (n + k) = (m <<< n) <<< k
   | 0 => rfl
   | k + 1 => by simp [← Nat.add_assoc, shiftLeft_add _ _ k, shiftLeft_succ]
 
+@[deprecated shiftLeft_add (since := "2024-06-02")]
+theorem shiftLeft_shiftLeft (m n : Nat) : ∀ k, (m <<< n) <<< k = m <<< (n + k)
+  | 0 => rfl
+  | k + 1 => by simp [← Nat.add_assoc, shiftLeft_shiftLeft _ _ k, shiftLeft_succ]
+
 @[simp] theorem shiftLeft_shiftRight (x n : Nat) : x <<< n >>> n = x := by
   rw [Nat.shiftLeft_eq, Nat.shiftRight_eq_div_pow, Nat.mul_div_cancel _ (Nat.two_pow_pos _)]
 

src/Init/Data/UInt/Lemmas.lean

@@ -234,3 +234,23 @@ theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < size) : n ≤ ofNa
 
 theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < size) : ofNat m ≤ n → m ≤ n.toNat := by
   simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
+
+@[deprecated UInt8.toNat_zero (since := "2024-06-23")] protected abbrev UInt8.zero_toNat := @UInt8.toNat_zero
+@[deprecated UInt8.toNat_div (since := "2024-06-23")] protected abbrev UInt8.div_toNat := @UInt8.toNat_div
+@[deprecated UInt8.toNat_mod (since := "2024-06-23")] protected abbrev UInt8.mod_toNat := @UInt8.toNat_mod
+
+@[deprecated UInt16.toNat_zero (since := "2024-06-23")] protected abbrev UInt16.zero_toNat := @UInt16.toNat_zero
+@[deprecated UInt16.toNat_div (since := "2024-06-23")] protected abbrev UInt16.div_toNat := @UInt16.toNat_div
+@[deprecated UInt16.toNat_mod (since := "2024-06-23")] protected abbrev UInt16.mod_toNat := @UInt16.toNat_mod
+
+@[deprecated UInt32.toNat_zero (since := "2024-06-23")] protected abbrev UInt32.zero_toNat := @UInt32.toNat_zero
+@[deprecated UInt32.toNat_div (since := "2024-06-23")] protected abbrev UInt32.div_toNat := @UInt32.toNat_div
+@[deprecated UInt32.toNat_mod (since := "2024-06-23")] protected abbrev UInt32.mod_toNat := @UInt32.toNat_mod
+
+@[deprecated UInt64.toNat_zero (since := "2024-06-23")] protected abbrev UInt64.zero_toNat := @UInt64.toNat_zero
+@[deprecated UInt64.toNat_div (since := "2024-06-23")] protected abbrev UInt64.div_toNat := @UInt64.toNat_div
+@[deprecated UInt64.toNat_mod (since := "2024-06-23")] protected abbrev UInt64.mod_toNat := @UInt64.toNat_mod
+
+@[deprecated USize.toNat_zero (since := "2024-06-23")] protected abbrev USize.zero_toNat := @USize.toNat_zero
+@[deprecated USize.toNat_div (since := "2024-06-23")] protected abbrev USize.div_toNat := @USize.toNat_div
+@[deprecated USize.toNat_mod (since := "2024-06-23")] protected abbrev USize.mod_toNat := @USize.toNat_mod

src/Init/Data/Vector/Lemmas.lean

@@ -1746,92 +1746,6 @@ theorem flatMap_mkArray {β} (f : α → Vector β m) : (mkVector n a).flatMap f
 @[simp] theorem sum_mkArray_nat (n : Nat) (a : Nat) : (mkVector n a).sum = n * a := by
   simp [toArray_mkVector]
 
-/-! ### reverse -/
-
-@[simp] theorem reverse_push (as : Vector α n) (a : α) :
-    (as.push a).reverse = (#v[a] ++ as.reverse).cast (by omega) := by
-  rcases as with ⟨as, rfl⟩
-  simp [Array.reverse_push]
-
-@[simp] theorem mem_reverse {x : α} {as : Vector α n} : x ∈ as.reverse ↔ x ∈ as := by
-  cases as
-  simp
-
-@[simp] theorem getElem_reverse (a : Vector α n) (i : Nat) (hi : i < n) :
-    (a.reverse)[i] = a[n - 1 - i] := by
-  rcases a with ⟨a, rfl⟩
-  simp
-
-/-- Variant of `getElem?_reverse` with a hypothesis giving the linear relation between the indices. -/
-theorem getElem?_reverse' {l : Vector α n} (i j) (h : i + j + 1 = n) : l.reverse[i]? = l[j]? := by
-  rcases l with ⟨l, rfl⟩
-  simpa using Array.getElem?_reverse' i j h
-
-@[simp]
-theorem getElem?_reverse {l : Vector α n} {i} (h : i < n) :
-    l.reverse[i]? = l[n - 1 - i]? := by
-  cases l
-  simp_all
-
-@[simp] theorem reverse_reverse (as : Vector α n) : as.reverse.reverse = as := by
-  rcases as with ⟨as, rfl⟩
-  simp [Array.reverse_reverse]
-
-theorem reverse_eq_iff {as bs : Vector α n} : as.reverse = bs ↔ as = bs.reverse := by
-  constructor <;> (rintro rfl; simp)
-
-@[simp] theorem reverse_inj {xs ys : Vector α n} : xs.reverse = ys.reverse ↔ xs = ys := by
-  simp [reverse_eq_iff]
-
-@[simp] theorem reverse_eq_push_iff {xs : Vector α (n + 1)} {ys : Vector α n} {a : α} :
-    xs.reverse = ys.push a ↔ xs = (#v[a] ++ ys.reverse).cast (by omega) := by
-  rcases xs with ⟨xs, h⟩
-  rcases ys with ⟨ys, rfl⟩
-  simp [Array.reverse_eq_push_iff]
-
-@[simp] theorem map_reverse (f : α → β) (l : Vector α n) : l.reverse.map f = (l.map f).reverse := by
-  rcases l with ⟨l, rfl⟩
-  simp [Array.map_reverse]
-
-@[simp] theorem reverse_append (as : Vector α n) (bs : Vector α m) :
-    (as ++ bs).reverse = (bs.reverse ++ as.reverse).cast (by omega) := by
-  rcases as with ⟨as, rfl⟩
-  rcases bs with ⟨bs, rfl⟩
-  simp [Array.reverse_append]
-
-@[simp] theorem reverse_eq_append_iff {xs : Vector α (n + m)} {ys : Vector α n} {zs : Vector α m} :
-    xs.reverse = ys ++ zs ↔ xs = (zs.reverse ++ ys.reverse).cast (by omega) := by
-  cases xs
-  cases ys
-  cases zs
-  simp
-
-/-- Reversing a flatten is the same as reversing the order of parts and reversing all parts. -/
-theorem reverse_flatten (L : Vector (Vector α m) n) :
-    L.flatten.reverse = (L.map reverse).reverse.flatten := by
-  cases L using vector₂_induction
-  simp [Array.reverse_flatten]
-
-/-- Flattening a reverse is the same as reversing all parts and reversing the flattened result. -/
-theorem flatten_reverse (L : Vector (Vector α m) n) :
-    L.reverse.flatten = (L.map reverse).flatten.reverse := by
-  cases L using vector₂_induction
-  simp [Array.flatten_reverse]
-
-theorem reverse_flatMap {β} (l : Vector α n) (f : α → Vector β m) :
-    (l.flatMap f).reverse = l.reverse.flatMap (reverse ∘ f) := by
-  rcases l with ⟨l, rfl⟩
-  simp [Array.reverse_flatMap, Function.comp_def]
-
-theorem flatMap_reverse {β} (l : Vector α n) (f : α → Vector β m) :
-    (l.reverse.flatMap f) = (l.flatMap (reverse ∘ f)).reverse := by
-  rcases l with ⟨l, rfl⟩
-  simp [Array.flatMap_reverse, Function.comp_def]
-
-@[simp] theorem reverse_mkVector (n) (a : α) : reverse (mkVector n a) = mkVector n a := by
-  rw [← toArray_inj]
-  simp
-
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/
 
 @[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
@@ -1963,6 +1877,13 @@ theorem swap_comm (a : Vector α n) {i j : Nat} {hi hj} :
   cases a
   simp
 
+/-! ### reverse -/
+
+@[simp] theorem getElem_reverse (a : Vector α n) (i : Nat) (hi : i < n) :
+    (a.reverse)[i] = a[n - 1 - i] := by
+  rcases a with ⟨a, rfl⟩
+  simp
+
 /-! ### Decidable quantifiers. -/
 
 theorem forall_zero_iff {P : Vector α 0 → Prop} :

src/Init/Grind/Norm.lean

@@ -12,105 +12,116 @@ import Init.ByCases
 namespace Lean.Grind
 /-!
 Normalization theorems for the `grind` tactic.
+
+We are also going to use simproc's in the future.
 -/
 
-theorem iff_eq (p q : Prop) : (p ↔ q) = (p = q) := by
+-- Not
+attribute [grind_norm] Classical.not_not
+
+-- Ne
+attribute [grind_norm] ne_eq
+
+-- Iff
+@[grind_norm] theorem iff_eq (p q : Prop) : (p ↔ q) = (p = q) := by
   by_cases p <;> by_cases q <;> simp [*]
 
-theorem eq_true_eq (p : Prop) : (p = True) = p := by simp
-theorem eq_false_eq (p : Prop) : (p = False) = ¬p := by simp
-theorem not_eq_prop (p q : Prop) : (¬(p = q)) = (p = ¬q) := by
+-- Eq
+attribute [grind_norm] eq_self heq_eq_eq
+
+-- Prop equality
+@[grind_norm] theorem eq_true_eq (p : Prop) : (p = True) = p := by simp
+@[grind_norm] theorem eq_false_eq (p : Prop) : (p = False) = ¬p := by simp
+@[grind_norm] theorem not_eq_prop (p q : Prop) : (¬(p = q)) = (p = ¬q) := by
   by_cases p <;> by_cases q <;> simp [*]
 
+-- True
+attribute [grind_norm] not_true
+
+-- False
+attribute [grind_norm] not_false_eq_true
+
 -- Remark: we disabled the following normalization rule because we want this information when implementing splitting heuristics
 -- Implication as a clause
 theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
   by_cases p <;> by_cases q <;> simp [*]
 
-theorem true_imp_eq (p : Prop) : (True → p) = p := by simp
-theorem false_imp_eq (p : Prop) : (False → p) = True := by simp
-theorem imp_true_eq (p : Prop) : (p → True) = True := by simp
-theorem imp_false_eq (p : Prop) : (p → False) = ¬p := by simp
-theorem imp_self_eq (p : Prop) : (p → p) = True := by simp
+@[grind_norm] theorem true_imp_eq (p : Prop) : (True → p) = p := by simp
+@[grind_norm] theorem false_imp_eq (p : Prop) : (False → p) = True := by simp
+@[grind_norm] theorem imp_true_eq (p : Prop) : (p → True) = True := by simp
+@[grind_norm] theorem imp_false_eq (p : Prop) : (p → False) = ¬p := by simp
+@[grind_norm] theorem imp_self_eq (p : Prop) : (p → p) = True := by simp
 
-theorem not_and (p q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q) := by
+-- And
+@[grind_norm↓] theorem not_and (p q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q) := by
   by_cases p <;> by_cases q <;> simp [*]
+attribute [grind_norm] and_true true_and and_false false_and and_assoc
 
-theorem not_ite {_ : Decidable p} (q r : Prop) : (¬ite p q r) = ite p (¬q) (¬r) := by
+-- Or
+attribute [grind_norm↓] not_or
+attribute [grind_norm] or_true true_or or_false false_or or_assoc
+
+-- ite
+attribute [grind_norm] ite_true ite_false
+@[grind_norm↓] theorem not_ite {_ : Decidable p} (q r : Prop) : (¬ite p q r) = ite p (¬q) (¬r) := by
   by_cases p <;> simp [*]
 
-theorem ite_true_false {_ : Decidable p} : (ite p True False) = p := by
+@[grind_norm] theorem ite_true_false {_ : Decidable p} : (ite p True False) = p := by
   by_cases p <;> simp
 
-theorem ite_false_true {_ : Decidable p} : (ite p False True) = ¬p := by
+@[grind_norm] theorem ite_false_true {_ : Decidable p} : (ite p False True) = ¬p := by
   by_cases p <;> simp
 
-theorem not_forall (p : α → Prop) : (¬∀ x, p x) = ∃ x, ¬p x := by simp
+-- Forall
+@[grind_norm↓] theorem not_forall (p : α → Prop) : (¬∀ x, p x) = ∃ x, ¬p x := by simp
+attribute [grind_norm] forall_and
 
-theorem not_exists (p : α → Prop) : (¬∃ x, p x) = ∀ x, ¬p x := by simp
+-- Exists
+@[grind_norm↓] theorem not_exists (p : α → Prop) : (¬∃ x, p x) = ∀ x, ¬p x := by simp
+attribute [grind_norm] exists_const exists_or exists_prop exists_and_left exists_and_right
 
-theorem cond_eq_ite (c : Bool) (a b : α) : cond c a b = ite c a b := by
+-- Bool cond
+@[grind_norm] theorem cond_eq_ite (c : Bool) (a b : α) : cond c a b = ite c a b := by
   cases c <;> simp [*]
 
-theorem Nat.lt_eq (a b : Nat) : (a < b) = (a + 1 ≤ b) := by
+-- Bool or
+attribute [grind_norm]
+  Bool.or_false Bool.or_true Bool.false_or Bool.true_or Bool.or_eq_true Bool.or_assoc
+
+-- Bool and
+attribute [grind_norm]
+  Bool.and_false Bool.and_true Bool.false_and Bool.true_and Bool.and_eq_true Bool.and_assoc
+
+-- Bool not
+attribute [grind_norm]
+  Bool.not_not
+
+-- beq
+attribute [grind_norm] beq_iff_eq
+
+-- bne
+attribute [grind_norm] bne_iff_ne
+
+-- Bool not eq true/false
+attribute [grind_norm] Bool.not_eq_true Bool.not_eq_false
+
+-- decide
+attribute [grind_norm] decide_eq_true_eq decide_not not_decide_eq_true
+
+-- Nat LE
+attribute [grind_norm] Nat.le_zero_eq
+
+-- Nat/Int LT
+@[grind_norm] theorem Nat.lt_eq (a b : Nat) : (a < b) = (a + 1 ≤ b) := by
   simp [Nat.lt, LT.lt]
 
-theorem Int.lt_eq (a b : Int) : (a < b) = (a + 1 ≤ b) := by
+@[grind_norm] theorem Int.lt_eq (a b : Int) : (a < b) = (a + 1 ≤ b) := by
   simp [Int.lt, LT.lt]
 
-theorem ge_eq [LE α] (a b : α) : (a ≥ b) = (b ≤ a) := rfl
-theorem gt_eq [LT α] (a b : α) : (a > b) = (b < a) := rfl
+-- GT GE
+attribute [grind_norm] GT.gt GE.ge
 
-init_grind_norm
-  /- Pre theorems -/
-  not_and not_or not_ite not_forall not_exists
-  |
-  /- Post theorems -/
-  Classical.not_not
-  ne_eq iff_eq eq_self heq_eq_eq
-  -- Prop equality
-  eq_true_eq eq_false_eq not_eq_prop
-  -- True
-  not_true
-  -- False
-  not_false_eq_true
-  -- Implication
-  true_imp_eq false_imp_eq imp_true_eq imp_false_eq imp_self_eq
-  -- And
-  and_true true_and and_false false_and and_assoc
-  -- Or
-  or_true true_or or_false false_or or_assoc
-  -- ite
-  ite_true ite_false ite_true_false ite_false_true
-  -- Forall
-  forall_and
-  -- Exists
-  exists_const exists_or exists_prop exists_and_left exists_and_right
-  -- Bool cond
-  cond_eq_ite
-  -- Bool or
-  Bool.or_false Bool.or_true Bool.false_or Bool.true_or Bool.or_eq_true Bool.or_assoc
-  -- Bool and
-  Bool.and_false Bool.and_true Bool.false_and Bool.true_and Bool.and_eq_true Bool.and_assoc
-  -- Bool not
-  Bool.not_not
-  -- beq
-  beq_iff_eq
-  -- bne
-  bne_iff_ne
-  -- Bool not eq true/false
-  Bool.not_eq_true Bool.not_eq_false
-  -- decide
-  decide_eq_true_eq decide_not not_decide_eq_true
-  -- Nat LE
-  Nat.le_zero_eq
-  -- Nat/Int LT
-  Nat.lt_eq
-  -- Nat.succ
-  Nat.succ_eq_add_one
-  -- Int
-  Int.lt_eq
-  -- GT GE
-  ge_eq gt_eq
+-- Succ
+attribute [grind_norm] Nat.succ_eq_add_one
 
 end Lean.Grind

src/Init/Grind/Tactics.lean

@@ -14,9 +14,7 @@ syntax grindEqRhs  := atomic("=" "_")
 syntax grindBwd    := "←"
 syntax grindFwd    := "→"
 
-syntax grindThmMod := grindEqBoth <|> grindEqRhs <|> grindEq <|> grindBwd <|> grindFwd
-
-syntax (name := grind) "grind" (grindThmMod)? : attr
+syntax (name := grind) "grind" (grindEqBoth <|> grindEqRhs <|> grindEq <|> grindBwd <|> grindFwd)? : attr
 
 end Lean.Parser.Attr
 
@@ -51,8 +49,6 @@ structure Config where
   failures : Nat := 1
   /-- Maximum number of heartbeats (in thousands) the canonicalizer can spend per definitional equality test. -/
   canonHeartbeats : Nat := 1000
-  /-- If `ext` is `true`, `grind` uses extensionality theorems available in the environment. -/
-  ext : Bool := true
   deriving Inhabited, BEq
 
 end Lean.Grind
@@ -63,13 +59,7 @@ namespace Lean.Parser.Tactic
 `grind` tactic and related tactics.
 -/
 
-syntax grindErase := "-" ident
-syntax grindLemma := (Attr.grindThmMod)? ident
-syntax grindParam := grindErase <|> grindLemma
-
-syntax (name := grind)
-  "grind" optConfig (&" only")?
-  (" [" withoutPosition(grindParam,*) "]")?
-  ("on_failure " term)? : tactic
+-- TODO: parameters
+syntax (name := grind) "grind" optConfig ("on_failure " term)? : tactic
 
 end Lean.Parser.Tactic

src/Init/Prelude.lean

@@ -150,9 +150,6 @@ It can also be written as `()`.
 /-- Marker for information that has been erased by the code generator. -/
 unsafe axiom lcErased : Type
 
-/-- Marker for type dependency that has been erased by the code generator. -/
-unsafe axiom lcAny : Type
-
 /--
 Auxiliary unsafe constant used by the Compiler when erasing proofs from code.
 

src/Init/Tactics.lean

@@ -1648,6 +1648,17 @@ If there are several with the same priority, it is uses the "most recent one". E
 -/
 syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
 
+/--
+Theorems tagged with the `grind_norm` attribute are used by the `grind` tactic normalizer/pre-processor.
+-/
+syntax (name := grind_norm) "grind_norm" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
+
+/--
+Simplification procedures tagged with the `grind_norm_proc` attribute are used by the `grind` tactic normalizer/pre-processor.
+-/
+syntax (name := grind_norm_proc) "grind_norm_proc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
+
+
 /-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`. -/
 syntax normCastLabel := &"elim" <|> &"move" <|> &"squash"
 

src/Lean/AddDecl.lean

@@ -14,54 +14,21 @@ register_builtin_option debug.skipKernelTC : Bool := {
   descr    := "skip kernel type checker. WARNING: setting this option to true may compromise soundness because your proofs will not be checked by the Lean kernel"
 }
 
-/-- Adds given declaration to the environment, respecting `debug.skipKernelTC`. -/
-def Kernel.Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration)
-    (cancelTk? : Option IO.CancelToken := none) : Except Exception Environment :=
+def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration)
+    (cancelTk? : Option IO.CancelToken := none) : Except KernelException Environment :=
   if debug.skipKernelTC.get opts then
     addDeclWithoutChecking env decl
   else
     addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl cancelTk?
 
-private def Environment.addDeclAux (env : Environment) (opts : Options) (decl : Declaration)
-    (cancelTk? : Option IO.CancelToken := none) : Except Kernel.Exception Environment :=
-  env.addDeclCore (Core.getMaxHeartbeats opts).toUSize decl cancelTk? (!debug.skipKernelTC.get opts)
-
-@[deprecated "use `Lean.addDecl` instead to ensure new namespaces are registered" (since := "2024-12-03")]
-def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration)
-    (cancelTk? : Option IO.CancelToken := none) : Except Kernel.Exception Environment :=
-  Environment.addDeclAux env opts decl cancelTk?
-
-private def isNamespaceName : Name → Bool
-  | .str .anonymous _ => true
-  | .str p _          => isNamespaceName p
-  | _                 => false
-
-private def registerNamePrefixes (env : Environment) (name : Name) : Environment :=
-  match name with
-    | .str _ s =>
-      if s.get 0 == '_' then
-        -- Do not register namespaces that only contain internal declarations.
-        env
-      else
-        go env name
-    | _ => env
-where go env
-  | .str p _ => if isNamespaceName p then go (env.registerNamespace p) p else env
-  | _        => env
-
 def addDecl (decl : Declaration) : CoreM Unit := do
   profileitM Exception "type checking" (← getOptions) do
-    let mut env ← withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
+    withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
       if !(← MonadLog.hasErrors) && decl.hasSorry then
         logWarning "declaration uses 'sorry'"
-      (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk? |> ofExceptKernelException
-
-    -- register namespaces for newly added constants; this used to be done by the kernel itself
-    -- but that is incompatible with moving it to a separate task
-    env := decl.getNames.foldl registerNamePrefixes env
-    if let .inductDecl _ _ types _ := decl then
-      env := types.foldl (registerNamePrefixes · <| ·.name ++ `rec) env
-    setEnv env
+      match (← getEnv).addDecl (← getOptions) decl (← read).cancelTk? with
+      | .ok    env => setEnv env
+      | .error ex  => throwKernelException ex
 
 def addAndCompile (decl : Declaration) : CoreM Unit := do
   addDecl decl

src/Lean/Compiler/LCNF/ToMono.lean

@@ -150,7 +150,18 @@ where
 
 def toMono : Pass where
   name     := `toMono
-  run      := (·.mapM (·.toMono))
+  run      := fun decls => do
+    let decls ← decls.filterM fun decl => do
+      if hasLocalInst decl.type then
+        /-
+        Declaration is a "template" for the code specialization pass.
+        So, we should delete it before going to next phase.
+        -/
+        decl.erase
+        return false
+      else
+        return true
+    decls.mapM (·.toMono)
   phase    := .base
   phaseOut := .mono
 

src/Lean/CoreM.lean

@@ -515,7 +515,7 @@ register_builtin_option compiler.enableNew : Bool := {
 opaque compileDeclsNew (declNames : List Name) : CoreM Unit
 
 @[extern "lean_compile_decls"]
-opaque compileDeclsOld (env : Environment) (opt : @& Options) (decls : @& List Name) : Except Kernel.Exception Environment
+opaque compileDeclsOld (env : Environment) (opt : @& Options) (decls : @& List Name) : Except KernelException Environment
 
 def compileDecl (decl : Declaration) : CoreM Unit := do
   let opts ← getOptions
@@ -526,7 +526,7 @@ def compileDecl (decl : Declaration) : CoreM Unit := do
     return compileDeclsOld (← getEnv) opts decls
   match res with
   | Except.ok env => setEnv env
-  | Except.error (.other msg) =>
+  | Except.error (KernelException.other msg) =>
     checkUnsupported decl -- Generate nicer error message for unsupported recursors and axioms
     throwError msg
   | Except.error ex =>
@@ -538,7 +538,7 @@ def compileDecls (decls : List Name) : CoreM Unit := do
     compileDeclsNew decls
   match compileDeclsOld (← getEnv) opts decls with
   | Except.ok env   => setEnv env
-  | Except.error (.other msg) =>
+  | Except.error (KernelException.other msg) =>
     throwError msg
   | Except.error ex =>
     throwKernelException ex

src/Lean/Data/NameTrie.lean

@@ -54,10 +54,6 @@ instance : EmptyCollection (NameTrie β) where
 def NameTrie.find? (t : NameTrie β) (k : Name) : Option β :=
   PrefixTree.find? t (toKey k)
 
-@[inline, inherit_doc PrefixTree.findLongestPrefix?]
-def NameTrie.findLongestPrefix? (t : NameTrie β) (k : Name) : Option β :=
-  PrefixTree.findLongestPrefix? t (toKey k)
-
 @[inline]
 def NameTrie.foldMatchingM [Monad m] (t : NameTrie β) (k : Name) (init : σ) (f : β → σ → m σ) : m σ :=
   PrefixTree.foldMatchingM t (toKey k) init f

src/Lean/Data/PrefixTree.lean

@@ -48,17 +48,6 @@ partial def find? (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k :
       | some t => loop t ks
   loop t k
 
-/-- Returns the the value of the longest key in `t` that is a prefix of `k`, if any. -/
-@[specialize]
-partial def findLongestPrefix? (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k : List α) : Option β :=
-  let rec loop acc?
-    | PrefixTreeNode.Node val _, [] => val <|> acc?
-    | PrefixTreeNode.Node val m, k :: ks =>
-      match RBNode.find cmp m k with
-      | none   => val
-      | some t => loop (val <|> acc?) t ks
-  loop none t k
-
 @[specialize]
 partial def foldMatchingM [Monad m] (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k : List α) (init : σ) (f : β → σ → m σ) : m σ :=
   let rec fold : PrefixTreeNode α β → σ → m σ
@@ -103,10 +92,6 @@ def PrefixTree.insert (t : PrefixTree α β p) (k : List α) (v : β) : PrefixTr
 def PrefixTree.find? (t : PrefixTree α β p) (k : List α) : Option β :=
   t.val.find? p k
 
-@[inline, inherit_doc PrefixTreeNode.findLongestPrefix?]
-def PrefixTree.findLongestPrefix? (t : PrefixTree α β p) (k : List α) : Option β :=
-  t.val.findLongestPrefix? p k
-
 @[inline]
 def PrefixTree.foldMatchingM [Monad m] (t : PrefixTree α β p) (k : List α) (init : σ) (f : β → σ → m σ) : m σ :=
   t.val.foldMatchingM p k init f

src/Lean/Declaration.lean

@@ -193,19 +193,6 @@ def Declaration.definitionVal! : Declaration → DefinitionVal
   | .defnDecl val => val
   | _ => panic! "Expected a `Declaration.defnDecl`."
 
-/--
-Returns all top-level names to be defined by adding this declaration to the environment. This does
-not include auxiliary definitions such as projections.
--/
-def Declaration.getNames : Declaration → List Name
-  | .axiomDecl val          => [val.name]
-  | .defnDecl val           => [val.name]
-  | .thmDecl val            => [val.name]
-  | .opaqueDecl val         => [val.name]
-  | .quotDecl               => [``Quot, ``Quot.mk, ``Quot.lift, ``Quot.ind]
-  | .mutualDefnDecl defns   => defns.map (·.name)
-  | .inductDecl _ _ types _ => types.map (·.name)
-
 @[specialize] def Declaration.foldExprM {α} {m : Type → Type} [Monad m] (d : Declaration) (f : α → Expr → m α) (a : α) : m α :=
   match d with
   | .quotDecl                                        => pure a
@@ -482,10 +469,6 @@ def isInductive : ConstantInfo → Bool
   | .inductInfo _ => true
   | _             => false
 
-def isDefinition : ConstantInfo → Bool
-  | .defnInfo _ => true
-  | _           => false
-
 def isTheorem : ConstantInfo → Bool
   | .thmInfo _ => true
   | _          => false

src/Lean/Elab/BuiltinCommand.lean

@@ -124,7 +124,9 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
   n[1].forArgsM addUnivLevel
 
 @[builtin_command_elab «init_quot»] def elabInitQuot : CommandElab := fun _ => do
-  liftCoreM <| addDecl Declaration.quotDecl
+  match (← getEnv).addDecl (← getOptions) Declaration.quotDecl with
+  | Except.ok env   => setEnv env
+  | Except.error ex => throwError (ex.toMessageData (← getOptions))
 
 @[builtin_command_elab «export»] def elabExport : CommandElab := fun stx => do
   let `(export $ns ($ids*)) := stx | throwUnsupportedSyntax
@@ -292,7 +294,7 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
     modify fun s => { s with messages := {} };
     pure messages
   let restoreMessages (prevMessages : MessageLog) : CommandElabM Unit := do
-    modify fun s => { s with messages := prevMessages ++ s.messages.errorsToInfos }
+    modify fun s => { s with messages := prevMessages ++ s.messages.errorsToWarnings }
   let prevMessages ← resetMessages
   let succeeded ← try
     x

src/Lean/Elab/Structure.lean

@@ -681,7 +681,7 @@ private partial def checkResultingUniversesForFields (fieldInfos : Array StructF
       throwErrorAt info.ref msg
 
 @[extern "lean_mk_projections"]
-private opaque mkProjections (env : Environment) (structName : Name) (projs : List Name) (isClass : Bool) : Except Kernel.Exception Environment
+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
   if r.type.isProp then

src/Lean/Elab/Tactic/Ext.lean

@@ -5,7 +5,6 @@ Authors: Gabriel Ebner, Mario Carneiro
 -/
 prelude
 import Init.Ext
-import Lean.Meta.Tactic.Ext
 import Lean.Elab.DeclarationRange
 import Lean.Elab.Tactic.RCases
 import Lean.Elab.Tactic.Repeat
@@ -175,8 +174,65 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do
 ### Attribute
 -/
 
-abbrev extExtension := Meta.Ext.extExtension
-abbrev getExtTheorems := Meta.Ext.getExtTheorems
+/-- Information about an extensionality theorem, stored in the environment extension. -/
+structure ExtTheorem where
+  /-- Declaration name of the extensionality theorem. -/
+  declName : Name
+  /-- Priority of the extensionality theorem. -/
+  priority : Nat
+  /--
+  Key in the discrimination tree,
+  for the type in which the extensionality theorem holds.
+  -/
+  keys : Array DiscrTree.Key
+  deriving Inhabited, Repr, BEq, Hashable
+
+/-- The state of the `ext` extension environment -/
+structure ExtTheorems where
+  /-- The tree of `ext` extensions. -/
+  tree   : DiscrTree ExtTheorem := {}
+  /-- Erased `ext`s via `attribute [-ext]`. -/
+  erased  : PHashSet Name := {}
+  deriving Inhabited
+
+/-- The environment extension to track `@[ext]` theorems. -/
+builtin_initialize extExtension :
+    SimpleScopedEnvExtension ExtTheorem ExtTheorems ←
+  registerSimpleScopedEnvExtension {
+    addEntry := fun { tree, erased } thm =>
+      { tree := tree.insertCore thm.keys thm, erased := erased.erase thm.declName }
+    initial := {}
+  }
+
+/-- Gets the list of `@[ext]` theorems corresponding to the key `ty`,
+ordered from high priority to low. -/
+@[inline] def getExtTheorems (ty : Expr) : MetaM (Array ExtTheorem) := do
+  let extTheorems := extExtension.getState (← getEnv)
+  let arr ← extTheorems.tree.getMatch ty
+  let erasedArr := arr.filter fun thm => !extTheorems.erased.contains thm.declName
+  -- Using insertion sort because it is stable and the list of matches should be mostly sorted.
+  -- Most ext theorems have default priority.
+  return erasedArr.insertionSort (·.priority < ·.priority) |>.reverse
+
+/--
+Erases a name marked `ext` by adding it to the state's `erased` field and
+removing it from the state's list of `Entry`s.
+
+This is triggered by `attribute [-ext] name`.
+-/
+def ExtTheorems.eraseCore (d : ExtTheorems) (declName : Name) : ExtTheorems :=
+ { d with erased := d.erased.insert declName }
+
+/--
+Erases a name marked as a `ext` attribute.
+Check that it does in fact have the `ext` attribute by making sure it names a `ExtTheorem`
+found somewhere in the state's tree, and is not erased.
+-/
+def ExtTheorems.erase [Monad m] [MonadError m] (d : ExtTheorems) (declName : Name) :
+    m ExtTheorems := do
+  unless d.tree.containsValueP (·.declName == declName) && !d.erased.contains declName do
+    throwError "'{declName}' does not have [ext] attribute"
+  return d.eraseCore declName
 
 builtin_initialize registerBuiltinAttribute {
   name := `ext

src/Lean/Elab/Tactic/Grind.lean

@@ -34,67 +34,8 @@ def elabGrindPattern : CommandElab := fun stx => do
         Grind.addEMatchTheorem declName xs.size patterns.toList
   | _ => throwUnsupportedSyntax
 
-open Command Term in
-@[builtin_command_elab Lean.Parser.Command.initGrindNorm]
-def elabInitGrindNorm : CommandElab := fun stx =>
-  match stx with
-  | `(init_grind_norm $pre:ident* | $post*) =>
-    Command.liftTermElabM do
-      let pre ← pre.mapM fun id => realizeGlobalConstNoOverloadWithInfo id
-      let post ← post.mapM fun id => realizeGlobalConstNoOverloadWithInfo id
-      Grind.registerNormTheorems pre post
-  | _ => throwUnsupportedSyntax
-
-def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.grindParam) : MetaM Grind.Params := do
-  let mut params := params
-  for p in ps do
-    match p with
-    | `(Parser.Tactic.grindParam| - $id:ident) =>
-      let declName ← realizeGlobalConstNoOverloadWithInfo id
-      if (← isInductivePredicate declName) then
-        throwErrorAt p "NIY"
-      else
-        params := { params with ematch := (← params.ematch.eraseDecl declName) }
-    | `(Parser.Tactic.grindParam| $[$mod?:grindThmMod]? $id:ident) =>
-      let declName ← realizeGlobalConstNoOverloadWithInfo id
-      let kind ← if let some mod := mod? then Grind.getTheoremKindCore mod else pure .default
-      if (← isInductivePredicate declName) then
-        throwErrorAt p "NIY"
-      else
-        let info ← getConstInfo declName
-        match info with
-        | .thmInfo _ =>
-          if kind == .eqBoth then
-            params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqLhs) }
-            params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqRhs) }
-          else
-            params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName kind) }
-        | .defnInfo _ =>
-          if (← isReducible declName) then
-            throwErrorAt p "`{declName}` is a reducible definition, `grind` automatically unfolds them"
-          if kind != .eqLhs && kind != .default then
-            throwErrorAt p "invalid `grind` parameter, `{declName}` is a definition, the only acceptable (and redundant) modifier is '='"
-          let some thms ← Grind.mkEMatchEqTheoremsForDef? declName
-            | throwErrorAt p "failed to genereate equation theorems for `{declName}`"
-          params := { params with extra := params.extra ++ thms.toPArray' }
-        | _ =>
-          throwErrorAt p "invalid `grind` parameter, `{declName}` is not a theorem, definition, or inductive type"
-    | _ => throwError "unexpected `grind` parameter{indentD p}"
-  return params
-
-def mkGrindParams (config : Grind.Config) (only : Bool) (ps :  TSyntaxArray ``Parser.Tactic.grindParam) : MetaM Grind.Params := do
-  let params ← Grind.mkParams config
-  let ematch ← if only then pure {} else Grind.getEMatchTheorems
-  let params := { params with ematch }
-  elabGrindParams params ps
-
-def grind
-    (mvarId : MVarId) (config : Grind.Config)
-    (only : Bool)
-    (ps   :  TSyntaxArray ``Parser.Tactic.grindParam)
-    (mainDeclName : Name) (fallback : Grind.Fallback) : MetaM Unit := do
-  let params ← mkGrindParams config only ps
-  let goals ← Grind.main mvarId params mainDeclName fallback
+def grind (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Grind.Fallback) : MetaM Unit := do
+  let goals ← Grind.main mvarId config mainDeclName fallback
   unless goals.isEmpty do
     throwError "`grind` failed\n{← Grind.goalsToMessageData goals config}"
 
@@ -115,16 +56,14 @@ private def elabFallback (fallback? : Option Term) : TermElabM (Grind.GoalM Unit
     pure auxDeclName
   unsafe evalConst (Grind.GoalM Unit) auxDeclName
 
-@[builtin_tactic Lean.Parser.Tactic.grind] def evalGrind : Tactic := fun stx => do
+@[builtin_tactic Lean.Parser.Tactic.grind] def evalApplyRfl : Tactic := fun stx => do
   match stx with
-  | `(tactic| grind $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
+  | `(tactic| grind $config:optConfig $[on_failure $fallback?]?) =>
     let fallback ← elabFallback fallback?
-    let only := only.isSome
-    let params := if let some params := params then params.getElems else #[]
     logWarningAt stx "The `grind` tactic is experimental and still under development. Avoid using it in production projects"
     let declName := (← Term.getDeclName?).getD `_grind
     let config ← elabGrindConfig config
-    withMainContext do liftMetaFinishingTactic (grind · config only params declName fallback)
+    withMainContext do liftMetaFinishingTactic (grind · config declName fallback)
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic

src/Lean/Environment.lean

@@ -7,10 +7,8 @@ prelude
 import Init.Control.StateRef
 import Init.Data.Array.BinSearch
 import Init.Data.Stream
-import Init.System.Promise
 import Lean.ImportingFlag
 import Lean.Data.HashMap
-import Lean.Data.NameTrie
 import Lean.Data.SMap
 import Lean.Declaration
 import Lean.LocalContext
@@ -18,50 +16,6 @@ import Lean.Util.Path
 import Lean.Util.FindExpr
 import Lean.Util.Profile
 import Lean.Util.InstantiateLevelParams
-import Lean.PrivateName
-
-/-!
-# Note [Environment Branches]
-
-The kernel environment type `Lean.Kernel.Environment` enforces a linear order on the addition of
-declarations: `addDeclCore` takes an environment and returns a new one, assuming type checking
-succeeded. On the other hand, the metaprogramming-level `Lean.Environment` wrapper must allow for
-*branching* environment transformations so that multiple declarations can be elaborated
-concurrently while still being able to access information about preceding declarations that have
-also been branched out as soon as they are available.
-
-The basic function to introduce such branches is `addConstAsync`, which takes an environment and
-returns a structure containing two environments: one for the "main" branch that can be used in
-further branching and eventually contains all the declarations of the file and one for the "async"
-branch that can be used concurrently to the main branch to elaborate and add the declaration for
-which the branch was introduced. Branches are "joined" back together implicitly via the kernel
-environment, which as mentioned cannot be changed concurrently: when the main branch first tries to
-access it, evaluation is blocked until the kernel environment on the async branch is complete.
-Thus adding two declarations A and B concurrently can be visualized like this:
-```text
-o addConstAsync A
-|\
-| \
-|  \
-o addConstAsync B
-|\   \
-| \   o elaborate A
-|  \  |
-|   o elaborate B
-|   | |
-|   | o addDeclCore A
-|   |/
-|   o addDeclCore B
-|  /
-| /
-|/
-o .olean serialization calls Environment.toKernelEnv
-```
-While each edge represents a `Lean.Environment` that has its own view of the state of the module,
-the kernel environment really lives only in the right-most path, with all other paths merely holding
-an unfulfilled `Task` representing it and where forcing that task leads to the back-edges joining
-paths back together.
--/
 
 namespace Lean
 /-- Opaque environment extension state. -/
@@ -134,6 +88,11 @@ structure EnvironmentHeader where
   -/
   trustLevel   : UInt32       := 0
   /--
+  `quotInit = true` if the command `init_quot` has already been executed for the environment, and
+  `Quot` declarations have been added to the environment.
+  -/
+  quotInit     : Bool         := false
+  /--
   Name of the module being compiled.
   -/
   mainModule   : Name         := default
@@ -147,15 +106,6 @@ structure EnvironmentHeader where
   moduleData   : Array ModuleData := #[]
   deriving Nonempty
 
-namespace Kernel
-
-structure Diagnostics where
-  /-- Number of times each declaration has been unfolded by the kernel. -/
-  unfoldCounter : PHashMap Name Nat := {}
-  /-- If `enabled = true`, kernel records declarations that have been unfolded. -/
-  enabled : Bool := false
-  deriving Inhabited
-
 /--
 An environment stores declarations provided by the user. The kernel
 currently supports different kinds of declarations such as definitions, theorems,
@@ -171,33 +121,10 @@ declared by users are stored in an environment extension. Users can declare new
 using meta-programming.
 -/
 structure Environment where
-  /--
-  The constructor of `Environment` is private to protect against modification that bypasses the
-  kernel.
-  -/
+  /-- The constructor of `Environment` is private to protect against modification
+  that bypasses the kernel. -/
   private mk ::
   /--
-  Mapping from constant name to `ConstantInfo`. It contains all constants (definitions, theorems,
-  axioms, etc) that have been already type checked by the kernel.
-  -/
-  constants   : ConstMap
-  /--
-  `quotInit = true` if the command `init_quot` has already been executed for the environment, and
-  `Quot` declarations have been added to the environment. When the flag is set, the type checker can
-  assume that the `Quot` declarations in the environment have indeed been added by the kernel and
-  not by the user.
-  -/
-  quotInit    : Bool := false
-  /--
-  Diagnostic information collected during kernel execution.
-
-  Remark: We store kernel diagnostic information in an environment field to simplify the interface
-  with the kernel implemented in C/C++. Thus, we can only track declarations in methods, such as
-  `addDecl`, which return a new environment. `Kernel.isDefEq` and `Kernel.whnf` do not update the
-  statistics. We claim this is ok since these methods are mainly used for debugging.
-  -/
-  diagnostics : Diagnostics := {}
-  /--
   Mapping from constant name to module (index) where constant has been declared.
   Recall that a Lean file has a header where previously compiled modules can be imported.
   Each imported module has a unique `ModuleIdx`.
@@ -207,23 +134,96 @@ structure Environment where
   the field `constants`. These auxiliary constants are invisible to the Lean kernel and elaborator.
   Only the code generator uses them.
   -/
-  const2ModIdx            : Std.HashMap Name ModuleIdx
+  const2ModIdx : Std.HashMap Name ModuleIdx
+  /--
+  Mapping from constant name to `ConstantInfo`. It contains all constants (definitions, theorems, axioms, etc)
+  that have been already type checked by the kernel.
+  -/
+  constants    : ConstMap
   /--
   Environment extensions. It also includes user-defined extensions.
   -/
-  private extensions      : Array EnvExtensionState
+  extensions   : Array EnvExtensionState
   /--
   Constant names to be saved in the field `extraConstNames` at `ModuleData`.
   It contains auxiliary declaration names created by the code generator which are not in `constants`.
   When importing modules, we want to insert them at `const2ModIdx`.
   -/
-  private extraConstNames : NameSet
-  /-- The header contains additional information that is set at import time. -/
-  header                  : EnvironmentHeader := {}
-deriving Nonempty
+  extraConstNames : NameSet
+  /-- The header contains additional information that is not updated often. -/
+  header       : EnvironmentHeader := {}
+  deriving Nonempty
 
-/-- Exceptions that can be raised by the kernel when type checking new declarations. -/
-inductive Exception where
+namespace Environment
+
+private def addAux (env : Environment) (cinfo : ConstantInfo) : Environment :=
+  { env with constants := env.constants.insert cinfo.name cinfo }
+
+/--
+Save an extra constant name that is used to populate `const2ModIdx` when we import
+.olean files. We use this feature to save in which module an auxiliary declaration
+created by the code generator has been created.
+-/
+def addExtraName (env : Environment) (name : Name) : Environment :=
+  if env.constants.contains name then
+    env
+  else
+    { env with extraConstNames := env.extraConstNames.insert name }
+
+@[export lean_environment_find]
+def find? (env : Environment) (n : Name) : Option ConstantInfo :=
+  /- It is safe to use `find'` because we never overwrite imported declarations. -/
+  env.constants.find?' n
+
+def contains (env : Environment) (n : Name) : Bool :=
+  env.constants.contains n
+
+def imports (env : Environment) : Array Import :=
+  env.header.imports
+
+def allImportedModuleNames (env : Environment) : Array Name :=
+  env.header.moduleNames
+
+@[export lean_environment_set_main_module]
+def setMainModule (env : Environment) (m : Name) : Environment :=
+  { env with header := { env.header with mainModule := m } }
+
+@[export lean_environment_main_module]
+def mainModule (env : Environment) : Name :=
+  env.header.mainModule
+
+@[export lean_environment_mark_quot_init]
+private def markQuotInit (env : Environment) : Environment :=
+  { env with header := { env.header with quotInit := true } }
+
+@[export lean_environment_quot_init]
+private def isQuotInit (env : Environment) : Bool :=
+  env.header.quotInit
+
+@[export lean_environment_trust_level]
+private def getTrustLevel (env : Environment) : UInt32 :=
+  env.header.trustLevel
+
+def getModuleIdxFor? (env : Environment) (declName : Name) : Option ModuleIdx :=
+  env.const2ModIdx[declName]?
+
+def isConstructor (env : Environment) (declName : Name) : Bool :=
+  match env.find? declName with
+  | some (.ctorInfo _) => true
+  | _                  => false
+
+def isSafeDefinition (env : Environment) (declName : Name) : Bool :=
+  match env.find? declName with
+  | some (.defnInfo { safety := .safe, .. }) => true
+  | _ => false
+
+def getModuleIdx? (env : Environment) (moduleName : Name) : Option ModuleIdx :=
+  env.header.moduleNames.findIdx? (· == moduleName)
+
+end Environment
+
+/-- Exceptions that can be raised by the Kernel when type checking new declarations. -/
+inductive KernelException where
   | unknownConstant  (env : Environment) (name : Name)
   | alreadyDeclared  (env : Environment) (name : Name)
   | declTypeMismatch (env : Environment) (decl : Declaration) (givenType : Expr)
@@ -244,500 +244,21 @@ inductive Exception where
 
 namespace Environment
 
-@[export lean_environment_find]
-def find? (env : Environment) (n : Name) : Option ConstantInfo :=
-  /- It is safe to use `find'` because we never overwrite imported declarations. -/
-  env.constants.find?' n
-
-@[export lean_environment_mark_quot_init]
-private def markQuotInit (env : Environment) : Environment :=
-  { env with quotInit := true }
-
-@[export lean_environment_quot_init]
-private def isQuotInit (env : Environment) : Bool :=
-  env.quotInit
-
-/-- Type check given declaration and add it to the environment -/
+/--
+Type check given declaration and add it to the environment
+-/
 @[extern "lean_add_decl"]
 opaque addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration)
-  (cancelTk? : @& Option IO.CancelToken) : Except Exception Environment
+  (cancelTk? : @& Option IO.CancelToken) : Except KernelException Environment
 
 /--
 Add declaration to kernel without type checking it.
-
 **WARNING** This function is meant for temporarily working around kernel performance issues.
 It compromises soundness because, for example, a buggy tactic may produce an invalid proof,
 and the kernel will not catch it if the new option is set to true.
 -/
 @[extern "lean_add_decl_without_checking"]
-opaque addDeclWithoutChecking (env : Environment) (decl : @& Declaration) : Except Exception Environment
-
-@[export lean_environment_add]
-private def add (env : Environment) (cinfo : ConstantInfo) : Environment :=
-  { env with constants := env.constants.insert cinfo.name cinfo }
-
-@[export lean_kernel_diag_is_enabled]
-def Diagnostics.isEnabled (d : Diagnostics) : Bool :=
-  d.enabled
-
-/-- Enables/disables kernel diagnostics. -/
-def enableDiag (env : Environment) (flag : Bool) : Environment :=
-  { env with diagnostics.enabled := flag }
-
-def isDiagnosticsEnabled (env : Environment) : Bool :=
-  env.diagnostics.enabled
-
-def resetDiag (env : Environment) : Environment :=
-  { env with diagnostics.unfoldCounter := {} }
-
-@[export lean_kernel_record_unfold]
-def Diagnostics.recordUnfold (d : Diagnostics) (declName : Name) : Diagnostics :=
-  if d.enabled then
-    let cNew := if let some c := d.unfoldCounter.find? declName then c + 1 else 1
-    { d with unfoldCounter := d.unfoldCounter.insert declName cNew }
-  else
-    d
-
-@[export lean_kernel_get_diag]
-def getDiagnostics (env : Environment) : Diagnostics :=
-  env.diagnostics
-
-@[export lean_kernel_set_diag]
-def setDiagnostics (env : Environment) (diag : Diagnostics) : Environment :=
-  { env with diagnostics := diag}
-
-end Kernel.Environment
-
-@[deprecated Kernel.Exception (since := "2024-12-12")]
-abbrev KernelException := Kernel.Exception
-
-inductive ConstantKind where
-  | defn | thm | «axiom» | «opaque» | quot | induct | ctor | recursor
-deriving Inhabited, BEq, Repr
-
-def ConstantKind.ofConstantInfo : ConstantInfo → ConstantKind
-  | .defnInfo   _ => .defn
-  | .thmInfo    _ => .thm
-  | .axiomInfo  _ => .axiom
-  | .opaqueInfo _ => .opaque
-  | .quotInfo   _ => .quot
-  | .inductInfo _ => .induct
-  | .ctorInfo   _ => .ctor
-  | .recInfo    _ => .recursor
-
-/-- `ConstantInfo` variant that allows for asynchronous filling of components via tasks. -/
-structure AsyncConstantInfo where
-  /-- The declaration name, known immediately. -/
-  name      : Name
-  /-- The kind of the constant, known immediately. -/
-  kind      : ConstantKind
-  /-- The "signature" including level params and type, potentially filled asynchronously. -/
-  sig       : Task ConstantVal
-  /-- The final, complete constant info, potentially filled asynchronously. -/
-  constInfo : Task ConstantInfo
-
-namespace AsyncConstantInfo
-
-def toConstantVal (c : AsyncConstantInfo) : ConstantVal :=
-  c.sig.get
-
-def toConstantInfo (c : AsyncConstantInfo) : ConstantInfo :=
-  c.constInfo.get
-
-def ofConstantInfo (c : ConstantInfo) : AsyncConstantInfo where
-  name := c.name
-  kind := .ofConstantInfo c
-  sig := .pure c.toConstantVal
-  constInfo := .pure c
-
-end AsyncConstantInfo
-
-/--
-Information about the current branch of the environment representing asynchronous elaboration.
--/
-structure AsyncContext where
-  /--
-  Name of the declaration asynchronous elaboration was started for. All constants added to this
-  environment branch must have the name as a prefix, after erasing macro scopes and private name
-  prefixes.
-  -/
-  declPrefix : Name
-deriving Nonempty
-
-/--
-Checks whether a declaration named `n` may be added to the environment in the given context. See
-also `AsyncContext.declPrefix`.
--/
-def AsyncContext.mayContain (ctx : AsyncContext) (n : Name) : Bool :=
-  ctx.declPrefix.isPrefixOf <| privateToUserName n.eraseMacroScopes
-
-/--
-Constant info and environment extension states eventually resulting from async elaboration.
--/
-structure AsyncConst where
-  constInfo : AsyncConstantInfo
-  /--
-  Reported extension state eventually fulfilled by promise; may be missing for tasks (e.g. kernel
-  checking) that can eagerly guarantee they will not report any state.
-  -/
-  exts?     : Option (Task (Array EnvExtensionState))
-
-/-- Data structure holding a sequence of `AsyncConst`s optimized for efficient access. -/
-structure AsyncConsts where
-  toArray : Array AsyncConst := #[]
-  /-- Map from declaration name to const for fast direct access. -/
-  private map : NameMap AsyncConst := {}
-  /-- Trie of declaration names without private name prefixes for fast longest-prefix access. -/
-  private normalizedTrie : NameTrie AsyncConst := {}
-deriving Inhabited
-
-def AsyncConsts.add (aconsts : AsyncConsts) (aconst : AsyncConst) : AsyncConsts :=
-  { aconsts with
-    toArray := aconsts.toArray.push aconst
-    map := aconsts.map.insert aconst.constInfo.name aconst
-    normalizedTrie := aconsts.normalizedTrie.insert (privateToUserName aconst.constInfo.name) aconst
-  }
-
-def AsyncConsts.find? (aconsts : AsyncConsts) (declName : Name) : Option AsyncConst :=
-  aconsts.map.find? declName
-
-/-- Checks whether the name of any constant in the collection is a prefix of `declName`. -/
-def AsyncConsts.hasPrefix (aconsts : AsyncConsts) (declName : Name) : Bool :=
-  -- as macro scopes are a strict suffix,
-  aconsts.normalizedTrie.findLongestPrefix? (privateToUserName declName.eraseMacroScopes) |>.isSome
-
-/--
-Elaboration-specific extension of `Kernel.Environment` that adds tracking of asynchronously
-elaborated declarations.
--/
-structure Environment where
-  /-
-  Like with `Kernel.Environment`, this constructor is private to protect consistency of the
-  environment, though there are no soundness concerns in this case given that it is used purely for
-  elaboration.
-  -/
-  private mk ::
-  /--
-  Kernel environment not containing any asynchronously elaborated declarations. Also stores
-  environment extension state for the current branch of the environment.
-
-  Ignoring extension state, this is guaranteed to be some prior version of `checked` that is eagerly
-  available. Thus we prefer taking information from it instead of `checked` whenever possible.
-  -/
-  checkedWithoutAsync : Kernel.Environment
-  /--
-  Kernel environment task that is fulfilled when all asynchronously elaborated declarations are
-  finished, containing the resulting environment. Also collects the environment extension state of
-  all environment branches that contributed contained declarations.
-  -/
-  checked             : Task Kernel.Environment := .pure checkedWithoutAsync
-  /--
-  Container of asynchronously elaborated declarations, i.e.
-  `checked = checkedWithoutAsync ⨃ asyncConsts`.
-  -/
-  private asyncConsts : AsyncConsts := {}
-  /-- Information about this asynchronous branch of the environment, if any. -/
-  private asyncCtx?   : Option AsyncContext := none
-deriving Nonempty
-
-namespace Environment
-
-@[export lean_elab_environment_of_kernel_env]
-def ofKernelEnv (env : Kernel.Environment) : Environment :=
-  { checkedWithoutAsync := env }
-
-@[export lean_elab_environment_to_kernel_env]
-def toKernelEnv (env : Environment) : Kernel.Environment :=
-  env.checked.get
-
-/-- Consistently updates synchronous and asynchronous parts of the environment without blocking. -/
-private def modifyCheckedAsync (env : Environment) (f : Kernel.Environment → Kernel.Environment) : Environment :=
-  { env with checked := env.checked.map (sync := true) f, checkedWithoutAsync := f env.checkedWithoutAsync }
-
-/-- Sets synchronous and asynchronous parts of the environment to the given kernel environment. -/
-private def setCheckedSync (env : Environment) (newChecked : Kernel.Environment) : Environment :=
-  { env with checked := .pure newChecked, checkedWithoutAsync := newChecked }
-
-@[extern "lean_elab_add_decl"]
-private opaque addDeclCheck (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration)
-  (cancelTk? : @& Option IO.CancelToken) : Except Kernel.Exception Environment
-
-@[extern "lean_elab_add_decl_without_checking"]
-private opaque addDeclWithoutChecking (env : Environment) (decl : @& Declaration) :
-  Except Kernel.Exception Environment
-
-/--
-Adds given declaration to the environment, type checking it unless `doCheck` is false.
-
-This is a plumbing function for the implementation of `Lean.addDecl`, most users should use it
-instead.
--/
-def addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration)
-    (cancelTk? : @& Option IO.CancelToken) (doCheck := true) :
-    Except Kernel.Exception Environment := do
-  if let some ctx := env.asyncCtx? then
-    if let some n := decl.getNames.find? (!ctx.mayContain ·) then
-      throw <| .other s!"cannot add declaration {n} to environment as it is restricted to the \
-        prefix {ctx.declPrefix}"
-  if doCheck then
-    addDeclCheck env maxHeartbeats decl cancelTk?
-  else
-    addDeclWithoutChecking env decl
-
-@[inherit_doc Kernel.Environment.constants]
-def constants (env : Environment) : ConstMap :=
-  env.toKernelEnv.constants
-
-@[inherit_doc Kernel.Environment.const2ModIdx]
-def const2ModIdx (env : Environment) : Std.HashMap Name ModuleIdx :=
-  env.toKernelEnv.const2ModIdx
-
--- only needed for the lakefile.lean cache
-@[export lake_environment_add]
-private def lakeAdd (env : Environment) (cinfo : ConstantInfo) : Environment :=
-  { env with checked := .pure <| env.checked.get.add cinfo }
-
-/--
-Save an extra constant name that is used to populate `const2ModIdx` when we import
-.olean files. We use this feature to save in which module an auxiliary declaration
-created by the code generator has been created.
--/
-def addExtraName (env : Environment) (name : Name) : Environment :=
-  if env.constants.contains name then
-    env
-  else
-    env.modifyCheckedAsync fun env => { env with extraConstNames := env.extraConstNames.insert name }
-
-/-- Find base case: name did not match any asynchronous declaration. -/
-private def findNoAsync (env : Environment) (n : Name) : Option ConstantInfo := do
-  if env.asyncConsts.hasPrefix n then
-    -- Constant generated in a different environment branch: wait for final kernel environment. Rare
-    -- case when only proofs are elaborated asynchronously as they are rarely inspected. Could be
-    -- optimized in the future by having the elaboration thread publish an (incremental?) map of
-    -- generated declarations before kernel checking (which must wait on all previous threads).
-    env.checked.get.constants.find?' n
-  else
-    -- Not in the kernel environment nor in the name prefix of environment branch: undefined by
-    -- `addDeclCore` invariant.
-    none
-
-/--
-Looks up the given declaration name in the environment, avoiding forcing any in-progress elaboration
-tasks.
--/
-def findAsync? (env : Environment) (n : Name) : Option AsyncConstantInfo := do
-  -- Check declarations already added to the kernel environment (e.g. because they were imported)
-  -- first as that should be the most common case. It is safe to use `find?'` because we never
-  -- overwrite imported declarations.
-  if let some c := env.checkedWithoutAsync.constants.find?' n then
-    some <| .ofConstantInfo c
-  else if let some asyncConst := env.asyncConsts.find? n then
-    -- Constant for which an asynchronous elaboration task was spawned
-    return asyncConst.constInfo
-  else env.findNoAsync n |>.map .ofConstantInfo
-
-/--
-Looks up the given declaration name in the environment, avoiding forcing any in-progress elaboration
-tasks for declaration bodies (which are not accessible from `ConstantVal`).
--/
-def findConstVal? (env : Environment) (n : Name) : Option ConstantVal := do
-  if let some c := env.checkedWithoutAsync.constants.find?' n then
-    some c.toConstantVal
-  else if let some asyncConst := env.asyncConsts.find? n then
-    return asyncConst.constInfo.toConstantVal
-  else env.findNoAsync n |>.map (·.toConstantVal)
-
-/--
-Looks up the given declaration name in the environment, blocking on the corresponding elaboration
-task if not yet complete.
--/
-def find? (env : Environment) (n : Name) : Option ConstantInfo :=
-  if let some c := env.checkedWithoutAsync.constants.find?' n then
-    some c
-  else if let some asyncConst := env.asyncConsts.find? n then
-    return asyncConst.constInfo.toConstantInfo
-  else
-    env.findNoAsync n
-
-/-- Returns debug output about the asynchronous state of the environment. -/
-def dbgFormatAsyncState (env : Environment) : BaseIO String :=
-  return s!"\
-    asyncCtx.declPrefix: {repr <| env.asyncCtx?.map (·.declPrefix)}\
-  \nasyncConsts: {repr <| env.asyncConsts.toArray.map (·.constInfo.name)}\
-  \ncheckedWithoutAsync.constants.map₂: {repr <|
-      env.checkedWithoutAsync.constants.map₂.toList.map (·.1)}"
-
-/-- Returns debug output about the synchronous state of the environment. -/
-def dbgFormatCheckedSyncState (env : Environment) : BaseIO String :=
-  return s!"checked.get.constants.map₂: {repr <| env.checked.get.constants.map₂.toList.map (·.1)}"
-
-/--
-Result of `Lean.Environment.addConstAsync` which is necessary to complete the asynchronous addition.
--/
-structure AddConstAsyncResult where
-  /--
-  Resulting "main branch" environment which contains the declaration name as an asynchronous
-  constant. Accessing the constant or kernel environment will block until the corresponding
-  `AddConstAsyncResult.commit*` function has been called.
-  -/
-  mainEnv : Environment
-  /--
-  Resulting "async branch" environment which should be used to add the desired declaration in a new
-  task and then call `AddConstAsyncResult.commit*` to commit results back to the main environment.
-  One of `commitCheckEnv` or `commitFailure` must be called eventually to prevent deadlocks on main
-  branch accesses.
-  -/
-  asyncEnv : Environment
-  private constName : Name
-  private kind : ConstantKind
-  private sigPromise : IO.Promise ConstantVal
-  private infoPromise : IO.Promise ConstantInfo
-  private extensionsPromise : IO.Promise (Array EnvExtensionState)
-  private checkedEnvPromise : IO.Promise Kernel.Environment
-
-/--
-Starts the asynchronous addition of a constant to the environment. The environment is split into a
-"main" branch that holds a reference to the constant to be added but will block on access until the
-corresponding information has been added on the "async" environment branch and committed there; see
-the respective fields of `AddConstAsyncResult` as well as the [Environment Branches] note for more
-information.
--/
-def addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind) (reportExts := true) :
-    IO AddConstAsyncResult := do
-  let sigPromise ← IO.Promise.new
-  let infoPromise ← IO.Promise.new
-  let extensionsPromise ← IO.Promise.new
-  let checkedEnvPromise ← IO.Promise.new
-  let asyncConst := {
-    constInfo := {
-      name := constName
-      kind
-      sig := sigPromise.result
-      constInfo := infoPromise.result
-    }
-    exts? := guard reportExts *> some extensionsPromise.result
-  }
-  return {
-    constName, kind
-    mainEnv := { env with
-      asyncConsts := env.asyncConsts.add asyncConst
-      checked := checkedEnvPromise.result }
-    asyncEnv := { env with
-      asyncCtx? := some { declPrefix := privateToUserName constName.eraseMacroScopes }
-    }
-    sigPromise, infoPromise, extensionsPromise, checkedEnvPromise
-  }
-
-/--
-Commits the signature of the constant to the main environment branch. The declaration name must
-match the name originally given to `addConstAsync`. It is optional to call this function but can
-help in unblocking corresponding accesses to the constant on the main branch.
--/
-def AddConstAsyncResult.commitSignature (res : AddConstAsyncResult) (sig : ConstantVal) :
-    IO Unit := do
-  if sig.name != res.constName then
-    throw <| .userError s!"AddConstAsyncResult.commitSignature: constant has name {sig.name} but expected {res.constName}"
-  res.sigPromise.resolve sig
-
-/--
-Commits the full constant info to the main environment branch. If `info?` is `none`, it is taken
-from the given environment. The declaration name and kind must match the original values given to
-`addConstAsync`. The signature must match the previous `commitSignature` call, if any.
--/
-def AddConstAsyncResult.commitConst (res : AddConstAsyncResult) (env : Environment)
-    (info? : Option ConstantInfo := none) :
-    IO Unit := do
-  let info ← match info? <|> env.find? res.constName with
-    | some info => pure info
-    | none =>
-      throw <| .userError s!"AddConstAsyncResult.commitConst: constant {res.constName} not found in async context"
-  res.commitSignature info.toConstantVal
-  let kind' := .ofConstantInfo info
-  if res.kind != kind' then
-    throw <| .userError s!"AddConstAsyncResult.commitConst: constant has kind {repr kind'} but expected {repr res.kind}"
-  let sig := res.sigPromise.result.get
-  if sig.levelParams != info.levelParams then
-    throw <| .userError s!"AddConstAsyncResult.commitConst: constant has level params {info.levelParams} but expected {sig.levelParams}"
-  if sig.type != info.type then
-    throw <| .userError s!"AddConstAsyncResult.commitConst: constant has type {info.type} but expected {sig.type}"
-  res.infoPromise.resolve info
-  res.extensionsPromise.resolve env.checkedWithoutAsync.extensions
-
-/--
-Aborts async addition, filling in missing information with default values/sorries and leaving the
-kernel environment unchanged.
--/
-def AddConstAsyncResult.commitFailure (res : AddConstAsyncResult) : BaseIO Unit := do
-  let val := if (← IO.hasFinished res.sigPromise.result) then
-    res.sigPromise.result.get
-  else {
-    name := res.constName
-    levelParams := []
-    type := mkApp2 (mkConst ``sorryAx [0]) (mkSort 0) (mkConst ``true)
-  }
-  res.sigPromise.resolve val
-  res.infoPromise.resolve <| match res.kind with
-    | .defn => .defnInfo { val with
-      value := mkApp2 (mkConst ``sorryAx [0]) val.type (mkConst ``true)
-      hints := .abbrev
-      safety := .safe
-    }
-    | .thm  => .thmInfo { val with
-      value := mkApp2 (mkConst ``sorryAx [0]) val.type (mkConst ``true)
-    }
-    | k => panic! s!"AddConstAsyncResult.commitFailure: unsupported constant kind {repr k}"
-  res.extensionsPromise.resolve #[]
-  let _ ← BaseIO.mapTask (t := res.asyncEnv.checked) (sync := true) res.checkedEnvPromise.resolve
-
-/--
-Assuming `Lean.addDecl` has been run for the constant to be added on the async environment branch,
-commits the full constant info from that call to the main environment, waits for the final kernel
-environment resulting from the `addDecl` call, and commits it to the main branch as well, unblocking
-kernel additions there. All `commitConst` preconditions apply.
--/
-def AddConstAsyncResult.commitCheckEnv (res : AddConstAsyncResult) (env : Environment) :
-    IO Unit := do
-  let some _ := env.findAsync? res.constName
-    | throw <| .userError s!"AddConstAsyncResult.checkAndCommitEnv: constant {res.constName} not \
-      found in async context"
-  res.commitConst env
-  res.checkedEnvPromise.resolve env.checked.get
-
-def contains (env : Environment) (n : Name) : Bool :=
-  env.findAsync? n |>.isSome
-
-def header (env : Environment) : EnvironmentHeader :=
-  -- can be assumed to be in sync with `env.checked`; see `setMainModule`, the only modifier of the header
-  env.checkedWithoutAsync.header
-
-def imports (env : Environment) : Array Import :=
-  env.header.imports
-
-def allImportedModuleNames (env : Environment) : Array Name :=
-  env.header.moduleNames
-
-def setMainModule (env : Environment) (m : Name) : Environment :=
-  env.modifyCheckedAsync ({ · with header.mainModule := m })
-
-def mainModule (env : Environment) : Name :=
-  env.header.mainModule
-
-def getModuleIdxFor? (env : Environment) (declName : Name) : Option ModuleIdx :=
-  -- async constants are always from the current module
-  env.checkedWithoutAsync.const2ModIdx[declName]?
-
-def isConstructor (env : Environment) (declName : Name) : Bool :=
-  match env.find? declName with
-  | some (.ctorInfo _) => true
-  | _                  => false
-
-def isSafeDefinition (env : Environment) (declName : Name) : Bool :=
-  match env.find? declName with
-  | some (.defnInfo { safety := .safe, .. }) => true
-  | _ => false
-
-def getModuleIdx? (env : Environment) (moduleName : Name) : Option ModuleIdx :=
-  env.header.moduleNames.findIdx? (· == moduleName)
+opaque addDeclWithoutChecking (env : Environment) (decl : @& Declaration) : Except KernelException Environment
 
 end Environment
 
@@ -864,22 +385,20 @@ opaque EnvExtensionInterfaceImp : EnvExtensionInterface
 def EnvExtension (σ : Type) : Type := EnvExtensionInterfaceImp.ext σ
 
 private def ensureExtensionsArraySize (env : Environment) : IO Environment := do
-  let exts ← EnvExtensionInterfaceImp.ensureExtensionsSize env.checked.get.extensions
-  return env.modifyCheckedAsync ({ · with extensions := exts })
+  let exts ← EnvExtensionInterfaceImp.ensureExtensionsSize env.extensions
+  return { env with extensions := exts }
 
 namespace EnvExtension
 instance {σ} [s : Inhabited σ] : Inhabited (EnvExtension σ) := EnvExtensionInterfaceImp.inhabitedExt s
 
 def setState {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) : Environment :=
-  let checked := env.checked.get
-  env.setCheckedSync { checked with extensions := EnvExtensionInterfaceImp.setState ext checked.extensions s }
+  { env with extensions := EnvExtensionInterfaceImp.setState ext env.extensions s }
 
 def modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ → σ) : Environment :=
-  let checked := env.checked.get
-  env.setCheckedSync { checked with extensions := EnvExtensionInterfaceImp.modifyState ext checked.extensions f }
+  { env with extensions := EnvExtensionInterfaceImp.modifyState ext env.extensions f }
 
 def getState {σ : Type} [Inhabited σ] (ext : EnvExtension σ) (env : Environment) : σ :=
-  EnvExtensionInterfaceImp.getState ext env.checked.get.extensions
+  EnvExtensionInterfaceImp.getState ext env.extensions
 
 end EnvExtension
 
@@ -899,13 +418,11 @@ def mkEmptyEnvironment (trustLevel : UInt32 := 0) : IO Environment := do
   if initializing then throw (IO.userError "environment objects cannot be created during initialization")
   let exts ← mkInitialExtensionStates
   pure {
-    checkedWithoutAsync := {
-      const2ModIdx    := {}
-      constants       := {}
-      header          := { trustLevel }
-      extraConstNames := {}
-      extensions      := exts
-    }
+    const2ModIdx    := {}
+    constants       := {}
+    header          := { trustLevel := trustLevel }
+    extraConstNames := {}
+    extensions      := exts
   }
 
 structure PersistentEnvExtensionState (α : Type) (σ : Type) where
@@ -1189,12 +706,11 @@ def mkModuleData (env : Environment) : IO ModuleData := do
   let entries := pExts.map fun pExt =>
     let state := pExt.getState env
     (pExt.name, pExt.exportEntriesFn state)
-  let kenv := env.toKernelEnv
-  let constNames := kenv.constants.foldStage2 (fun names name _ => names.push name) #[]
-  let constants  := kenv.constants.foldStage2 (fun cs _ c => cs.push c) #[]
+  let constNames := env.constants.foldStage2 (fun names name _ => names.push name) #[]
+  let constants  := env.constants.foldStage2 (fun cs _ c => cs.push c) #[]
   return {
     imports         := env.header.imports
-    extraConstNames := env.checked.get.extraConstNames.toArray
+    extraConstNames := env.extraConstNames.toArray
     constNames, constants, entries
   }
 
@@ -1215,23 +731,19 @@ def mkExtNameMap (startingAt : Nat) : IO (Std.HashMap Name Nat) := do
   return result
 
 private def setImportedEntries (env : Environment) (mods : Array ModuleData) (startingAt : Nat := 0) : IO Environment := do
-  -- We work directly on the states array instead of `env` as `Environment.modifyState` introduces
-  -- significant overhead on such frequent calls
-  let mut states := env.checkedWithoutAsync.extensions
+  let mut env := env
   let extDescrs ← persistentEnvExtensionsRef.get
   /- For extensions starting at `startingAt`, ensure their `importedEntries` array have size `mods.size`. -/
   for extDescr in extDescrs[startingAt:] do
-    states := EnvExtensionInterfaceImp.modifyState extDescr.toEnvExtension states fun s =>
-      { s with importedEntries := mkArray mods.size #[] }
+    env := extDescr.toEnvExtension.modifyState env fun s => { s with importedEntries := mkArray mods.size #[] }
   /- For each module `mod`, and `mod.entries`, if the extension name is one of the extensions after `startingAt`, set `entries` -/
   let extNameIdx ← mkExtNameMap startingAt
   for h : modIdx in [:mods.size] do
     let mod := mods[modIdx]
     for (extName, entries) in mod.entries do
       if let some entryIdx := extNameIdx[extName]? then
-        states := EnvExtensionInterfaceImp.modifyState extDescrs[entryIdx]!.toEnvExtension states fun s =>
-          { s with importedEntries := s.importedEntries.set! modIdx entries }
-  return env.setCheckedSync { env.checkedWithoutAsync with extensions := states }
+        env := extDescrs[entryIdx]!.toEnvExtension.modifyState env fun s => { s with importedEntries := s.importedEntries.set! modIdx entries }
+  return env
 
 /--
   "Forward declaration" needed for updating the attribute table with user-defined attributes.
@@ -1361,17 +873,17 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
   let constants : ConstMap := SMap.fromHashMap constantMap false
   let exts ← mkInitialExtensionStates
   let mut env : Environment := {
-    checkedWithoutAsync := {
-      const2ModIdx, constants
-      quotInit        := !imports.isEmpty -- We assume `core.lean` initializes quotient module
-      extraConstNames := {}
-      extensions      := exts
-      header     := {
-        trustLevel, imports
-        regions      := s.regions
-        moduleNames  := s.moduleNames
-        moduleData   := s.moduleData
-      }
+    const2ModIdx    := const2ModIdx
+    constants       := constants
+    extraConstNames := {}
+    extensions      := exts
+    header          := {
+      quotInit     := !imports.isEmpty -- We assume `core.lean` initializes quotient module
+      trustLevel   := trustLevel
+      imports      := imports
+      regions      := s.regions
+      moduleNames  := s.moduleNames
+      moduleData   := s.moduleData
     }
   }
   env ← setImportedEntries env s.moduleData
@@ -1434,21 +946,54 @@ builtin_initialize namespacesExt : SimplePersistentEnvExtension Name NameSSet
     addEntryFn      := fun s n => s.insert n
   }
 
-@[inherit_doc Kernel.Environment.enableDiag]
-def Kernel.enableDiag (env : Lean.Environment) (flag : Bool) : Lean.Environment :=
-  env.modifyCheckedAsync (·.enableDiag flag)
+structure Kernel.Diagnostics where
+  /-- Number of times each declaration has been unfolded by the kernel. -/
+  unfoldCounter : PHashMap Name Nat := {}
+  /-- If `enabled = true`, kernel records declarations that have been unfolded. -/
+  enabled : Bool := false
+  deriving Inhabited
 
-def Kernel.isDiagnosticsEnabled (env : Lean.Environment) : Bool :=
-  env.checkedWithoutAsync.isDiagnosticsEnabled
+/--
+Extension for storting diagnostic information.
 
-def Kernel.resetDiag (env : Lean.Environment) : Lean.Environment :=
-  env.modifyCheckedAsync (·.resetDiag)
+Remark: We store kernel diagnostic information in an environment extension to simplify
+the interface with the kernel implemented in C/C++. Thus, we can only track
+declarations in methods, such as `addDecl`, which return a new environment.
+`Kernel.isDefEq` and `Kernel.whnf` do not update the statistics. We claim
+this is ok since these methods are mainly used for debugging.
+-/
+builtin_initialize diagExt : EnvExtension Kernel.Diagnostics ←
+  registerEnvExtension (pure {})
 
-def Kernel.getDiagnostics (env : Lean.Environment) : Diagnostics :=
-  env.checked.get.diagnostics
+@[export lean_kernel_diag_is_enabled]
+def Kernel.Diagnostics.isEnabled (d : Diagnostics) : Bool :=
+  d.enabled
 
-def Kernel.setDiagnostics (env : Lean.Environment) (diag : Diagnostics) : Lean.Environment :=
-  env.modifyCheckedAsync (·.setDiagnostics diag)
+/-- Enables/disables kernel diagnostics. -/
+def Kernel.enableDiag (env : Environment) (flag : Bool) : Environment :=
+  diagExt.modifyState env fun s => { s with enabled := flag }
+
+def Kernel.isDiagnosticsEnabled (env : Environment) : Bool :=
+  diagExt.getState env |>.enabled
+
+def Kernel.resetDiag (env : Environment) : Environment :=
+  diagExt.modifyState env fun s => { s with unfoldCounter := {} }
+
+@[export lean_kernel_record_unfold]
+def Kernel.Diagnostics.recordUnfold (d : Diagnostics) (declName : Name) : Diagnostics :=
+  if d.enabled then
+    let cNew := if let some c := d.unfoldCounter.find? declName then c + 1 else 1
+    { d with unfoldCounter := d.unfoldCounter.insert declName cNew }
+  else
+    d
+
+@[export lean_kernel_get_diag]
+def Kernel.getDiagnostics (env : Environment) : Diagnostics :=
+  diagExt.getState env
+
+@[export lean_kernel_set_diag]
+def Kernel.setDiagnostics (env : Environment) (diag : Diagnostics) : Environment :=
+  diagExt.setState env diag
 
 namespace Environment
 
@@ -1464,9 +1009,27 @@ def isNamespace (env : Environment) (n : Name) : Bool :=
 def getNamespaceSet (env : Environment) : NameSSet :=
   namespacesExt.getState env
 
-@[export lean_elab_environment_update_base_after_kernel_add]
-private def updateBaseAfterKernelAdd (env : Environment) (kernel : Kernel.Environment) : Environment :=
-  env.setCheckedSync kernel
+private def isNamespaceName : Name → Bool
+  | .str .anonymous _ => true
+  | .str p _          => isNamespaceName p
+  | _                 => false
+
+private def registerNamePrefixes : Environment → Name → Environment
+  | env, .str p _ => if isNamespaceName p then registerNamePrefixes (registerNamespace env p) p else env
+  | env, _        => env
+
+@[export lean_environment_add]
+private def add (env : Environment) (cinfo : ConstantInfo) : Environment :=
+  let name := cinfo.name
+  let env := match name with
+    | .str _ s =>
+      if s.get 0 == '_' then
+        -- Do not register namespaces that only contain internal declarations.
+        env
+      else
+        registerNamePrefixes env name
+    | _ => env
+  env.addAux cinfo
 
 @[export lean_display_stats]
 def displayStats (env : Environment) : IO Unit := do
@@ -1476,7 +1039,7 @@ def displayStats (env : Environment) : IO Unit := do
   IO.println ("number of memory-mapped modules:       " ++ toString (env.header.regions.filter (·.isMemoryMapped) |>.size));
   IO.println ("number of buckets for imported consts: " ++ toString env.constants.numBuckets);
   IO.println ("trust level:                           " ++ toString env.header.trustLevel);
-  IO.println ("number of extensions:                  " ++ toString env.checkedWithoutAsync.extensions.size);
+  IO.println ("number of extensions:                  " ++ toString env.extensions.size);
   pExtDescrs.forM fun extDescr => do
     IO.println ("extension '" ++ toString extDescr.name ++ "'")
     let s := extDescr.toEnvExtension.getState env
@@ -1522,33 +1085,27 @@ namespace Kernel
 
 /--
   Kernel isDefEq predicate. We use it mainly for debugging purposes.
-  Recall that the kernel type checker does not support metavariables.
+  Recall that the Kernel type checker does not support metavariables.
   When implementing automation, consider using the `MetaM` methods. -/
--- We use `Lean.Environment` for ease of use; as this is a debugging function, we forgo a
--- `Kernel.Environment` base variant
 @[extern "lean_kernel_is_def_eq"]
-opaque isDefEq (env : Lean.Environment) (lctx : LocalContext) (a b : Expr) : Except Kernel.Exception Bool
+opaque isDefEq (env : Environment) (lctx : LocalContext) (a b : Expr) : Except KernelException Bool
 
-def isDefEqGuarded (env : Lean.Environment) (lctx : LocalContext) (a b : Expr) : Bool :=
+def isDefEqGuarded (env : Environment) (lctx : LocalContext) (a b : Expr) : Bool :=
   if let .ok result := isDefEq env lctx a b then result else false
 
 /--
   Kernel WHNF function. We use it mainly for debugging purposes.
-  Recall that the kernel type checker does not support metavariables.
+  Recall that the Kernel type checker does not support metavariables.
   When implementing automation, consider using the `MetaM` methods. -/
--- We use `Lean.Environment` for ease of use; as this is a debugging function, we forgo a
--- `Kernel.Environment` base variant
 @[extern "lean_kernel_whnf"]
-opaque whnf (env : Lean.Environment) (lctx : LocalContext) (a : Expr) : Except Kernel.Exception Expr
+opaque whnf (env : Environment) (lctx : LocalContext) (a : Expr) : Except KernelException Expr
 
 /--
   Kernel typecheck function. We use it mainly for debugging purposes.
   Recall that the Kernel type checker does not support metavariables.
   When implementing automation, consider using the `MetaM` methods. -/
--- We use `Lean.Environment` for ease of use; as this is a debugging function, we forgo a
--- `Kernel.Environment` base variant
 @[extern "lean_kernel_check"]
-opaque check (env : Lean.Environment) (lctx : LocalContext) (a : Expr) : Except Kernel.Exception Expr
+opaque check (env : Environment) (lctx : LocalContext) (a : Expr) : Except KernelException Expr
 
 end Kernel
 

src/Lean/Exception.lean

@@ -89,11 +89,11 @@ def ofExcept [Monad m] [MonadError m] [ToMessageData ε] (x : Except ε α) : m
 /--
 Throw an error exception for the given kernel exception.
 -/
-def throwKernelException [Monad m] [MonadError m] [MonadOptions m] (ex : Kernel.Exception) : m α := do
+def throwKernelException [Monad m] [MonadError m] [MonadOptions m] (ex : KernelException) : m α := do
   Lean.throwError <| ex.toMessageData (← getOptions)
 
 /-- Lift from `Except KernelException` to `m` when `m` can throw kernel exceptions. -/
-def ofExceptKernelException [Monad m] [MonadError m] [MonadOptions m] (x : Except Kernel.Exception α) : m α :=
+def ofExceptKernelException [Monad m] [MonadError m] [MonadOptions m] (x : Except KernelException α) : m α :=
   match x with
   | .ok a    => return a
   | .error e => throwKernelException e

src/Lean/Expr.lean

@@ -639,7 +639,7 @@ def mkFVar (fvarId : FVarId) : Expr :=
 /--
 `.mvar mvarId` is now the preferred form.
 This function is seldom used, metavariables are often created using functions such
-as `mkFreshExprMVar` at `MetaM`.
+as `mkFresheExprMVar` at `MetaM`.
 -/
 def mkMVar (mvarId : MVarId) : Expr :=
   .mvar mvarId

src/Lean/Message.lean

@@ -448,9 +448,6 @@ def markAllReported (log : MessageLog) : MessageLog :=
 def errorsToWarnings (log : MessageLog) : MessageLog :=
   { unreported := log.unreported.map (fun m => match m.severity with | MessageSeverity.error => { m with severity := MessageSeverity.warning } | _ => m) }
 
-def errorsToInfos (log : MessageLog) : MessageLog :=
-  { unreported := log.unreported.map (fun m => match m.severity with | MessageSeverity.error => { m with severity := MessageSeverity.information } | _ => m) }
-
 def getInfoMessages (log : MessageLog) : MessageLog :=
   { unreported := log.unreported.filter fun m => match m.severity with | MessageSeverity.information => true | _ => false }
 
@@ -540,12 +537,12 @@ macro_rules
 def toMessageList (msgs : Array MessageData) : MessageData :=
   indentD (MessageData.joinSep msgs.toList m!"\n\n")
 
-namespace Kernel.Exception
+namespace KernelException
 
 private def mkCtx (env : Environment) (lctx : LocalContext) (opts : Options) (msg : MessageData) : MessageData :=
-  MessageData.withContext { env := .ofKernelEnv env, mctx := {}, lctx := lctx, opts := opts } msg
+  MessageData.withContext { env := env, mctx := {}, lctx := lctx, opts := opts } msg
 
-def toMessageData (e : Kernel.Exception) (opts : Options) : MessageData :=
+def toMessageData (e : KernelException) (opts : Options) : MessageData :=
   match e with
   | unknownConstant env constName       => mkCtx env {} opts m!"(kernel) unknown constant '{constName}'"
   | alreadyDeclared env constName       => mkCtx env {} opts m!"(kernel) constant has already been declared '{.ofConstName constName true}'"
@@ -573,5 +570,5 @@ def toMessageData (e : Kernel.Exception) (opts : Options) : MessageData :=
   | deepRecursion                       => "(kernel) deep recursion detected"
   | interrupted                         => "(kernel) interrupted"
 
-end Kernel.Exception
+end KernelException
 end Lean

src/Lean/Meta/Constructions/CasesOn.lean

@@ -9,13 +9,13 @@ import Lean.Meta.Basic
 
 namespace Lean
 
-@[extern "lean_mk_cases_on"] opaque mkCasesOnImp (env : Kernel.Environment) (declName : @& Name) : Except Kernel.Exception Declaration
+@[extern "lean_mk_cases_on"] opaque mkCasesOnImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
 
 open Meta
 
 def mkCasesOn (declName : Name) : MetaM Unit := do
   let name := mkCasesOnName declName
-  let decl ← ofExceptKernelException (mkCasesOnImp (← getEnv).toKernelEnv declName)
+  let decl ← ofExceptKernelException (mkCasesOnImp (← getEnv) declName)
   addDecl decl
   setReducibleAttribute name
   modifyEnv fun env => markAuxRecursor env name

src/Lean/Meta/Constructions/NoConfusion.lean

@@ -10,8 +10,8 @@ import Lean.Meta.CompletionName
 
 namespace Lean
 
-@[extern "lean_mk_no_confusion_type"] opaque mkNoConfusionTypeCoreImp (env : Environment) (declName : @& Name) : Except Kernel.Exception Declaration
-@[extern "lean_mk_no_confusion"] opaque mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except Kernel.Exception Declaration
+@[extern "lean_mk_no_confusion_type"] opaque mkNoConfusionTypeCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
+@[extern "lean_mk_no_confusion"] opaque mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
 
 open Meta
 

src/Lean/Meta/ExprDefEq.lean

@@ -1233,7 +1233,10 @@ private def processAssignment' (mvarApp : Expr) (v : Expr) : MetaM Bool := do
 
 private def isDeltaCandidate? (t : Expr) : MetaM (Option ConstantInfo) := do
   match t.getAppFn with
-  | .const c _ => getUnfoldableConst? c
+  | .const c _ =>
+    match (← getUnfoldableConst? c) with
+    | r@(some info) => if info.hasValue then return r else return none
+    | _             => return none
   | _ => pure none
 
 /-- Auxiliary method for isDefEqDelta -/

src/Lean/Meta/GetUnfoldableConst.lean

@@ -30,7 +30,7 @@ def canUnfold (info : ConstantInfo) : MetaM Bool := do
 
 /--
 Look up a constant name, returning the `ConstantInfo`
-if it is a def/theorem that should be unfolded at the current reducibility settings,
+if it should be unfolded at the current reducibility settings,
 or `none` otherwise.
 
 This is part of the implementation of `whnf`.
@@ -40,7 +40,7 @@ def getUnfoldableConst? (constName : Name) : MetaM (Option ConstantInfo) := do
   match (← getEnv).find? constName with
   | some (info@(.thmInfo _))  => getTheoremInfo info
   | some (info@(.defnInfo _)) => if (← canUnfold info) then return info else return none
-  | some _                    => return none
+  | some info                 => return some info
   | none                      => throwUnknownConstant constName
 
 /--
@@ -50,6 +50,7 @@ def getUnfoldableConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) :=
   match (← getEnv).find? constName with
   | some (info@(.thmInfo _))  => getTheoremInfo info
   | some (info@(.defnInfo _)) => if (← canUnfold info) then return info else return none
-  | _                         => return none
+  | some info                 => return some info
+  | none                      => return none
 
 end Meta

src/Lean/Meta/IndPredBelow.lean

@@ -296,7 +296,7 @@ where
     m.apply recursor
 
   applyCtors (ms : List MVarId) : MetaM $ List MVarId := do
-    let mss ← ms.toArray.mapM fun m => do
+    let mss ← ms.toArray.mapIdxM fun _ m => do
       let m ← introNPRec m
       (← m.getType).withApp fun below args =>
       m.withContext do

src/Lean/Meta/Tactic.lean

@@ -41,4 +41,3 @@ import Lean.Meta.Tactic.FunInd
 import Lean.Meta.Tactic.Rfl
 import Lean.Meta.Tactic.Rewrites
 import Lean.Meta.Tactic.Grind
-import Lean.Meta.Tactic.Ext

src/Lean/Meta/Tactic/Ext.lean

@@ -1,76 +0,0 @@
-/-
-Copyright (c) 2021 Gabriel Ebner. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Mario Carneiro
--/
-prelude
-import Init.Data.Array.InsertionSort
-import Lean.Meta.DiscrTree
-
-namespace Lean.Meta.Ext
-
-/-!
-### Environment extension for `ext` theorems
--/
-
-/-- Information about an extensionality theorem, stored in the environment extension. -/
-structure ExtTheorem where
-  /-- Declaration name of the extensionality theorem. -/
-  declName : Name
-  /-- Priority of the extensionality theorem. -/
-  priority : Nat
-  /--
-  Key in the discrimination tree,
-  for the type in which the extensionality theorem holds.
-  -/
-  keys : Array DiscrTree.Key
-  deriving Inhabited, Repr, BEq, Hashable
-
-/-- The state of the `ext` extension environment -/
-structure ExtTheorems where
-  /-- The tree of `ext` extensions. -/
-  tree   : DiscrTree ExtTheorem := {}
-  /-- Erased `ext`s via `attribute [-ext]`. -/
-  erased  : PHashSet Name := {}
-  deriving Inhabited
-
-/-- The environment extension to track `@[ext]` theorems. -/
-builtin_initialize extExtension :
-    SimpleScopedEnvExtension ExtTheorem ExtTheorems ←
-  registerSimpleScopedEnvExtension {
-    addEntry := fun { tree, erased } thm =>
-      { tree := tree.insertCore thm.keys thm, erased := erased.erase thm.declName }
-    initial := {}
-  }
-
-/-- Gets the list of `@[ext]` theorems corresponding to the key `ty`,
-ordered from high priority to low. -/
-@[inline] def getExtTheorems (ty : Expr) : MetaM (Array ExtTheorem) := do
-  let extTheorems := extExtension.getState (← getEnv)
-  let arr ← extTheorems.tree.getMatch ty
-  let erasedArr := arr.filter fun thm => !extTheorems.erased.contains thm.declName
-  -- Using insertion sort because it is stable and the list of matches should be mostly sorted.
-  -- Most ext theorems have default priority.
-  return erasedArr.insertionSort (·.priority < ·.priority) |>.reverse
-
-/--
-Erases a name marked `ext` by adding it to the state's `erased` field and
-removing it from the state's list of `Entry`s.
-
-This is triggered by `attribute [-ext] name`.
--/
-def ExtTheorems.eraseCore (d : ExtTheorems) (declName : Name) : ExtTheorems :=
- { d with erased := d.erased.insert declName }
-
-/--
-Erases a name marked as a `ext` attribute.
-Check that it does in fact have the `ext` attribute by making sure it names a `ExtTheorem`
-found somewhere in the state's tree, and is not erased.
--/
-def ExtTheorems.erase [Monad m] [MonadError m] (d : ExtTheorems) (declName : Name) :
-    m ExtTheorems := do
-  unless d.tree.containsValueP (·.declName == declName) && !d.erased.contains declName do
-    throwError "'{declName}' does not have [ext] attribute"
-  return d.eraseCore declName
-
-end Lean.Meta.Ext

src/Lean/Meta/Tactic/Grind.lean

@@ -25,7 +25,6 @@ import Lean.Meta.Tactic.Grind.EMatch
 import Lean.Meta.Tactic.Grind.Main
 import Lean.Meta.Tactic.Grind.CasesMatch
 import Lean.Meta.Tactic.Grind.Arith
-import Lean.Meta.Tactic.Grind.Ext
 
 namespace Lean
 
@@ -39,7 +38,6 @@ builtin_initialize registerTraceClass `grind.ematch.pattern
 builtin_initialize registerTraceClass `grind.ematch.pattern.search
 builtin_initialize registerTraceClass `grind.ematch.instance
 builtin_initialize registerTraceClass `grind.ematch.instance.assignment
-builtin_initialize registerTraceClass `grind.eqResolution
 builtin_initialize registerTraceClass `grind.issues
 builtin_initialize registerTraceClass `grind.simp
 builtin_initialize registerTraceClass `grind.split
@@ -53,7 +51,6 @@ builtin_initialize registerTraceClass `grind.offset.propagate
 builtin_initialize registerTraceClass `grind.offset.eq
 builtin_initialize registerTraceClass `grind.offset.eq.to (inherited := true)
 builtin_initialize registerTraceClass `grind.offset.eq.from (inherited := true)
-builtin_initialize registerTraceClass `grind.beta
 
 /-! Trace options for `grind` developers -/
 builtin_initialize registerTraceClass `grind.debug
@@ -68,7 +65,4 @@ builtin_initialize registerTraceClass `grind.debug.split
 builtin_initialize registerTraceClass `grind.debug.canon
 builtin_initialize registerTraceClass `grind.debug.offset
 builtin_initialize registerTraceClass `grind.debug.offset.proof
-builtin_initialize registerTraceClass `grind.debug.ematch.pattern
-builtin_initialize registerTraceClass `grind.debug.beta
-
 end Lean

src/Lean/Meta/Tactic/Grind/Attr.lean

@@ -10,6 +10,12 @@ import Lean.Meta.Tactic.Simp.Simproc
 namespace Lean.Meta.Grind
 open Simp
 
+builtin_initialize grindNormExt : SimpExtension ←
+  registerSimpAttr `grind_norm "simplification/normalization theorems for `grind`"
+
+builtin_initialize grindNormSimprocExt : SimprocExtension ←
+  registerSimprocAttr `grind_norm_proc "simplification/normalization procedured for `grind`" none
+
 builtin_initialize grindCasesExt : SimpleScopedEnvExtension Name NameSet ←
   registerSimpleScopedEnvExtension {
     initial        := {}

src/Lean/Meta/Tactic/Grind/Beta.lean

@@ -1,77 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Tactic.Grind.Types
-
-namespace Lean.Meta.Grind
-
-/-- Returns all lambda expressions in the equivalence class with root `root`. -/
-def getEqcLambdas (root : ENode) : GoalM (Array Expr) := do
-  unless root.hasLambdas do return #[]
-  foldEqc root.self (init := #[]) fun n lams =>
-    if n.self.isLambda then return lams.push n.self else return lams
-
-/--
-Returns the root of the functions in the equivalence class containing `e`.
-That is, if `f a` is in `root`s equivalence class, results contains the root of `f`.
--/
-def getFnRoots (e : Expr) : GoalM (Array Expr) := do
-  foldEqc e (init := #[]) fun n fns => do
-    let fn := n.self.getAppFn
-    let fnRoot := (← getRoot? fn).getD fn
-    if Option.isNone <| fns.find? (isSameExpr · fnRoot) then
-      return fns.push fnRoot
-    else
-      return fns
-
-/--
-For each `lam` in `lams` s.t. `lam` and `f` are in the same equivalence class,
-propagate `f args = lam args`.
--/
-def propagateBetaEqs (lams : Array Expr) (f : Expr) (args : Array Expr) : GoalM Unit := do
-  if args.isEmpty then return ()
-  for lam in lams do
-    let rhs := lam.beta args
-    unless rhs.isLambda do
-      let mut gen := Nat.max (← getGeneration lam) (← getGeneration f)
-      let lhs := mkAppN f args
-      if (← hasSameType f lam) then
-        let mut h ← mkEqProof f lam
-        for arg in args do
-          gen := Nat.max gen (← getGeneration arg)
-          h ← mkCongrFun h arg
-        let eq ← mkEq lhs rhs
-        trace[grind.beta] "{eq}, using {lam}"
-        addNewFact h eq (gen+1)
-
-private def isPropagateBetaTarget (e : Expr) : GoalM Bool := do
-  let .app f _ := e | return false
-  go f
-where
-  go (f : Expr) : GoalM Bool := do
-    if let some root ← getRootENode? f then
-      return root.hasLambdas
-    let .app f _ := f | return false
-    go f
-
-/--
-Applies beta-reduction for lambdas in `f`s equivalence class.
-We use this function while internalizing new applications.
--/
-def propagateBetaForNewApp (e : Expr) : GoalM Unit := do
-  unless (← isPropagateBetaTarget e) do return ()
-  let mut e := e
-  let mut args := #[]
-  repeat
-    unless args.isEmpty do
-      if let some root ← getRootENode? e then
-        if root.hasLambdas then
-          propagateBetaEqs (← getEqcLambdas root) e args.reverse
-    let .app f arg := e | return ()
-    e := f
-    args := args.push arg
-
-end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Core.lean

@@ -11,7 +11,6 @@ import Lean.Meta.Tactic.Grind.Inv
 import Lean.Meta.Tactic.Grind.PP
 import Lean.Meta.Tactic.Grind.Ctor
 import Lean.Meta.Tactic.Grind.Util
-import Lean.Meta.Tactic.Grind.Beta
 import Lean.Meta.Tactic.Grind.Internalize
 
 namespace Lean.Meta.Grind
@@ -41,7 +40,7 @@ Remove `root` parents from the congruence table.
 This is an auxiliary function performed while merging equivalence classes.
 -/
 private def removeParents (root : Expr) : GoalM ParentSet := do
-  let parents ← getParents root
+  let parents ← getParentsAndReset root
   for parent in parents do
     -- Recall that we may have `Expr.forallE` in `parents` because of `ForallProp.lean`
     if (← pure parent.isApp <&&> isCongrRoot parent) then
@@ -108,31 +107,6 @@ private def propagateOffsetEq (rhsRoot lhsRoot : ENode) : GoalM Unit := do
     if let some rhsOffset := rhsRoot.offset? then
       Arith.processNewOffsetEqLit rhsOffset lhsRoot.self
 
-/--
-Tries to apply beta-reductiong using the parent applications of the functions in `fns` with
-the lambda expressions in `lams`.
--/
-def propagateBeta (lams : Array Expr) (fns : Array Expr) : GoalM Unit := do
-  if lams.isEmpty then return ()
-  let lamRoot ← getRoot lams.back!
-  trace[grind.debug.beta] "fns: {fns}, lams: {lams}"
-  for fn in fns do
-    trace[grind.debug.beta] "fn: {fn}, parents: {(← getParents fn).toArray}"
-    for parent in (← getParents fn) do
-      let mut args := #[]
-      let mut curr := parent
-      trace[grind.debug.beta] "parent: {parent}"
-      repeat
-        trace[grind.debug.beta] "curr: {curr}"
-        if (← isEqv curr lamRoot) then
-          propagateBetaEqs lams curr args.reverse
-        let .app f arg := curr
-          | break
-        -- Remark: recall that we do not eagerly internalize partial applications.
-        internalize curr (← getGeneration parent)
-        args := args.push arg
-        curr := f
-
 private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
   let lhsNode ← getENode lhs
   let rhsNode ← getENode rhs
@@ -184,10 +158,6 @@ where
       proof?  := proof
       flipped
     }
-    let lams₁ ← getEqcLambdas lhsRoot
-    let lams₂ ← getEqcLambdas rhsRoot
-    let fns₁  ← if lams₁.isEmpty then pure #[] else getFnRoots rhsRoot.self
-    let fns₂  ← if lams₂.isEmpty then pure #[] else getFnRoots lhsRoot.self
     let parents ← removeParents lhsRoot.self
     updateRoots lhs rhsNode.root
     trace_goal[grind.debug] "{← ppENodeRef lhs} new root {← ppENodeRef rhsNode.root}, {← ppENodeRef (← getRoot lhs)}"
@@ -202,9 +172,6 @@ where
       hasLambdas := rhsRoot.hasLambdas || lhsRoot.hasLambdas
       heqProofs  := isHEq || rhsRoot.heqProofs || lhsRoot.heqProofs
     }
-    propagateBeta lams₁ fns₁
-    propagateBeta lams₂ fns₂
-    resetParentsOf lhsRoot.self
     copyParentsTo parents rhsNode.root
     unless (← isInconsistent) do
       updateMT rhsRoot.self

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -266,7 +266,7 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
   for mvar in mvars, bi in bis do
     if bi.isInstImplicit && !(← mvar.mvarId!.isAssigned) then
       let type ← inferType mvar
-      unless (← synthesizeInstanceAndAssign mvar type) do
+      unless (← synthesizeInstance mvar type) do
         reportIssue m!"failed to synthesize instance when instantiating {← thm.origin.pp}{indentExpr type}"
         return ()
   let proof := mkAppN proof mvars
@@ -278,6 +278,10 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
       reportIssue m!"failed to instantiate {← thm.origin.pp}, failed to instantiate non propositional argument with type{indentExpr (← inferType mvarBad)}"
     let proof ← mkLambdaFVars (binderInfoForMVars := .default) mvars (← instantiateMVars proof)
     addNewInstance thm.origin proof c.gen
+where
+  synthesizeInstance (x type : Expr) : MetaM Bool := do
+    let .some val ← trySynthInstance type | return false
+    isDefEq x val
 
 /-- Process choice stack until we don't have more choices to be processed. -/
 private def processChoices : M Unit := do

src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -516,9 +516,7 @@ def mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof :
       | HEq _ lhs _ rhs => pure (lhs, rhs)
       | _ => throwError "invalid E-matching equality theorem, conclusion must be an equality{indentExpr type}"
     let pat := if useLhs then lhs else rhs
-    trace[grind.debug.ematch.pattern] "mkEMatchEqTheoremCore: origin: {← origin.pp}, pat: {pat}, useLhs: {useLhs}"
     let pat ← preprocessPattern pat normalizePattern
-    trace[grind.debug.ematch.pattern] "mkEMatchEqTheoremCore: after preprocessing: {pat}, {← normalize pat}"
     let pats := splitWhileForbidden (pat.abstract xs)
     return (xs.size, pats)
   mkEMatchTheoremCore origin levelParams numParams proof patterns
@@ -553,7 +551,7 @@ def getEMatchTheorems : CoreM EMatchTheorems :=
 
 inductive TheoremKind where
   | eqLhs | eqRhs | eqBoth | fwd | bwd | default
-  deriving Inhabited, BEq, Repr
+  deriving Inhabited, BEq
 
 private def TheoremKind.toAttribute : TheoremKind → String
   | .eqLhs   => "[grind =]"
@@ -653,9 +651,9 @@ private def collectPatterns? (proof : Expr) (xs : Array Expr) (searchPlaces : Ar
 
 def mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : TheoremKind) : MetaM (Option EMatchTheorem) := do
   if kind == .eqLhs then
-    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := true))
+    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := false) (useLhs := true))
   else if kind == .eqRhs then
-    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := false))
+    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := false) (useLhs := false))
   let type ← inferType proof
   forallTelescopeReducing type fun xs type => do
     let searchPlaces ← match kind with
@@ -679,40 +677,28 @@ where
       levelParams, origin
     }
 
-/-- Return theorem kind for `stx` of the form `Attr.grindThmMod` -/
-def getTheoremKindCore (stx : Syntax) : CoreM TheoremKind := do
-  match stx with
-  | `(Parser.Attr.grindThmMod| =) => return .eqLhs
-  | `(Parser.Attr.grindThmMod| →) => return .fwd
-  | `(Parser.Attr.grindThmMod| ←) => return .bwd
-  | `(Parser.Attr.grindThmMod| =_) => return .eqRhs
-  | `(Parser.Attr.grindThmMod| _=_) => return .eqBoth
-  | _ => throwError "unexpected `grind` theorem kind: `{stx}`"
-
-/-- Return theorem kind for `stx` of the form `(Attr.grindThmMod)?` -/
-def getTheoremKindFromOpt (stx : Syntax) : CoreM TheoremKind := do
+private def getKind (stx : Syntax) : TheoremKind :=
   if stx[1].isNone then
-    return .default
+    .default
+  else if stx[1][0].getKind == ``Parser.Attr.grindEq then
+    .eqLhs
+  else if stx[1][0].getKind == ``Parser.Attr.grindFwd then
+    .fwd
+  else if stx[1][0].getKind == ``Parser.Attr.grindEqRhs then
+    .eqRhs
+  else if stx[1][0].getKind == ``Parser.Attr.grindEqBoth then
+    .eqBoth
   else
-    getTheoremKindCore stx[1][0]
-
-def mkEMatchTheoremForDecl (declName : Name) (thmKind : TheoremKind) : MetaM EMatchTheorem := do
-  let some thm ← mkEMatchTheoremWithKind? (.decl declName) #[] (← getProofFor declName) thmKind
-    | throwError "`@{thmKind.toAttribute} theorem {declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command"
-  return thm
-
-def mkEMatchEqTheoremsForDef? (declName : Name) : MetaM (Option (Array EMatchTheorem)) := do
-  let some eqns ← getEqnsFor? declName | return none
-  eqns.mapM fun eqn => do
-    mkEMatchEqTheorem eqn (normalizePattern := true)
+    .bwd
 
 private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) (useLhs := true) : MetaM Unit := do
   if (← getConstInfo declName).isTheorem then
     ematchTheoremsExt.add (← mkEMatchEqTheorem declName (normalizePattern := true) (useLhs := useLhs)) attrKind
-  else if let some thms ← mkEMatchEqTheoremsForDef? declName then
+  else if let some eqns ← getEqnsFor? declName then
     unless useLhs do
       throwError "`{declName}` is a definition, you must only use the left-hand side for extracting patterns"
-    thms.forM (ematchTheoremsExt.add · attrKind)
+    for eqn in eqns do
+      ematchTheoremsExt.add (← mkEMatchEqTheorem eqn) attrKind
   else
     throwError s!"`{thmKind.toAttribute}` attribute can only be applied to equational theorems or function definitions"
 
@@ -727,26 +713,10 @@ private def addGrindAttr (declName : Name) (attrKind : AttributeKind) (thmKind :
   else if !(← getConstInfo declName).isTheorem then
     addGrindEqAttr declName attrKind thmKind
   else
-    let thm ← mkEMatchTheoremForDecl declName thmKind
+    let some thm ← mkEMatchTheoremWithKind? (.decl declName) #[] (← getProofFor declName) thmKind
+      | throwError "`@{thmKind.toAttribute} theorem {declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command"
     ematchTheoremsExt.add thm attrKind
 
-def EMatchTheorems.eraseDecl (s : EMatchTheorems) (declName : Name) : MetaM EMatchTheorems := do
-  let throwErr {α} : MetaM α :=
-    throwError "`{declName}` is not marked with the `[grind]` attribute"
-  let info ← getConstInfo declName
-  if !info.isTheorem then
-    if let some eqns ← getEqnsFor? declName then
-       let s := ematchTheoremsExt.getState (← getEnv)
-       unless eqns.all fun eqn => s.contains (.decl eqn) do
-         throwErr
-       return eqns.foldl (init := s) fun s eqn => s.erase (.decl eqn)
-    else
-      throwErr
-  else
-    unless ematchTheoremsExt.getState (← getEnv) |>.contains (.decl declName) do
-      throwErr
-    return s.erase <| .decl declName
-
 builtin_initialize
   registerBuiltinAttribute {
     name := `grind
@@ -769,7 +739,7 @@ builtin_initialize
       `grind` will add an instance of this theorem to the local context whenever it encounters the pattern `foo (foo x)`."
     applicationTime := .afterCompilation
     add := fun declName stx attrKind => do
-      addGrindAttr declName attrKind (← getTheoremKindFromOpt stx) |>.run' {}
+      addGrindAttr declName attrKind (getKind stx) |>.run' {}
     erase := fun declName => MetaM.run' do
       /-
       Remark: consider the following example
@@ -785,9 +755,21 @@ builtin_initialize
       attribute [-grind] foo  -- ok
       ```
       -/
-      let s := ematchTheoremsExt.getState (← getEnv)
-      let s ← s.eraseDecl declName
-      modifyEnv fun env => ematchTheoremsExt.modifyState env fun _ => s
+      let throwErr := throwError "`{declName}` is not marked with the `[grind]` attribute"
+      let info ← getConstInfo declName
+      if !info.isTheorem then
+        if let some eqns ← getEqnsFor? declName then
+           let s := ematchTheoremsExt.getState (← getEnv)
+           unless eqns.all fun eqn => s.contains (.decl eqn) do
+             throwErr
+           modifyEnv fun env => ematchTheoremsExt.modifyState env fun s =>
+             eqns.foldl (init := s) fun s eqn => s.erase (.decl eqn)
+        else
+          throwErr
+      else
+        unless ematchTheoremsExt.getState (← getEnv) |>.contains (.decl declName) do
+          throwErr
+        modifyEnv fun env => ematchTheoremsExt.modifyState env fun s => s.erase (.decl declName)
   }
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/EqResolution.lean

@@ -1,47 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.AppBuilder
-
-namespace Lean.Meta.Grind
-/-! A basic "equality resolution" procedure. -/
-
-private def eqResCore (prop proof : Expr) : MetaM (Option (Expr × Expr)) := withNewMCtxDepth do
-  let (ms, _, type) ← forallMetaTelescopeReducing prop
-  if ms.isEmpty then return none
-  let mut progress := false
-  for m in ms do
-    let type ← inferType m
-    let_expr Eq _ lhs rhs ← type
-      | pure ()
-    if (← isDefEq lhs rhs) then
-      unless (← m.mvarId!.checkedAssign (← mkEqRefl lhs)) do
-        return none
-      progress := true
-  unless progress do
-    return none
-  if (← ms.anyM fun m => m.mvarId!.isDelayedAssigned) then
-    return none
-  let prop' ← instantiateMVars type
-  let proof' ← instantiateMVars (mkAppN proof ms)
-  let ms ← ms.filterM fun m => return !(← m.mvarId!.isAssigned)
-  let prop' ← mkForallFVars ms prop' (binderInfoForMVars := .default)
-  let proof' ← mkLambdaFVars ms proof'
-  return some (prop', proof')
-
-/--
-A basic "equality resolution" procedure: Given a proposition `prop` with a proof `proof`, it attempts to resolve equality hypotheses using `isDefEq`. For example, it reduces `∀ x y, f x = f (g y y) → g x y = y` to `∀ y, g (g y y) y = y`, and `∀ (x : Nat), f x ≠ f a` to `False`.
-If successful, the result is a pair `(prop', proof)`, where `prop'` is the simplified proposition,
-and `proof : prop → prop'`
--/
-def eqResolution (prop : Expr) : MetaM (Option (Expr × Expr)) :=
-  withLocalDeclD `h prop fun h => do
-    let some (prop', proof') ← eqResCore prop h
-      | return none
-    let proof' ← mkLambdaFVars #[h] proof'
-    return some (prop', proof')
-
-end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Ext.lean

@@ -1,40 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Tactic.Grind.Types
-
-namespace Lean.Meta.Grind
-/-! Extensionality theorems support. -/
-
-def instantiateExtTheorem (thm : Ext.ExtTheorem) (e : Expr) : GoalM Unit := withNewMCtxDepth do
-  unless (← getGeneration e) < (← getMaxGeneration) do return ()
-  let c ← mkConstWithFreshMVarLevels thm.declName
-  let (mvars, bis, type) ← withDefault <| forallMetaTelescopeReducing (← inferType c)
-  unless (← isDefEq e type) do
-    reportIssue m!"failed to apply extensionality theorem `{thm.declName}` for {indentExpr e}\nis not definitionally equal to{indentExpr type}"
-    return ()
-  -- Instantiate type class instances
-  for mvar in mvars, bi in bis do
-    if bi.isInstImplicit && !(← mvar.mvarId!.isAssigned) then
-      let type ← inferType mvar
-      unless (← synthesizeInstanceAndAssign mvar type) do
-        reportIssue m!"failed to synthesize instance when instantiating extensionality theorem `{thm.declName}` for {indentExpr e}"
-        return ()
-  -- Remark: `proof c mvars` has type `e`
-  let proof ← instantiateMVars (mkAppN c mvars)
-  -- `e` is equal to `False`
-  let eEqFalse ← mkEqFalseProof e
-  -- So, we use `Eq.mp` to build a `proof` of `False`
-  let proof ← mkEqMP eEqFalse proof
-  let mvars ← mvars.filterM fun mvar => return !(← mvar.mvarId!.isAssigned)
-  let proof' ← instantiateMVars (← mkLambdaFVars mvars proof)
-  let prop' ← inferType proof'
-  if proof'.hasMVar || prop'.hasMVar then
-    reportIssue m!"failed to apply extensionality theorem `{thm.declName}` for {indentExpr e}\nresulting terms contain metavariables"
-    return ()
-  addNewFact proof' prop' ((← getGeneration e) + 1)
-
-end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/ForallProp.lean

@@ -8,7 +8,6 @@ import Init.Grind.Lemmas
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Internalize
 import Lean.Meta.Tactic.Grind.Simp
-import Lean.Meta.Tactic.Grind.EqResolution
 
 namespace Lean.Meta.Grind
 /--
@@ -97,13 +96,7 @@ def propagateForallPropDown (e : Expr) : GoalM Unit := do
       pushEqTrue a <| mkApp3 (mkConst ``Grind.eq_true_of_imp_eq_false) a b h
       pushEqFalse b <| mkApp3 (mkConst ``Grind.eq_false_of_imp_eq_false) a b h
   else if (← isEqTrue e) then
-    if let some (e', h') ← eqResolution e then
-      trace[grind.eqResolution] "{e}, {e'}"
-      let h := mkOfEqTrueCore e (← mkEqTrueProof e)
-      let h' := mkApp h' h
-      addNewFact h' e' (← getGeneration e)
-    else
-      if b.hasLooseBVars then
-        addLocalEMatchTheorems e
+    if b.hasLooseBVars then
+      addLocalEMatchTheorems e
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -12,7 +12,6 @@ import Lean.Meta.Match.MatchEqsExt
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Canon
-import Lean.Meta.Tactic.Grind.Beta
 import Lean.Meta.Tactic.Grind.Arith.Internalize
 
 namespace Lean.Meta.Grind
@@ -195,7 +194,7 @@ partial def internalize (e : Expr) (generation : Nat) (parent? : Option Expr :=
           activateTheoremPatterns fName generation
         else
           internalize f generation e
-        registerParent e f
+          registerParent e f
         for h : i in [: args.size] do
           let arg := args[i]
           internalize arg generation e
@@ -205,8 +204,6 @@ partial def internalize (e : Expr) (generation : Nat) (parent? : Option Expr :=
       updateAppMap e
       Arith.internalize e parent?
       propagateUp e
-      propagateBetaForNewApp e
-
 end
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Main.lean

@@ -20,19 +20,6 @@ import Lean.Meta.Tactic.Grind.SimpUtil
 
 namespace Lean.Meta.Grind
 
-structure Params where
-  config    : Grind.Config
-  ematch    : EMatchTheorems := {}
-  extra     : PArray EMatchTheorem := {}
-  norm      : Simp.Context
-  normProcs : Array Simprocs
-  -- TODO: inductives to split
-
-def mkParams (config : Grind.Config) : MetaM Params := do
-  let norm ← Grind.getSimpContext
-  let normProcs ← Grind.getSimprocs
-  return { config, norm, normProcs }
-
 def mkMethods (fallback : Fallback) : CoreM Methods := do
   let builtinPropagators ← builtinPropagatorsRef.get
   return {
@@ -50,29 +37,26 @@ def mkMethods (fallback : Fallback) : CoreM Methods := do
        prop e
   }
 
-def GrindM.run (x : GrindM α) (mainDeclName : Name) (params : Params) (fallback : Fallback) : MetaM α := do
+def GrindM.run (x : GrindM α) (mainDeclName : Name) (config : Grind.Config) (fallback : Fallback) : MetaM α := do
   let scState := ShareCommon.State.mk _
   let (falseExpr, scState) := ShareCommon.State.shareCommon scState (mkConst ``False)
   let (trueExpr, scState)  := ShareCommon.State.shareCommon scState (mkConst ``True)
   let (natZExpr, scState)  := ShareCommon.State.shareCommon scState (mkNatLit 0)
-  let simprocs := params.normProcs
-  let simp := params.norm
-  let config := params.config
+  let simprocs ← Grind.getSimprocs
+  let simp ← Grind.getSimpContext
   x (← mkMethods fallback).toMethodsRef { mainDeclName, config, simprocs, simp } |>.run' { scState, trueExpr, falseExpr, natZExpr }
 
-private def mkGoal (mvarId : MVarId) (params : Params) : GrindM Goal := do
+private def mkGoal (mvarId : MVarId) : GrindM Goal := do
   let trueExpr ← getTrueExpr
   let falseExpr ← getFalseExpr
   let natZeroExpr ← getNatZeroExpr
-  let thmMap := params.ematch
+  let thmMap ← getEMatchTheorems
   GoalM.run' { mvarId, thmMap } do
     mkENodeCore falseExpr (interpreted := true) (ctor := false) (generation := 0)
     mkENodeCore trueExpr (interpreted := true) (ctor := false) (generation := 0)
     mkENodeCore natZeroExpr (interpreted := true) (ctor := false) (generation := 0)
-    for thm in params.extra do
-      activateTheorem thm 0
 
-private def initCore (mvarId : MVarId) (params : Params) : GrindM (List Goal) := do
+private def initCore (mvarId : MVarId) : GrindM (List Goal) := do
   mvarId.ensureProp
   -- TODO: abstract metavars
   mvarId.ensureNoMVar
@@ -81,13 +65,13 @@ private def initCore (mvarId : MVarId) (params : Params) : GrindM (List Goal) :=
   let mvarId ← mvarId.unfoldReducible
   let mvarId ← mvarId.betaReduce
   appendTagSuffix mvarId `grind
-  let goals ← intros (← mkGoal mvarId params) (generation := 0)
+  let goals ← intros (← mkGoal mvarId) (generation := 0)
   goals.forM (·.checkInvariants (expensive := true))
   return goals.filter fun goal => !goal.inconsistent
 
-def main (mvarId : MVarId) (params : Params) (mainDeclName : Name) (fallback : Fallback) : MetaM (List Goal) := do
+def main (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Fallback) : MetaM (List Goal) := do
   let go : GrindM (List Goal) := do
-    let goals ← initCore mvarId params
+    let goals ← initCore mvarId
     let goals ← solve goals
     let goals ← goals.filterMapM fun goal => do
       if goal.inconsistent then return none
@@ -97,6 +81,6 @@ def main (mvarId : MVarId) (params : Params) (mainDeclName : Name) (fallback : F
       return some goal
     trace[grind.debug.final] "{← ppGoals goals}"
     return goals
-  go.run mainDeclName params fallback
+  go.run mainDeclName config fallback
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Parser.lean

@@ -12,8 +12,4 @@ Builtin parsers for `grind` related commands
 -/
 @[builtin_command_parser] def grindPattern := leading_parser
   "grind_pattern " >>  ident >> darrow >> sepBy1 termParser ","
-
-@[builtin_command_parser] def initGrindNorm := leading_parser
-  "init_grind_norm " >> many ident >> "| " >> many ident
-
 end Lean.Parser.Command

src/Lean/Meta/Tactic/Grind/Propagate.lean

@@ -8,7 +8,6 @@ import Init.Grind
 import Lean.Meta.Tactic.Grind.Proof
 import Lean.Meta.Tactic.Grind.PropagatorAttr
 import Lean.Meta.Tactic.Grind.Simp
-import Lean.Meta.Tactic.Grind.Ext
 import Lean.Meta.Tactic.Grind.Internalize
 
 namespace Lean.Meta.Grind
@@ -134,19 +133,6 @@ builtin_grind_propagator propagateEqDown ↓Eq := fun e => do
   if (← isEqTrue e) then
     let_expr Eq _ a b := e | return ()
     pushEq a b <| mkOfEqTrueCore e (← mkEqTrueProof e)
-  else if (← isEqFalse e) then
-    let_expr Eq α lhs rhs := e | return ()
-    let thms ← getExtTheorems α
-    if !thms.isEmpty then
-      /-
-      Heuristic for lists: If `lhs` or `rhs` are contructors we do not apply extensionality theorems.
-      For example, we don't want to apply the extensionality theorem to things like `xs ≠ []`.
-      TODO: polish this hackish heuristic later.
-      -/
-      if α.isAppOf ``List && ((← getRootENode lhs).ctor || (← getRootENode rhs).ctor) then
-        return ()
-      for thm in (← getExtTheorems α) do
-        instantiateExtTheorem thm e
 
 /-- Propagates `EqMatch` downwards -/
 builtin_grind_propagator propagateEqMatchDown ↓Grind.EqMatch := fun e => do

src/Lean/Meta/Tactic/Grind/SimpUtil.lean

@@ -7,44 +7,18 @@ prelude
 import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.DoNotSimp
-import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
 
 namespace Lean.Meta.Grind
 
-builtin_initialize normExt : SimpExtension ← mkSimpExt
-
-def registerNormTheorems (preDeclNames : Array Name) (postDeclNames : Array Name) : MetaM Unit := do
-  let thms ← normExt.getTheorems
-  unless thms.lemmaNames.isEmpty do
-    throwError "`grind` normalization theorems have already been initialized"
-  for declName in preDeclNames do
-    addSimpTheorem normExt declName (post := false) (inv := false) .global (eval_prio default)
-  for declName in postDeclNames do
-    addSimpTheorem normExt declName (post := true) (inv := false) .global (eval_prio default)
-
 /-- Returns the array of simprocs used by `grind`. -/
 protected def getSimprocs : MetaM (Array Simprocs) := do
-  let e ← Simp.getSEvalSimprocs
-  /-
-  We don't want to apply `List.reduceReplicate` as a normalization operation in
-  `grind`. Consider the following example:
-  ```
-  example (ys : List α) : n = 0 → List.replicate n ys = [] := by
-    grind only [List.replicate]
-  ```
-  The E-matching module generates the following instance for `List.replicate.eq_1`
-  ```
-  List.replicate 0 [] = []
-  ```
-  We don't want it to be simplified to `[] = []`.
-  -/
-  let e := e.erase ``List.reduceReplicate
-  let e ← addDoNotSimp e
-  return #[e]
+  let s ← grindNormSimprocExt.getSimprocs
+  let s ← addDoNotSimp s
+  return #[s, (← Simp.getSEvalSimprocs)]
 
 /-- Returns the simplification context used by `grind`. -/
 protected def getSimpContext : MetaM Simp.Context := do
-  let thms ← normExt.getTheorems
+  let thms ← grindNormExt.getTheorems
   Simp.mkContext
     (config := { arith := true })
     (simpTheorems := #[thms])

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

@@ -13,7 +13,6 @@ import Lean.Meta.CongrTheorems
 import Lean.Meta.AbstractNestedProofs
 import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.Util
-import Lean.Meta.Tactic.Ext
 import Lean.Meta.Tactic.Grind.ENodeKey
 import Lean.Meta.Tactic.Grind.Attr
 import Lean.Meta.Tactic.Grind.Arith.Types
@@ -396,8 +395,6 @@ structure Goal where
   users when `grind` fails.
   -/
   issues     : List MessageData := []
-  /-- Cached extensionality theorems for types. -/
-  extThms    : PHashMap ENodeKey (Array Ext.ExtTheorem) := {}
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=
@@ -501,9 +498,8 @@ def getENode (e : Expr) : GoalM ENode := do
   (← get).getENode e
 
 /-- Returns the generation of the given term. Is assumes it has been internalized -/
-def getGeneration (e : Expr) : GoalM Nat := do
-  let some n ← getENode? e | return 0
-  return n.generation
+def getGeneration (e : Expr) : GoalM Nat :=
+  return (← getENode e).generation
 
 /-- Returns `true` if `e` is in the equivalence class of `True`. -/
 def isEqTrue (e : Expr) : GoalM Bool := do
@@ -520,8 +516,8 @@ def isEqv (a b : Expr) : GoalM Bool := do
   if isSameExpr a b then
     return true
   else
-    let some na ← getENode? a | return false
-    let some nb ← getENode? b | return false
+    let na ← getENode a
+    let nb ← getENode b
     return isSameExpr na.root nb.root
 
 /-- Returns `true` if the root of its equivalence class. -/
@@ -550,11 +546,6 @@ def getRoot (e : Expr) : GoalM Expr := do
 def getRootENode (e : Expr) : GoalM ENode := do
   getENode (← getRoot e)
 
-/-- Returns the root enode in the equivalence class of `e` if it is in an equivalence class. -/
-def getRootENode? (e : Expr) : GoalM (Option ENode) := do
-  let some n ← getENode? e | return none
-  getENode? n.root
-
 /--
 Returns the next element in the equivalence class of `e`
 if `e` has been internalized in the given goal.
@@ -620,7 +611,7 @@ Records that `parent` is a parent of `child`. This function actually stores the
 information in the root (aka canonical representative) of `child`.
 -/
 def registerParent (parent : Expr) (child : Expr) : GoalM Unit := do
-  let childRoot := (← getRoot? child).getD child
+  let some childRoot ← getRoot? child | return ()
   let parents := if let some parents := (← get).parents.find? { expr := childRoot } then parents else {}
   modify fun s => { s with parents := s.parents.insert { expr := childRoot } (parents.insert parent) }
 
@@ -634,10 +625,12 @@ def getParents (e : Expr) : GoalM ParentSet := do
   return parents
 
 /--
-Removes the entry `e ↦ parents` from the parent map.
+Similar to `getParents`, but also removes the entry `e ↦ parents` from the parent map.
 -/
-def resetParentsOf (e : Expr) : GoalM Unit := do
+def getParentsAndReset (e : Expr) : GoalM ParentSet := do
+  let parents ← getParents e
   modify fun s => { s with parents := s.parents.erase { expr := e } }
+  return parents
 
 /--
 Copy `parents` to the parents of `root`.
@@ -804,18 +797,6 @@ def getENodes : GoalM (Array ENode) := do
     if isSameExpr n.next e then return ()
     curr := n.next
 
-/-- Folds using `f` and `init` over the equivalence class containing `e` -/
-@[inline] def foldEqc (e : Expr) (init : α) (f : ENode → α → GoalM α) : GoalM α := do
-  let mut curr := e
-  let mut r := init
-  repeat
-    let n ← getENode curr
-    r ← f n r
-    if isSameExpr n.next e then return r
-    curr := n.next
-  unreachable!
-  return r
-
 def forEachENode (f : ENode → GoalM Unit) : GoalM Unit := do
   let nodes ← getENodes
   for n in nodes do
@@ -905,25 +886,4 @@ def markCaseSplitAsResolved (e : Expr) : GoalM Unit := do
     trace_goal[grind.split.resolved] "{e}"
     modify fun s => { s with resolvedSplits := s.resolvedSplits.insert { expr := e } }
 
-/--
-Returns extensionality theorems for the given type if available.
-If `Config.ext` is `false`, the result is `#[]`.
--/
-def getExtTheorems (type : Expr) : GoalM (Array Ext.ExtTheorem) := do
-  unless (← getConfig).ext do return #[]
-  if let some thms := (← get).extThms.find? { expr := type } then
-    return thms
-  else
-    let thms ← Ext.getExtTheorems type
-    modify fun s => { s with extThms := s.extThms.insert { expr := type } thms }
-    return thms
-
-/--
-Helper function for instantiating a type class `type`, and
-then using the result to perform `isDefEq x val`.
--/
-def synthesizeInstanceAndAssign (x type : Expr) : MetaM Bool := do
-  let .some val ← trySynthInstance type | return false
-  isDefEq x val
-
 end Lean.Meta.Grind

src/Lean/Meta/WHNF.lean

@@ -104,7 +104,7 @@ Otherwise executes `failK`.
 -- ===========================
 
 private def getFirstCtor (d : Name) : MetaM (Option Name) := do
-  let some (ConstantInfo.inductInfo { ctors := ctor::_, ..}) := (← getEnv).find? d |
+  let some (ConstantInfo.inductInfo { ctors := ctor::_, ..}) ← getUnfoldableConstNoEx? d |
     return none
   return some ctor
 
@@ -258,7 +258,7 @@ private def reduceQuotRec (recVal  : QuotVal) (recArgs : Array Expr) (failK : Un
       let major ← whnf major
       match major with
       | Expr.app (Expr.app (Expr.app (Expr.const majorFn _) _) _) majorArg => do
-        let some (ConstantInfo.quotInfo { kind := QuotKind.ctor, .. }) := (← getEnv).find? majorFn | failK ()
+        let some (ConstantInfo.quotInfo { kind := QuotKind.ctor, .. }) ← getUnfoldableConstNoEx? majorFn | failK ()
         let f := recArgs[argPos]!
         let r := mkApp f majorArg
         let recArity := majorPos + 1
@@ -321,7 +321,7 @@ mutual
         | .mvar mvarId => return some mvarId
         | _ => getStuckMVar? e
       | .const fName _ =>
-        match (← getEnv).find? fName with
+        match (← getUnfoldableConstNoEx? fName) with
         | some <| .recInfo recVal  => isRecStuck? recVal e.getAppArgs
         | some <| .quotInfo recVal => isQuotRecStuck? recVal e.getAppArgs
         | _  =>
@@ -625,18 +625,17 @@ where
           | .partialApp   => pure e
           | .stuck _      => pure e
           | .notMatcher   =>
-            let .const cname lvls := f' | return e
-            let some cinfo := (← getEnv).find? cname | return e
-            match cinfo with
-            | .recInfo rec    => reduceRec rec lvls e.getAppArgs (fun _ => return e) (fun e => do recordUnfold cinfo.name; go e)
-            | .quotInfo rec   => reduceQuotRec rec e.getAppArgs (fun _ => return e) (fun e => do recordUnfold cinfo.name; go e)
-            | c@(.defnInfo _) => do
-              if (← isAuxDef c.name) then
-                recordUnfold c.name
-                deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => return e) go
-              else
-                return e
-            | _ => return e
+            matchConstAux f' (fun _ => return e) fun cinfo lvls =>
+              match cinfo with
+              | .recInfo rec    => reduceRec rec lvls e.getAppArgs (fun _ => return e) (fun e => do recordUnfold cinfo.name; go e)
+              | .quotInfo rec   => reduceQuotRec rec e.getAppArgs (fun _ => return e) (fun e => do recordUnfold cinfo.name; go e)
+              | c@(.defnInfo _) => do
+                if (← isAuxDef c.name) then
+                  recordUnfold c.name
+                  deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => return e) go
+                else
+                  return e
+              | _ => return e
       | .proj _ i c =>
         let k (c : Expr) := do
           match (← projectCore? c i) with
@@ -861,9 +860,7 @@ def reduceRecMatcher? (e : Expr) : MetaM (Option Expr) := do
     return none
   else match (← reduceMatcher? e) with
     | .reduced e => return e
-    | _ =>
-      let .const cname lvls := e.getAppFn | return none
-      let some cinfo := (← getEnv).find? cname | return none
+    | _ => matchConstAux e.getAppFn (fun _ => pure none) fun cinfo lvls => do
       match cinfo with
       | .recInfo «rec»  => reduceRec «rec» lvls e.getAppArgs (fun _ => pure none) (fun e => do recordUnfold cinfo.name; pure (some e))
       | .quotInfo «rec» => reduceQuotRec «rec» e.getAppArgs (fun _ => pure none) (fun e => do recordUnfold cinfo.name; pure (some e))

src/Lean/Modifiers.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Environment
-import Lean.PrivateName
 
 namespace Lean
 
@@ -17,12 +16,69 @@ def addProtected (env : Environment) (n : Name) : Environment :=
 def isProtected (env : Environment) (n : Name) : Bool :=
   protectedExt.isTagged env n
 
+/-! # Private name support.
+
+   Suppose the user marks as declaration `n` as private. Then, we create
+   the name: `_private.<module_name>.0 ++ n`.
+   We say `_private.<module_name>.0` is the "private prefix"
+
+   We assume that `n` is a valid user name and does not contain
+   `Name.num` constructors. Thus, we can easily convert from
+   private internal name to the user given name.
+-/
+
+def privateHeader : Name := `_private
+
 def mkPrivateName (env : Environment) (n : Name) : Name :=
   Name.mkNum (privateHeader ++ env.mainModule) 0 ++ n
 
+def isPrivateName : Name → Bool
+  | n@(.str p _) => n == privateHeader || isPrivateName p
+  | .num p _     => isPrivateName p
+  | _            => false
+
+@[export lean_is_private_name]
+def isPrivateNameExport (n : Name) : Bool :=
+  isPrivateName n
+
+/--
+Return `true` if `n` is of the form `_private.<module_name>.0`
+See comment above.
+-/
+def isPrivatePrefix (n : Name) : Bool :=
+  match n with
+  | .num p 0 => go p
+  | _ => false
+where
+  go (n : Name) : Bool :=
+    n == privateHeader ||
+    match n with
+    | .str p _ => go p
+    | _ => false
+
+private def privateToUserNameAux (n : Name) : Name :=
+  match n with
+  | .str p s => .str (privateToUserNameAux p) s
+  | .num p i => if isPrivatePrefix n then .anonymous else .num (privateToUserNameAux p) i
+  | _        => .anonymous
+
+@[export lean_private_to_user_name]
+def privateToUserName? (n : Name) : Option Name :=
+  if isPrivateName n then privateToUserNameAux n
+  else none
+
 def isPrivateNameFromImportedModule (env : Environment) (n : Name) : Bool :=
   match privateToUserName? n with
   | some userName => mkPrivateName env userName != n
   | _ => false
 
+private def privatePrefixAux : Name → Name
+  | .str p _ => privatePrefixAux p
+  | n        => n
+
+@[export lean_private_prefix]
+def privatePrefix? (n : Name) : Option Name :=
+  if isPrivateName n then privatePrefixAux n
+  else none
+
 end Lean

src/Lean/PrivateName.lean

@@ -1,75 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Notation
-
-namespace Lean
-
-/-! # Private name support.
-
-   Suppose the user marks as declaration `n` as private. Then, we create
-   the name: `_private.<module_name>.0 ++ n`.
-   We say `_private.<module_name>.0` is the "private prefix"
-
-   We assume that `n` is a valid user name and does not contain
-   `Name.num` constructors. Thus, we can easily convert from
-   private internal name to the user given name.
--/
-
-def privateHeader : Name := `_private
-
-def mkPrivateNameCore (mainModule : Name) (n : Name) : Name :=
-  Name.mkNum (privateHeader ++ mainModule) 0 ++ n
-
-def isPrivateName : Name → Bool
-  | n@(.str p _) => n == privateHeader || isPrivateName p
-  | .num p _     => isPrivateName p
-  | _            => false
-
-@[export lean_is_private_name]
-def isPrivateNameExport (n : Name) : Bool :=
-  isPrivateName n
-
-/--
-Return `true` if `n` is of the form `_private.<module_name>.0`
-See comment above.
--/
-def isPrivatePrefix (n : Name) : Bool :=
-  match n with
-  | .num p 0 => go p
-  | _ => false
-where
-  go (n : Name) : Bool :=
-    n == privateHeader ||
-    match n with
-    | .str p _ => go p
-    | _ => false
-
-private def privateToUserNameAux (n : Name) : Name :=
-  match n with
-  | .str p s => .str (privateToUserNameAux p) s
-  | .num p i => if isPrivatePrefix n then .anonymous else .num (privateToUserNameAux p) i
-  | _        => .anonymous
-
-@[export lean_private_to_user_name]
-def privateToUserName? (n : Name) : Option Name :=
-  if isPrivateName n then privateToUserNameAux n
-  else none
-
-def privateToUserName (n : Name) : Name :=
-  if isPrivateName n then privateToUserNameAux n
-  else n
-
-private def privatePrefixAux : Name → Name
-  | .str p _ => privatePrefixAux p
-  | n        => n
-
-@[export lean_private_prefix]
-def privatePrefix? (n : Name) : Option Name :=
-  if isPrivateName n then privatePrefixAux n
-  else none
-
-end Lean

src/Lean/Replay.lean

@@ -49,13 +49,15 @@ def isTodo (name : Name) : M Bool := do
   else
     return false
 
-/-- Use the current `Environment` to throw a `Kernel.Exception`. -/
-def throwKernelException (ex : Kernel.Exception) : M Unit := do
-  throw <| .userError <| (← ex.toMessageData {} |>.toString)
+/-- Use the current `Environment` to throw a `KernelException`. -/
+def throwKernelException (ex : KernelException) : M Unit := do
+    let ctx := { fileName := "", options := ({} : KVMap), fileMap := default }
+    let state := { env := (← get).env }
+    Prod.fst <$> (Lean.Core.CoreM.toIO · ctx state) do Lean.throwKernelException ex
 
-/-- Add a declaration, possibly throwing a `Kernel.Exception`. -/
+/-- Add a declaration, possibly throwing a `KernelException`. -/
 def addDecl (d : Declaration) : M Unit := do
-  match (← get).env.addDeclCore 0 d (cancelTk? := none) with
+  match (← get).env.addDecl {} d with
   | .ok env => modify fun s => { s with env := env }
   | .error ex => throwKernelException ex
 

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

@@ -74,6 +74,9 @@ instance [Clause α β] : Entails α β where
 instance [Clause α β] (p : α → Bool) (c : β) : Decidable (p ⊨ c) :=
   inferInstanceAs (Decidable (Clause.eval p c = true))
 
+instance [Clause α β] : Inhabited β where
+  default := empty
+
 end Clause
 
 /--

src/kernel/environment.cpp

@@ -19,9 +19,16 @@ Author: Leonardo de Moura
 
 namespace lean {
 extern "C" object* lean_environment_add(object*, object*);
+extern "C" object* lean_mk_empty_environment(uint32, object*);
 extern "C" object* lean_environment_find(object*, object*);
+extern "C" uint32 lean_environment_trust_level(object*);
 extern "C" object* lean_environment_mark_quot_init(object*);
 extern "C" uint8 lean_environment_quot_init(object*);
+extern "C" object* lean_register_extension(object*);
+extern "C" object* lean_get_extension(object*, object*);
+extern "C" object* lean_set_extension(object*, object*, object*);
+extern "C" object* lean_environment_set_main_module(object*, object*);
+extern "C" object* lean_environment_main_module(object*);
 extern "C" object* lean_kernel_record_unfold (object*, object*);
 extern "C" object* lean_kernel_get_diag(object*);
 extern "C" object* lean_kernel_set_diag(object*, object*);
@@ -55,6 +62,14 @@ environment scoped_diagnostics::update(environment const & env) const {
         return env;
 }
 
+environment mk_empty_environment(uint32 trust_lvl) {
+    return get_io_result<environment>(lean_mk_empty_environment(trust_lvl, io_mk_world()));
+}
+
+environment::environment(unsigned trust_lvl):
+    object_ref(mk_empty_environment(trust_lvl)) {
+}
+
 diagnostics environment::get_diag() const {
     return diagnostics(lean_kernel_get_diag(to_obj_arg()));
 }
@@ -63,6 +78,18 @@ environment environment::set_diag(diagnostics const & diag) const {
     return environment(lean_kernel_set_diag(to_obj_arg(), diag.to_obj_arg()));
 }
 
+void environment::set_main_module(name const & n) {
+    m_obj = lean_environment_set_main_module(m_obj, n.to_obj_arg());
+}
+
+name environment::get_main_module() const {
+    return name(lean_environment_main_module(to_obj_arg()));
+}
+
+unsigned environment::trust_lvl() const {
+    return lean_environment_trust_level(to_obj_arg());
+}
+
 bool environment::is_quot_initialized() const {
     return lean_environment_quot_init(to_obj_arg()) != 0;
 }
@@ -270,7 +297,7 @@ environment environment::add(declaration const & d, bool check) const {
 }
 /*
 addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration)
-  (cancelTk? : @& Option IO.CancelToken) : Except Kernel.Exception Environment
+  (cancelTk? : @& Option IO.CancelToken) : Except KernelException Environment
 */
 extern "C" LEAN_EXPORT object * lean_add_decl(object * env, size_t max_heartbeat, object * decl,
     object * opt_cancel_tk) {
@@ -294,6 +321,12 @@ void environment::for_each_constant(std::function<void(constant_info const & d)>
         });
 }
 
+extern "C" obj_res lean_display_stats(obj_arg env, obj_arg w);
+
+void environment::display_stats() const {
+    dec_ref(lean_display_stats(to_obj_arg(), io_mk_world()));
+}
+
 void initialize_environment() {
 }
 

src/kernel/environment.h

@@ -24,6 +24,10 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
+class environment_extension {
+public:
+    virtual ~environment_extension() {}
+};
 
 /* Wrapper for `Kernel.Diagnostics` */
 class diagnostics : public object_ref {
@@ -37,7 +41,7 @@ public:
 };
 
 /*
-Store `Kernel.Diagnostics` (to be stored in `Kernel.Environment.diagnostics`) in `m_diag` IF
+Store `Kernel.Diagnostics` stored in environment extension in `m_diag` IF
 - `Kernel.Diagnostics.enable = true`
 - `collect = true`. This is a minor optimization.
 
@@ -55,7 +59,6 @@ public:
     diagnostics * get() const { return m_diag; }
 };
 
-/* Wrapper for `Lean.Kernel.Environment` */
 class LEAN_EXPORT environment : public object_ref {
     friend class add_inductive_fn;
 
@@ -73,6 +76,7 @@ class LEAN_EXPORT environment : public object_ref {
     environment add_quot() const;
     environment add_inductive(declaration const & d) const;
 public:
+    environment(unsigned trust_lvl = 0);
     environment(environment const & other):object_ref(other) {}
     environment(environment && other):object_ref(other) {}
     explicit environment(b_obj_arg o, bool b):object_ref(o, b) {}
@@ -85,8 +89,15 @@ public:
     diagnostics get_diag() const;
     environment set_diag(diagnostics const & diag) const;
 
+    /** \brief Return the trust level of this environment. */
+    unsigned trust_lvl() const;
+
     bool is_quot_initialized() const;
 
+    void set_main_module(name const & n);
+
+    name get_main_module() const;
+
     /** \brief Return information for the constant with name \c n (if it is defined in this environment). */
     optional<constant_info> find(name const & n) const;
 
@@ -103,6 +114,8 @@ public:
     friend bool is_eqp(environment const & e1, environment const & e2) {
         return e1.raw() == e2.raw();
     }
+
+    void display_stats() const;
 };
 
 void check_no_metavar_no_fvar(environment const & env, name const & n, expr const & e);

src/kernel/kernel_exception.h

@@ -152,9 +152,9 @@ public:
 /*
 Helper function for interfacing C++ code with code written in Lean.
 It executes closure `f` which produces an object_ref of type `A` and may throw
-an `kernel_exception` or `exception`. Then, convert result into `Except Kernel.Exception T`
+an `kernel_exception` or `exception`. Then, convert result into `Except KernelException T`
 where `T` is the type of the lean objected represented by `A`.
-We use the constructor `Kernel.Exception.other <msg>` to handle C++ `exception` objects which
+We use the constructor `KernelException.other <msg>` to handle C++ `exception` objects which
 are not `kernel_exception`.
 */
 template<typename A>

src/kernel/trace.cpp

@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include <string>
 #include "util/io.h"
 #include "util/option_declarations.h"
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 #include "kernel/local_ctx.h"
 #include "kernel/trace.h"
 
@@ -17,7 +17,7 @@ static name_set *            g_trace_classes = nullptr;
 static name_map<name_set>  * g_trace_aliases = nullptr;
 MK_THREAD_LOCAL_GET_DEF(std::vector<name>, get_enabled_trace_classes);
 MK_THREAD_LOCAL_GET_DEF(std::vector<name>, get_disabled_trace_classes);
-LEAN_THREAD_PTR(elab_environment,      g_env);
+LEAN_THREAD_PTR(environment,           g_env);
 LEAN_THREAD_PTR(options,               g_opts);
 
 void register_trace_class(name const & n, name const & decl_name) {
@@ -90,7 +90,7 @@ bool is_trace_class_enabled(name const & n) {
 }
 
 
-void scope_trace_env::init(elab_environment * env, options * opts) {
+void scope_trace_env::init(environment * env, options * opts) {
     m_enable_sz  = get_enabled_trace_classes().size();
     m_disable_sz = get_disabled_trace_classes().size();
     m_old_env    = g_env;
@@ -111,12 +111,12 @@ void scope_trace_env::init(elab_environment * env, options * opts) {
     g_opts = opts;
 }
 
-scope_trace_env::scope_trace_env(elab_environment const & env, options const & o) {
-    init(const_cast<elab_environment*>(&env), const_cast<options*>(&o));
+scope_trace_env::scope_trace_env(environment const & env, options const & o) {
+    init(const_cast<environment*>(&env), const_cast<options*>(&o));
 }
 
 scope_trace_env::~scope_trace_env() {
-    g_env  = const_cast<elab_environment*>(m_old_env);
+    g_env  = const_cast<environment*>(m_old_env);
     g_opts = const_cast<options*>(m_old_opts);
     get_enabled_trace_classes().resize(m_enable_sz);
     get_disabled_trace_classes().resize(m_disable_sz);
@@ -169,7 +169,7 @@ def pretty (f : Format) (w : Nat := defWidth) (indent : Nat := 0) (column := 0)
 */
 extern "C" object * lean_format_pretty(object * f, object * w, object * i, object * c);
 
-std::string pp_expr(elab_environment const & env, options const & opts, local_ctx const & lctx, expr const & e) {
+std::string pp_expr(environment const & env, options const & opts, local_ctx const & lctx, expr const & e) {
     options o = opts;
     // o = o.update(name{"pp", "proofs"}, true); --
     object_ref fmt = get_io_result<object_ref>(lean_pp_expr(env.to_obj_arg(), lean_mk_metavar_ctx(lean_box(0)), lctx.to_obj_arg(), o.to_obj_arg(),
@@ -178,7 +178,7 @@ std::string pp_expr(elab_environment const & env, options const & opts, local_ct
     return str.to_std_string();
 }
 
-std::string pp_expr(elab_environment const & env, options const & opts, expr const & e) {
+std::string pp_expr(environment const & env, options const & opts, expr const & e) {
     local_ctx lctx;
     return pp_expr(env, opts, lctx, e);
 }

src/kernel/trace.h

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <memory>
 #include <string>
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 #include "util/options.h"
 #include "util/message_definitions.h"
 
@@ -20,13 +20,13 @@ bool is_trace_class_enabled(name const & n);
 #define lean_is_trace_enabled(CName) (::lean::is_trace_enabled() && ::lean::is_trace_class_enabled(CName))
 
 class scope_trace_env {
-    unsigned                 m_enable_sz;
-    unsigned                 m_disable_sz;
-    elab_environment const * m_old_env;
-    options     const *      m_old_opts;
-    void init(elab_environment * env, options * opts);
+    unsigned                m_enable_sz;
+    unsigned                m_disable_sz;
+    environment const *     m_old_env;
+    options     const *     m_old_opts;
+    void init(environment * env, options * opts);
 public:
-    scope_trace_env(elab_environment const & env, options const & opts);
+    scope_trace_env(environment const & env, options const & opts);
     ~scope_trace_env();
 };
 

src/kernel/type_checker.cpp

@@ -549,7 +549,7 @@ static expr * g_lean_reduce_bool = nullptr;
 static expr * g_lean_reduce_nat  = nullptr;
 
 namespace ir {
-object * run_boxed_kernel(environment const & env, options const & opts, name const & fn, unsigned n, object **args);
+object * run_boxed(environment const & env, options const & opts, name const & fn, unsigned n, object **args);
 }
 
 expr mk_bool_true();
@@ -560,7 +560,7 @@ optional<expr> reduce_native(environment const & env, expr const & e) {
     expr const & arg = app_arg(e);
     if (!is_constant(arg)) return none_expr();
     if (app_fn(e) == *g_lean_reduce_bool) {
-        object * r = ir::run_boxed_kernel(env, options(), const_name(arg), 0, nullptr);
+        object * r = ir::run_boxed(env, options(), const_name(arg), 0, nullptr);
         if (!lean_is_scalar(r)) {
             lean_dec_ref(r);
             throw kernel_exception(env, "type checker failure, unexpected result value for 'Lean.reduceBool'");
@@ -568,7 +568,7 @@ optional<expr> reduce_native(environment const & env, expr const & e) {
         return lean_unbox(r) == 0 ? some_expr(mk_bool_false()) : some_expr(mk_bool_true());
     }
     if (app_fn(e) == *g_lean_reduce_nat) {
-        object * r = ir::run_boxed_kernel(env, options(), const_name(arg), 0, nullptr);
+        object * r = ir::run_boxed(env, options(), const_name(arg), 0, nullptr);
         if (lean_is_scalar(r) || lean_is_mpz(r)) {
             return some_expr(mk_lit(literal(nat(r))));
         } else {
@@ -1193,6 +1193,24 @@ type_checker::~type_checker() {
         delete m_st;
 }
 
+extern "C" LEAN_EXPORT lean_object * lean_kernel_is_def_eq(lean_object * env, lean_object * lctx, lean_object * a, lean_object * b) {
+    return catch_kernel_exceptions<object*>([&]() {
+        return lean_box(type_checker(environment(env), local_ctx(lctx)).is_def_eq(expr(a), expr(b)));
+    });
+}
+
+extern "C" LEAN_EXPORT lean_object * lean_kernel_whnf(lean_object * env, lean_object * lctx, lean_object * a) {
+    return catch_kernel_exceptions<object*>([&]() {
+        return type_checker(environment(env), local_ctx(lctx)).whnf(expr(a)).steal();
+    });
+}
+
+extern "C" LEAN_EXPORT lean_object * lean_kernel_check(lean_object * env, lean_object * lctx, lean_object * a) {
+    return catch_kernel_exceptions<object*>([&]() {
+        return type_checker(environment(env), local_ctx(lctx)).check(expr(a)).steal();
+    });
+}
+
 inline static expr * new_persistent_expr_const(name const & n) {
     expr * e = new expr(mk_const(n));
     mark_persistent(e->raw());

src/kernel/type_checker.h

@@ -9,7 +9,6 @@ Author: Leonardo de Moura
 #include <memory>
 #include <utility>
 #include <algorithm>
-#include "runtime/flet.h"
 #include "util/lbool.h"
 #include "util/name_set.h"
 #include "util/name_generator.h"
@@ -105,7 +104,6 @@ private:
     optional<expr> reduce_pow(expr const & e);
     optional<expr> reduce_nat(expr const & e);
 public:
-    // The following two constructor are used only by the old compiler and should be deleted with it
     type_checker(state & st, local_ctx const & lctx, definition_safety ds = definition_safety::safe);
     type_checker(state & st, definition_safety ds = definition_safety::safe):type_checker(st, local_ctx(), ds) {}
     type_checker(environment const & env, local_ctx const & lctx, diagnostics * diag = nullptr, definition_safety ds = definition_safety::safe);

src/lake/Lake/Load/Lean/Elab.lean

@@ -81,10 +81,10 @@ def elabConfigFile (pkgDir : FilePath) (lakeOpts : NameMap String)
     return s.commandState.env
 
 /--
-`Lean.Kernel.Environment.add` is now private, this is an exported helper wrapping it for
-`Lean.Environment`.
+`Lean.Environment.add` is now private, but exported as `lean_environment_add`.
+We call it here via `@[extern]` with a mock implementation.
 -/
-@[extern "lake_environment_add"]
+@[extern "lean_environment_add"]
 private opaque addToEnv (env : Environment) (_ : ConstantInfo) : Environment
 
 /--

src/library/CMakeLists.txt

@@ -6,5 +6,4 @@ add_library(library OBJECT expr_lt.cpp
   projection.cpp
   aux_recursors.cpp
   profiling.cpp time_task.cpp
-  formatter.cpp
-  elab_environment.cpp)
+  formatter.cpp)

src/library/aux_recursors.cpp

@@ -10,11 +10,11 @@ namespace lean {
 extern "C" uint8 lean_is_aux_recursor(object * env, object * n);
 extern "C" uint8 lean_is_no_confusion(object * env, object * n);
 
-bool is_aux_recursor(elab_environment const & env, name const & r) {
+bool is_aux_recursor(environment const & env, name const & r) {
     return lean_is_aux_recursor(env.to_obj_arg(), r.to_obj_arg());
 }
 
-bool is_no_confusion(elab_environment const & env, name const & r) {
+bool is_no_confusion(environment const & env, name const & r) {
     return lean_is_no_confusion(env.to_obj_arg(), r.to_obj_arg());
 }
 }

src/library/aux_recursors.h

@@ -5,11 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 
 namespace lean {
 /** \brief Return true iff \c n is the name of an auxiliary recursor.
     \see add_aux_recursor */
-bool is_aux_recursor(elab_environment const & env, name const & n);
-bool is_no_confusion(elab_environment const & env, name const & n);
+bool is_aux_recursor(environment const & env, name const & n);
+bool is_no_confusion(environment const & env, name const & n);
 }

src/library/class.cpp

@@ -15,9 +15,9 @@ extern "C" uint8 lean_is_out_param(object* e);
 extern "C" uint8 lean_has_out_params(object* env, object* n);
 
 bool is_class_out_param(expr const & e) { return lean_is_out_param(e.to_obj_arg()); }
-bool has_class_out_params(elab_environment const & env, name const & c) { return lean_has_out_params(env.to_obj_arg(), c.to_obj_arg()); }
-bool is_class(elab_environment const & env, name const & c) { return lean_is_class(env.to_obj_arg(), c.to_obj_arg()); }
-bool is_instance(elab_environment const & env, name const & i) { return lean_is_instance(env.to_obj_arg(), i.to_obj_arg()); }
+bool has_class_out_params(environment const & env, name const & c) { return lean_has_out_params(env.to_obj_arg(), c.to_obj_arg()); }
+bool is_class(environment const & env, name const & c) { return lean_is_class(env.to_obj_arg(), c.to_obj_arg()); }
+bool is_instance(environment const & env, name const & i) { return lean_is_instance(env.to_obj_arg(), i.to_obj_arg()); }
 
 static name * g_anonymous_inst_name_prefix = nullptr;
 

src/library/class.h

@@ -6,12 +6,11 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "library/util.h"
-#include "library/elab_environment.h"
 namespace lean {
 /** \brief Return true iff \c c was declared with \c add_class. */
-bool is_class(elab_environment const & env, name const & c);
+bool is_class(environment const & env, name const & c);
 /** \brief Return true iff \c i was declared with \c add_instance. */
-bool is_instance(elab_environment const & env, name const & i);
+bool is_instance(environment const & env, name const & i);
 
 name const & get_anonymous_instance_prefix();
 name mk_anonymous_inst_name(unsigned idx);
@@ -21,7 +20,7 @@ bool is_anonymous_inst_name(name const & n);
 bool is_class_out_param(expr const & e);
 
 /** \brief Return true iff c is a type class that contains an `outParam` */
-bool has_class_out_params(elab_environment const & env, name const & c);
+bool has_class_out_params(environment const & env, name const & c);
 
 void initialize_class();
 void finalize_class();

src/library/compiler/closed_term_cache.cpp

@@ -5,17 +5,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "library/util.h"
-#include "library/elab_environment.h"
 
 namespace lean {
 extern "C" object * lean_cache_closed_term_name(object * env, object * e, object * n);
 extern "C" object * lean_get_closed_term_name(object * env, object * e);
 
-optional<name> get_closed_term_name(elab_environment const & env, expr const & e) {
+optional<name> get_closed_term_name(environment const & env, expr const & e) {
     return to_optional<name>(lean_get_closed_term_name(env.to_obj_arg(), e.to_obj_arg()));
 }
 
-elab_environment cache_closed_term_name(elab_environment const & env, expr const & e, name const & n) {
-    return elab_environment(lean_cache_closed_term_name(env.to_obj_arg(), e.to_obj_arg(), n.to_obj_arg()));
+environment cache_closed_term_name(environment const & env, expr const & e, name const & n) {
+    return environment(lean_cache_closed_term_name(env.to_obj_arg(), e.to_obj_arg(), n.to_obj_arg()));
 }
 }

src/library/compiler/closed_term_cache.h

@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 namespace lean {
-optional<name> get_closed_term_name(elab_environment const & env, expr const & e);
-elab_environment cache_closed_term_name(elab_environment const & env, expr const & e, name const & n);
+optional<name> get_closed_term_name(environment const & env, expr const & e);
+environment cache_closed_term_name(environment const & env, expr const & e, name const & n);
 }

src/library/compiler/compiler.cpp

@@ -44,19 +44,19 @@ static name get_real_name(name const & n) {
         return n;
 }
 
-static comp_decls to_comp_decls(elab_environment const & env, names const & cs) {
+static comp_decls to_comp_decls(environment const & env, names const & cs) {
     bool allow_opaque = true;
     return map2<comp_decl>(cs, [&](name const & n) {
             return comp_decl(get_real_name(n), env.get(n).get_value(allow_opaque));
         });
 }
 
-static expr eta_expand(elab_environment const & env, expr const & e) {
-    return type_checker(env.to_kernel_env()).eta_expand(e);
+static expr eta_expand(environment const & env, expr const & e) {
+    return type_checker(env).eta_expand(e);
 }
 
 template<typename F>
-comp_decls apply(F && f, elab_environment const & env, comp_decls const & ds) {
+comp_decls apply(F && f, environment const & env, comp_decls const & ds) {
     return map(ds, [&](comp_decl const & d) { return comp_decl(d.fst(), f(env, d.snd())); });
 }
 
@@ -75,7 +75,7 @@ void trace_comp_decls(comp_decls const & ds) {
     }
 }
 
-static elab_environment cache_stage1(elab_environment env, comp_decls const & ds) {
+static environment cache_stage1(environment env, comp_decls const & ds) {
     for (comp_decl const & d : ds) {
         name n = d.fst();
         expr v = d.snd();
@@ -94,7 +94,7 @@ static expr ensure_arity(expr const & t, unsigned arity) {
     return update_binding(t, binding_domain(t), ensure_arity(binding_body(t), arity-1));
 }
 
-static elab_environment cache_stage2(elab_environment env, comp_decls const & ds, bool only_new_ones = false) {
+static environment cache_stage2(environment env, comp_decls const & ds, bool only_new_ones = false) {
     buffer<expr> ts;
     ll_infer_type(env, ds, ts);
     lean_assert(ts.size() == length(ds));
@@ -116,11 +116,11 @@ static elab_environment cache_stage2(elab_environment env, comp_decls const & ds
 }
 
 /* Cache the declarations in `ds` that have not already been cached. */
-static elab_environment cache_new_stage2(elab_environment env, comp_decls const & ds) {
+static environment cache_new_stage2(environment env, comp_decls const & ds) {
     return cache_stage2(env, ds, true);
 }
 
-bool is_main_fn(elab_environment const & env, name const & n) {
+bool is_main_fn(environment const & env, name const & n) {
     if (n == "main") return true;
     if (optional<name> c = get_export_name_for(env, n)) {
         return *c == "main";
@@ -160,15 +160,15 @@ bool is_main_fn_type(expr const & type) {
 
 extern "C" object* lean_csimp_replace_constants(object* env, object* n);
 
-expr csimp_replace_constants(elab_environment const & env, expr const & e) {
+expr csimp_replace_constants(environment const & env, expr const & e) {
     return expr(lean_csimp_replace_constants(env.to_obj_arg(), e.to_obj_arg()));
 }
 
-bool is_matcher(elab_environment const & env, comp_decls const & ds) {
+bool is_matcher(environment const & env, comp_decls const & ds) {
     return length(ds) == 1 && is_matcher(env, head(ds).fst());
 }
 
-elab_environment compile(elab_environment const & env, options const & opts, names cs) {
+environment compile(environment const & env, options const & opts, names cs) {
     /* Do not generate code for irrelevant decls */
     cs = filter(cs, [&](name const & c) { return !is_irrelevant_type(env, env.get(c).get_type());});
     if (empty(cs)) return env;
@@ -202,8 +202,8 @@ elab_environment compile(elab_environment const & env, options const & opts, nam
     csimp_cfg cfg(opts);
     // Use the following line to see compiler intermediate steps
     // scope_traces_as_string trace_scope;
-    auto simp  = [&](elab_environment const & env, expr const & e) { return csimp(env, e, cfg); };
-    auto esimp = [&](elab_environment const & env, expr const & e) { return cesimp(env, e, cfg); };
+    auto simp  = [&](environment const & env, expr const & e) { return csimp(env, e, cfg); };
+    auto esimp = [&](environment const & env, expr const & e) { return cesimp(env, e, cfg); };
     trace_compiler(name({"compiler", "input"}), ds);
     ds = apply(eta_expand, env, ds);
     trace_compiler(name({"compiler", "eta_expand"}), ds);
@@ -218,7 +218,7 @@ elab_environment compile(elab_environment const & env, options const & opts, nam
     ds = apply(simp, env, ds);
     trace_compiler(name({"compiler", "simp"}), ds);
     // trace(ds);
-    elab_environment new_env = env;
+    environment new_env = env;
     std::tie(new_env, ds) = eager_lambda_lifting(new_env, ds, cfg);
     trace_compiler(name({"compiler", "eager_lambda_lifting"}), ds);
     ds = apply(max_sharing, ds);
@@ -274,8 +274,8 @@ elab_environment compile(elab_environment const & env, options const & opts, nam
 }
 
 extern "C" LEAN_EXPORT object * lean_compile_decls(object * env, object * opts, object * decls) {
-    return catch_kernel_exceptions<elab_environment>([&]() {
-            return compile(elab_environment(env), options(opts, true), names(decls, true));
+    return catch_kernel_exceptions<environment>([&]() {
+            return compile(environment(env), options(opts, true), names(decls, true));
         });
 }
 

src/library/compiler/compiler.h

@@ -5,10 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 namespace lean {
-elab_environment compile(elab_environment const & env, options const & opts, names cs);
-inline elab_environment compile(elab_environment const & env, options const & opts, name const & c) {
+environment compile(environment const & env, options const & opts, names cs);
+inline environment compile(environment const & env, options const & opts, name const & c) {
     return compile(env, opts, names(c));
 }
 void initialize_compiler();

src/library/compiler/cse.cpp

@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include <vector>
 #include "runtime/flet.h"
 #include "util/name_generator.h"
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "kernel/for_each_fn.h"
@@ -21,7 +21,7 @@ namespace lean {
 static name * g_cse_fresh = nullptr;
 
 class cse_fn {
-    elab_environment  m_env;
+    environment       m_env;
     name_generator    m_ngen;
     bool              m_before_erasure;
     expr_map<expr>    m_map;
@@ -148,14 +148,14 @@ public:
     }
 
 public:
-    cse_fn(elab_environment const & env, bool before_erasure):
+    cse_fn(environment const & env, bool before_erasure):
         m_env(env), m_ngen(*g_cse_fresh), m_before_erasure(before_erasure) {
     }
 
     expr operator()(expr const & e) { return visit(e); }
 };
 
-expr cse_core(elab_environment const & env, expr const & e, bool before_erasure) {
+expr cse_core(environment const & env, expr const & e, bool before_erasure) {
     return cse_fn(env, before_erasure)(e);
 }
 
@@ -170,7 +170,6 @@ expr cse_core(elab_environment const & env, expr const & e, bool before_erasure)
    ```
    The "else"-branch is duplicated by the equation compiler for each constructor different from `expr.app`. */
 class cce_fn {
-    elab_environment    m_env;
     type_checker::state m_st;
     local_ctx           m_lctx;
     buffer<expr>        m_fvars;
@@ -179,7 +178,7 @@ class cce_fn {
     name                m_j;
     unsigned            m_next_idx{1};
 public:
-    elab_environment & env() { return m_env; }
+    environment & env() { return m_st.env(); }
 
     name_generator & ngen() { return m_st.ngen(); }
 
@@ -395,8 +394,8 @@ public:
     }
 
 public:
-    cce_fn(elab_environment const & env, local_ctx const & lctx):
-        m_env(env), m_st(env), m_lctx(lctx), m_j("_j") {
+    cce_fn(environment const & env, local_ctx const & lctx):
+        m_st(env), m_lctx(lctx), m_j("_j") {
     }
 
     expr operator()(expr const & e) {
@@ -405,7 +404,7 @@ public:
     }
 };
 
-expr cce_core(elab_environment const & env, local_ctx const & lctx, expr const & e) {
+expr cce_core(environment const & env, local_ctx const & lctx, expr const & e) {
     return cce_fn(env, lctx)(e);
 }
 

src/library/compiler/cse.h

@@ -5,15 +5,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 namespace lean {
 /* Common subexpression elimination */
-expr cse_core(elab_environment const & env, expr const & e, bool before_erasure);
-inline expr cse(elab_environment const & env, expr const & e) { return cse_core(env, e, true); }
-inline expr ecse(elab_environment const & env, expr const & e) { return cse_core(env, e, false); }
+expr cse_core(environment const & env, expr const & e, bool before_erasure);
+inline expr cse(environment const & env, expr const & e) { return cse_core(env, e, true); }
+inline expr ecse(environment const & env, expr const & e) { return cse_core(env, e, false); }
 /* Common case elimination */
-expr cce_core(elab_environment const & env, local_ctx const & lctx, expr const & e);
-inline expr cce(elab_environment const & env, expr const & e) { return cce_core(env, local_ctx(), e); }
+expr cce_core(environment const & env, local_ctx const & lctx, expr const & e);
+inline expr cce(environment const & env, expr const & e) { return cce_core(env, local_ctx(), e); }
 void initialize_cse();
 void finalize_cse();
 }

src/library/compiler/csimp.cpp

@@ -64,7 +64,6 @@ optional<expr> fold_bin_op(bool before_erasure, expr const & f, expr const & a,
 
 class csimp_fn {
     typedef expr_pair_struct_map<expr> jp_cache;
-    elab_environment         m_env;
     type_checker::state      m_st;
     local_ctx                m_lctx;
     bool                     m_before_erasure;
@@ -97,7 +96,7 @@ class csimp_fn {
     typedef rb_expr_map<expr> expr2ctor;
     expr2ctor                m_expr2ctor;
 
-    elab_environment const & env() const { return m_env; }
+    environment const & env() const { return m_st.env(); }
 
     name_generator & ngen() { return m_st.ngen(); }
 
@@ -1626,12 +1625,12 @@ class csimp_fn {
     }
 
     struct is_recursive_fn {
-        elab_environment const & m_env;
+        environment const & m_env;
         csimp_cfg const &   m_cfg;
         bool                m_before_erasure;
         name                m_target;
 
-        is_recursive_fn(elab_environment const & env, csimp_cfg const & cfg, bool before_erasure):
+        is_recursive_fn(environment const & env, csimp_cfg const & cfg, bool before_erasure):
             m_env(env), m_cfg(cfg), m_before_erasure(before_erasure) {
         }
 
@@ -1970,8 +1969,8 @@ class csimp_fn {
     }
 
 public:
-    csimp_fn(elab_environment const & env, local_ctx const & lctx, bool before_erasure, csimp_cfg const & cfg):
-        m_env(env), m_st(env), m_lctx(lctx), m_before_erasure(before_erasure), m_cfg(cfg), m_x("_x"), m_j("j") {}
+    csimp_fn(environment const & env, local_ctx const & lctx, bool before_erasure, csimp_cfg const & cfg):
+        m_st(env), m_lctx(lctx), m_before_erasure(before_erasure), m_cfg(cfg), m_x("_x"), m_j("j") {}
 
     expr operator()(expr const & e) {
         if (is_lambda(e)) {
@@ -1993,7 +1992,7 @@ bool at_most_once(expr const & e, name const & x) {
 
 /* Eliminate join-points that are used only once */
 class elim_jp1_fn {
-    elab_environment const & m_env;
+    environment const & m_env;
     local_ctx           m_lctx;
     bool                m_before_erasure;
     name_generator      m_ngen;
@@ -2094,7 +2093,7 @@ class elim_jp1_fn {
     }
 
 public:
-    elim_jp1_fn(elab_environment const & env, local_ctx const & lctx, bool before_erasure):
+    elim_jp1_fn(environment const & env, local_ctx const & lctx, bool before_erasure):
         m_env(env), m_lctx(lctx), m_before_erasure(before_erasure) {}
     expr operator()(expr const & e) {
         m_expanded = false;
@@ -2104,7 +2103,7 @@ public:
     bool expanded() const { return m_expanded; }
 };
 
-expr csimp_core(elab_environment const & env, local_ctx const & lctx, expr const & e0, bool before_erasure, csimp_cfg const & cfg) {
+expr csimp_core(environment const & env, local_ctx const & lctx, expr const & e0, bool before_erasure, csimp_cfg const & cfg) {
     csimp_fn simp(env, lctx, before_erasure, cfg);
     elim_jp1_fn elim_jp1(env, lctx, before_erasure);
     expr e = e0;

src/library/compiler/csimp.h

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 namespace lean {
 struct csimp_cfg {
     /* If `m_inline` == false, then we will not inline `c` even if it is marked with the attribute `[inline]`. */
@@ -23,11 +23,11 @@ public:
     csimp_cfg();
 };
 
-expr csimp_core(elab_environment const & env, local_ctx const & lctx, expr const & e, bool before_erasure, csimp_cfg const & cfg);
-inline expr csimp(elab_environment const & env, expr const & e, csimp_cfg const & cfg = csimp_cfg()) {
+expr csimp_core(environment const & env, local_ctx const & lctx, expr const & e, bool before_erasure, csimp_cfg const & cfg);
+inline expr csimp(environment const & env, expr const & e, csimp_cfg const & cfg = csimp_cfg()) {
     return csimp_core(env, local_ctx(), e, true, cfg);
 }
-inline expr cesimp(elab_environment const & env, expr const & e, csimp_cfg const & cfg = csimp_cfg()) {
+inline expr cesimp(environment const & env, expr const & e, csimp_cfg const & cfg = csimp_cfg()) {
     return csimp_core(env, local_ctx(), e, false, cfg);
 }
 }

src/library/compiler/eager_lambda_lifting.cpp

@@ -98,7 +98,6 @@ static bool depends_on_fvar(local_ctx const & lctx, buffer<expr> const & params,
    Remark: we also skip this transformation for definitions marked as `[inline]` or `[instance]`.
 */
 class eager_lambda_lifting_fn {
-    elab_environment    m_env;
     type_checker::state m_st;
     csimp_cfg           m_cfg;
     local_ctx           m_lctx;
@@ -109,7 +108,7 @@ class eager_lambda_lifting_fn {
     name_set            m_nonterminal_lambdas;
     unsigned            m_next_idx{1};
 
-    elab_environment const & env() const { return m_env; }
+    environment const & env() const { return m_st.env(); }
 
     name_generator & ngen() { return m_st.ngen(); }
 
@@ -235,13 +234,12 @@ class eager_lambda_lifting_fn {
             }
             expr type = cheap_beta_reduce(type_checker(m_st).infer(code));
             name n    = next_name();
-            /* We add the auxiliary declaration `n` as a "meta" axiom to the elab_environment.
+            /* We add the auxiliary declaration `n` as a "meta" axiom to the environment.
                This is a hack to make sure we can use `csimp` to simplify `code` and
                other definitions that use `n`.
                We used a similar hack at `specialize.cpp`. */
             declaration aux_ax = mk_axiom(n, names(), type, true /* meta */);
-            m_env = m_env.add(aux_ax, false);
-            m_st.env() = m_env;
+            m_st.env() = env().add(aux_ax, false);
             m_new_decls.push_back(comp_decl(n, code));
             return mk_app(mk_constant(n), new_params);
         } catch (exception &) {
@@ -400,10 +398,10 @@ class eager_lambda_lifting_fn {
     }
 
 public:
-    eager_lambda_lifting_fn(elab_environment const & env, csimp_cfg const & cfg):
-        m_env(env), m_st(env), m_cfg(cfg) {}
+    eager_lambda_lifting_fn(environment const & env, csimp_cfg const & cfg):
+        m_st(env), m_cfg(cfg) {}
 
-    pair<elab_environment, comp_decls> operator()(comp_decl const & cdecl) {
+    pair<environment, comp_decls> operator()(comp_decl const & cdecl) {
         m_base_name = cdecl.fst();
         expr r = visit(cdecl.snd(), true);
         comp_decl new_cdecl(cdecl.fst(), r);
@@ -412,7 +410,7 @@ public:
     }
 };
 
-pair<elab_environment, comp_decls> eager_lambda_lifting(elab_environment env, comp_decls const & ds, csimp_cfg const & cfg) {
+pair<environment, comp_decls> eager_lambda_lifting(environment env, comp_decls const & ds, csimp_cfg const & cfg) {
     comp_decls r;
     for (comp_decl const & d : ds) {
         if (has_inline_attribute(env, d.fst()) || is_instance(env, d.fst())) {

src/library/compiler/eager_lambda_lifting.h

@@ -5,11 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 #include "library/compiler/csimp.h"
 namespace lean {
 /** \brief Eager version of lambda lifting. See comment at eager_lambda_lifting.cpp. */
-pair<elab_environment, comp_decls> eager_lambda_lifting(elab_environment env, comp_decls const & ds, csimp_cfg const & cfg);
+pair<environment, comp_decls> eager_lambda_lifting(environment env, comp_decls const & ds, csimp_cfg const & cfg);
 /* Return true iff `fn` is the name of an auxiliary function generated by `eager_lambda_lifting`. */
 bool is_elambda_lifting_name(name fn);
 };

src/library/compiler/erase_irrelevant.cpp

@@ -16,7 +16,6 @@ Author: Leonardo de Moura
 namespace lean {
 class erase_irrelevant_fn {
     typedef std::tuple<name, expr, expr> let_entry;
-    elab_environment     m_env;
     type_checker::state  m_st;
     local_ctx            m_lctx;
     buffer<expr>         m_let_fvars;
@@ -25,7 +24,7 @@ class erase_irrelevant_fn {
     unsigned             m_next_idx{1};
     expr_map<bool>       m_irrelevant_cache;
 
-    elab_environment & env() { return m_env; }
+    environment & env() { return m_st.env(); }
 
     name_generator & ngen() { return m_st.ngen(); }
 
@@ -486,14 +485,14 @@ class erase_irrelevant_fn {
         lean_unreachable();
     }
 public:
-    erase_irrelevant_fn(elab_environment const & env, local_ctx const & lctx):
-        m_env(env), m_st(env), m_lctx(lctx), m_x("_x") {}
+    erase_irrelevant_fn(environment const & env, local_ctx const & lctx):
+        m_st(env), m_lctx(lctx), m_x("_x") {}
     expr operator()(expr const & e) {
         return mk_let(0, visit(e));
     }
 };
 
-expr erase_irrelevant_core(elab_environment const & env, local_ctx const & lctx, expr const & e) {
+expr erase_irrelevant_core(environment const & env, local_ctx const & lctx, expr const & e) {
     return erase_irrelevant_fn(env, lctx)(e);
 }
 }

src/library/compiler/erase_irrelevant.h

@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 namespace lean {
-expr erase_irrelevant_core(elab_environment const & env, local_ctx const & lctx, expr const & e);
-inline expr erase_irrelevant(elab_environment const & env, expr const & e) { return erase_irrelevant_core(env, local_ctx(), e); }
+expr erase_irrelevant_core(environment const & env, local_ctx const & lctx, expr const & e);
+inline expr erase_irrelevant(environment const & env, expr const & e) { return erase_irrelevant_core(env, local_ctx(), e); }
 }

src/library/compiler/export_attribute.cpp

@@ -6,11 +6,10 @@ Author: Leonardo de Moura
 */
 #include "library/constants.h"
 #include "library/util.h"
-#include "library/elab_environment.h"
 
 namespace lean {
 extern "C" object* lean_get_export_name_for(object* env, object *n);
-optional<name> get_export_name_for(elab_environment const & env, name const & n) {
+optional<name> get_export_name_for(environment const & env, name const & n) {
     return to_optional<name>(lean_get_export_name_for(env.to_obj_arg(), n.to_obj_arg()));
 }
 }

src/library/compiler/export_attribute.h

@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 namespace lean {
-optional<name> get_export_name_for(elab_environment const & env, name const & n);
-inline bool has_export_name(elab_environment const & env, name const & n) { return static_cast<bool>(get_export_name_for(env, n)); }
+optional<name> get_export_name_for(environment const & env, name const & n);
+inline bool has_export_name(environment const & env, name const & n) { return static_cast<bool>(get_export_name_for(env, n)); }
 }

src/library/compiler/extern_attribute.cpp

@@ -23,15 +23,15 @@ Authors: Leonardo de Moura
 namespace lean {
 extern "C" object* lean_get_extern_attr_data(object* env, object* n);
 
-optional<extern_attr_data_value> get_extern_attr_data(elab_environment const & env, name const & fn) {
+optional<extern_attr_data_value> get_extern_attr_data(environment const & env, name const & fn) {
     return to_optional<extern_attr_data_value>(lean_get_extern_attr_data(env.to_obj_arg(), fn.to_obj_arg()));
 }
 
-bool is_extern_constant(elab_environment const & env, name const & c) {
+bool is_extern_constant(environment const & env, name const & c) {
     return static_cast<bool>(get_extern_attr_data(env, c));
 }
 
-bool is_extern_or_init_constant(elab_environment const & env, name const & c) {
+bool is_extern_or_init_constant(environment const & env, name const & c) {
     if (is_extern_constant(env, c)) {
         return true;
     } else if (auto info = env.find(c)) {
@@ -44,7 +44,7 @@ bool is_extern_or_init_constant(elab_environment const & env, name const & c) {
 
 extern "C" object * lean_get_extern_const_arity(object* env, object*, object* w);
 
-optional<unsigned> get_extern_constant_arity(elab_environment const & env, name const & c) {
+optional<unsigned> get_extern_constant_arity(environment const & env, name const & c) {
     auto arity = get_io_result<option_ref<nat>>(lean_get_extern_const_arity(env.to_obj_arg(), c.to_obj_arg(), lean_io_mk_world()));
     if (optional<nat> aux = arity.get()) {
         return optional<unsigned>(aux->get_small_value());
@@ -53,7 +53,7 @@ optional<unsigned> get_extern_constant_arity(elab_environment const & env, name
     }
 }
 
-bool get_extern_borrowed_info(elab_environment const & env, name const & c, buffer<bool> & borrowed_args, bool & borrowed_res) {
+bool get_extern_borrowed_info(environment const & env, name const & c, buffer<bool> & borrowed_args, bool & borrowed_res) {
     if (is_extern_constant(env, c)) {
         /* Extract borrowed info from type */
         expr type = env.get(c).get_type();
@@ -80,7 +80,7 @@ bool get_extern_borrowed_info(elab_environment const & env, name const & c, buff
     return false;
 }
 
-optional<expr> get_extern_constant_ll_type(elab_environment const & env, name const & c) {
+optional<expr> get_extern_constant_ll_type(environment const & env, name const & c) {
     if (is_extern_or_init_constant(env, c)) {
         unsigned arity = 0;
         expr type = env.get(c).get_type();

src/library/compiler/extern_attribute.h

@@ -6,15 +6,15 @@ Authors: Leonardo de Moura
 */
 #pragma once
 #include <string>
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 namespace lean {
-bool is_extern_constant(elab_environment const & env, name const & c);
-bool is_extern_or_init_constant(elab_environment const & env, name const & c);
-optional<expr> get_extern_constant_ll_type(elab_environment const & env, name const & c);
-optional<unsigned> get_extern_constant_arity(elab_environment const & env, name const & c);
+bool is_extern_constant(environment const & env, name const & c);
+bool is_extern_or_init_constant(environment const & env, name const & c);
+optional<expr> get_extern_constant_ll_type(environment const & env, name const & c);
+optional<unsigned> get_extern_constant_arity(environment const & env, name const & c);
 typedef object_ref extern_attr_data_value;
-optional<extern_attr_data_value> get_extern_attr_data(elab_environment const & env, name const & c);
+optional<extern_attr_data_value> get_extern_attr_data(environment const & env, name const & c);
 /* Return true if `c` is an extern constant, and store in borrowed_args and
    borrowed_res which arguments/results are marked as borrowed. */
-bool get_extern_borrowed_info(elab_environment const & env, name const & c, buffer<bool> & borrowed_args, bool & borrowed_res);
+bool get_extern_borrowed_info(environment const & env, name const & c, buffer<bool> & borrowed_args, bool & borrowed_res);
 }

src/library/compiler/extract_closed.cpp

@@ -25,7 +25,7 @@ bool is_extract_closed_aux_fn(name const & n) {
 }
 
 class extract_closed_fn {
-    elab_environment    m_env;
+    environment         m_env;
     comp_decls          m_input_decls;
     name_generator      m_ngen;
     local_ctx           m_lctx;
@@ -34,7 +34,7 @@ class extract_closed_fn {
     unsigned            m_next_idx{1};
     expr_map<bool>      m_closed;
 
-    elab_environment const & env() const { return m_env; }
+    environment const & env() const { return m_env; }
     name_generator & ngen() { return m_ngen; }
 
     name next_name() {
@@ -286,11 +286,11 @@ class extract_closed_fn {
     }
 
 public:
-    extract_closed_fn(elab_environment const & env, comp_decls const & ds):
+    extract_closed_fn(environment const & env, comp_decls const & ds):
         m_env(env), m_input_decls(ds) {
     }
 
-    pair<elab_environment, comp_decls> operator()(comp_decl const & d) {
+    pair<environment, comp_decls> operator()(comp_decl const & d) {
         if (arity_was_reduced(d)) {
             /* Do nothing since `d` will be inlined. */
             return mk_pair(env(), comp_decls(d));
@@ -308,11 +308,11 @@ public:
     }
 };
 
-pair<elab_environment, comp_decls> extract_closed_core(elab_environment const & env, comp_decls const & input_ds, comp_decl const & d) {
+pair<environment, comp_decls> extract_closed_core(environment const & env, comp_decls const & input_ds, comp_decl const & d) {
     return extract_closed_fn(env, input_ds)(d);
 }
 
-pair<elab_environment, comp_decls> extract_closed(elab_environment env, comp_decls const & ds) {
+pair<environment, comp_decls> extract_closed(environment env, comp_decls const & ds) {
     comp_decls r;
     for (comp_decl const & d : ds) {
         comp_decls new_ds;

src/library/compiler/extract_closed.h

@@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 #include "library/compiler/util.h"
 namespace lean {
 bool is_extract_closed_aux_fn(name const & n);
-pair<elab_environment, comp_decls> extract_closed(elab_environment env, comp_decls const & ds);
+pair<environment, comp_decls> extract_closed(environment env, comp_decls const & ds);
 }

src/library/compiler/find_jp.cpp

@@ -13,7 +13,7 @@ namespace lean {
 
 /* Find join-points */
 class find_jp_fn {
-    elab_environment const & m_env;
+    environment const & m_env;
     local_ctx           m_lctx;
     name_generator      m_ngen;
     name_map<unsigned>  m_candidates;
@@ -130,7 +130,7 @@ class find_jp_fn {
     }
 
 public:
-    find_jp_fn(elab_environment const & env):
+    find_jp_fn(environment const & env):
         m_env(env) {}
 
     expr operator()(expr const & e) {
@@ -138,7 +138,7 @@ public:
     }
 };
 
-expr find_jp(elab_environment const & env, expr const & e) {
+expr find_jp(environment const & env, expr const & e) {
     return find_jp_fn(env)(e);
 }
 }

src/library/compiler/find_jp.h

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 namespace lean {
-expr find_jp(elab_environment const & env, expr const & e);
+expr find_jp(environment const & env, expr const & e);
 }

src/library/compiler/implemented_by_attribute.cpp

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 namespace lean {
 extern "C" object* lean_get_implemented_by(object*, object*);
 
-optional<name> get_implemented_by_attribute(elab_environment const & env, name const & n) {
+optional<name> get_implemented_by_attribute(environment const & env, name const & n) {
     return to_optional<name>(lean_get_implemented_by(env.to_obj_arg(), n.to_obj_arg()));
 }
 }

src/library/compiler/implemented_by_attribute.h

@@ -5,11 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 
 namespace lean {
-optional<name> get_implemented_by_attribute(elab_environment const & env, name const & n);
-inline bool has_implemented_by_attribute(elab_environment const & env, name const & n) {
+optional<name> get_implemented_by_attribute(environment const & env, name const & n);
+inline bool has_implemented_by_attribute(environment const & env, name const & n) {
     return static_cast<bool>(get_implemented_by_attribute(env, n));
 }
 }

src/library/compiler/init_attribute.cpp

@@ -5,12 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 */
 #include "runtime/object_ref.h"
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 
 namespace lean {
 extern "C" object* lean_get_init_fn_name_for(object* env, object* fn);
 
-optional<name> get_init_fn_name_for(elab_environment const & env, name const & n) {
+optional<name> get_init_fn_name_for(environment const & env, name const & n) {
     return to_optional<name>(lean_get_init_fn_name_for(env.to_obj_arg(), n.to_obj_arg()));
 }
 }

src/library/compiler/init_attribute.h

@@ -5,11 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 */
 #pragma once
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 
 namespace lean {
-optional<name> get_init_fn_name_for(elab_environment const & env, name const & n);
-inline bool has_init_attribute(elab_environment const & env, name const & n) {
+optional<name> get_init_fn_name_for(environment const & env, name const & n);
+inline bool has_init_attribute(environment const & env, name const & n) {
     return static_cast<bool>(get_init_fn_name_for(env, n));
 }
 }

src/library/compiler/ir.cpp

@@ -100,8 +100,8 @@ std::string decl_to_string(decl const & d) {
     string_ref r(lean_ir_decl_to_string(d.to_obj_arg()));
     return r.to_std_string();
 }
-elab_environment add_decl(elab_environment const & env, decl const & d) {
-    return elab_environment(lean_ir_add_decl(env.to_obj_arg(), d.to_obj_arg()));
+environment add_decl(environment const & env, decl const & d) {
+    return environment(lean_ir_add_decl(env.to_obj_arg(), d.to_obj_arg()));
 }
 }
 
@@ -133,13 +133,12 @@ static ir::type to_ir_type(expr const & e) {
 }
 
 class to_ir_fn {
-    elab_environment    m_env;
     type_checker::state m_st;
     local_ctx           m_lctx;
     name                m_x{"x"};
     unsigned            m_next_idx{1};
 
-    elab_environment const & env() const { return m_env; }
+    environment const & env() const { return m_st.env(); }
 
     name_generator & ngen() { return m_st.ngen(); }
 
@@ -494,7 +493,7 @@ class to_ir_fn {
         return ir::mk_decl(fn, xs, type, b);
     }
 public:
-    to_ir_fn(elab_environment const & env):m_env(env), m_st(env) {}
+    to_ir_fn(environment const & env):m_st(env) {}
 
     ir::decl operator()(comp_decl const & d) { return to_ir_decl(d); }
 
@@ -521,7 +520,7 @@ public:
 };
 
 namespace ir {
-decl to_ir_decl(elab_environment const & env, comp_decl const & d) {
+decl to_ir_decl(environment const & env, comp_decl const & d) {
     return to_ir_fn(env)(d);
 }
 
@@ -529,7 +528,7 @@ decl to_ir_decl(elab_environment const & env, comp_decl const & d) {
 @[export lean.ir.compile_core]
 def compile (env : Environment) (opts : Options) (decls : Array Decl) : Log × (Except String Environment) :=
 */
-elab_environment compile(elab_environment const & env, options const & opts, comp_decls const & decls) {
+environment compile(environment const & env, options const & opts, comp_decls const & decls) {
     buffer<decl> ir_decls;
     for (comp_decl const & decl : decls) {
         lean_trace(name({"compiler", "lambda_pure"}),
@@ -550,7 +549,7 @@ elab_environment compile(elab_environment const & env, options const & opts, com
         dec_ref(r);
         throw exception(error.data());
     } else {
-        elab_environment new_env(cnstr_get(v, 0), true);
+        environment new_env(cnstr_get(v, 0), true);
         dec_ref(r);
         return new_env;
     }
@@ -561,28 +560,28 @@ elab_environment compile(elab_environment const & env, options const & opts, com
 def addBoxedVersion (env : Environment) (decl : Decl) : Except String Environment :=
 */
 extern "C" object * lean_ir_add_boxed_version(object * env, object * decl);
-elab_environment add_boxed_version(elab_environment const & env, decl const & d) {
+environment add_boxed_version(environment const & env, decl const & d) {
     object * v = lean_ir_add_boxed_version(env.to_obj_arg(), d.to_obj_arg());
     if (cnstr_tag(v) == 0) {
         string_ref error(cnstr_get(v, 0), true);
         dec_ref(v);
         throw exception(error.data());
     } else {
-        elab_environment new_env(cnstr_get(v, 0), true);
+        environment new_env(cnstr_get(v, 0), true);
         dec_ref(v);
         return new_env;
     }
 }
 
-elab_environment add_extern(elab_environment const & env, name const & fn) {
+environment add_extern(environment const & env, name const & fn) {
     decl d = to_ir_fn(env)(fn);
-    elab_environment new_env = ir::add_decl(env, d);
+    environment new_env = ir::add_decl(env, d);
     return add_boxed_version(new_env, d);
 }
 
 extern "C" LEAN_EXPORT object* lean_add_extern(object * env, object * fn) {
     try {
-        elab_environment new_env = add_extern(elab_environment(env), name(fn));
+        environment new_env = add_extern(environment(env), name(fn));
         return mk_except_ok(new_env);
     } catch (exception & ex) {
         // throw; // We use to uncomment this line when debugging weird bugs in the Lean/C++ interface.
@@ -592,7 +591,7 @@ extern "C" LEAN_EXPORT object* lean_add_extern(object * env, object * fn) {
 
 extern "C" object * lean_ir_emit_c(object * env, object * mod_name);
 
-string_ref emit_c(elab_environment const & env, name const & mod_name) {
+string_ref emit_c(environment const & env, name const & mod_name) {
     object * r = lean_ir_emit_c(env.to_obj_arg(), mod_name.to_obj_arg());
     string_ref s(cnstr_get(r, 0), true);
     if (cnstr_tag(r) == 0) {
@@ -640,7 +639,7 @@ object_ref to_object_ref(cnstr_info const & info) {
 }
 
 extern "C" LEAN_EXPORT object * lean_ir_get_ctor_layout(object * env0, object * ctor_name0) {
-    elab_environment const & env = TO_REF(elab_environment, env0);
+    environment const & env = TO_REF(environment, env0);
     name const & ctor_name  = TO_REF(name, ctor_name0);
     type_checker::state st(env);
     try {

src/library/compiler/ir.h

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <string>
-#include "library/elab_environment.h"
+#include "kernel/environment.h"
 #include "library/compiler/util.h"
 namespace lean {
 namespace ir {
@@ -35,10 +35,10 @@ typedef object_ref decl;
 typedef object_ref decl;
 std::string decl_to_string(decl const & d);
 void test(decl const & d);
-elab_environment compile(elab_environment const & env, options const & opts, comp_decls const & decls);
-elab_environment add_extern(elab_environment const & env, name const & fn);
-LEAN_EXPORT string_ref emit_c(elab_environment const & env, name const & mod_name);
-void emit_llvm(elab_environment const & env, name const & mod_name, std::string const &filepath);
+environment compile(environment const & env, options const & opts, comp_decls const & decls);
+environment add_extern(environment const & env, name const & fn);
+LEAN_EXPORT string_ref emit_c(environment const & env, name const & mod_name);
+void emit_llvm(environment const & env, name const & mod_name, std::string const &filepath);
 }
 void initialize_ir();
 void finalize_ir();