chore: remove dead code at Structure.lean

src/Init/Data/Array/Basic.lean

@@ -31,7 +31,6 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
   go (i : Nat) (acc : Array α) : Array α :=
     if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
 termination_by n - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 /-- The array `#[0, 1, ..., n - 1]`. -/
 def range (n : Nat) : Array Nat :=
@@ -307,7 +306,6 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
     else
       pure r
   termination_by as.size - i
-  decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
 @[inline]
@@ -380,7 +378,6 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
       else
         pure false
       termination_by stop - j
-      decreasing_by simp_wf; decreasing_trivial_pre_omega
     loop start
   if h : stop ≤ as.size then
     any stop h
@@ -466,7 +463,6 @@ def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
       if p as[j] then some j else loop (j + 1)
     else none
     termination_by as.size - j
-    decreasing_by simp_wf; decreasing_trivial_pre_omega
   loop 0
 
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
@@ -561,7 +557,6 @@ def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (
   else
     true
 termination_by a.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 @[inline] def isEqv (a b : Array α) (p : α → α → Bool) : Bool :=
   if h : a.size = b.size then
@@ -666,7 +661,6 @@ def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size)
     else indexOfAux a v (i+1)
   else none
 termination_by a.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
   indexOfAux a v 0
@@ -709,7 +703,6 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
   else
     as
 termination_by as.size
-decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
   let rec go (i : Nat) (r : Array α) : Array α :=
@@ -722,7 +715,6 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
     else
       r
     termination_by as.size - i
-    decreasing_by simp_wf; decreasing_trivial_pre_omega
   go 0 #[]
 
 /-- Remove the element at a given index from an array without bounds checks, using a `Fin` index.
@@ -739,7 +731,6 @@ def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
   else
     a.pop
 termination_by a.size - i.val
-decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
   induction a, i using Array.feraseIdx.induct with
@@ -772,7 +763,6 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
     else
       as
     termination_by j.1
-    decreasing_by simp_wf; decreasing_trivial_pre_omega
   let j := as.size
   let as := as.push a
   loop as ⟨j, size_push .. ▸ j.lt_succ_self⟩
@@ -826,7 +816,6 @@ def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : N
   else
     true
 termination_by as.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 /-- Return true iff `as` is a prefix of `bs`.
 That is, `bs = as ++ t` for some `t : List α`.-/
@@ -848,7 +837,6 @@ private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
   else
     true
 termination_by as.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def allDiff [BEq α] (as : Array α) : Bool :=
   allDiffAux as 0
@@ -864,7 +852,6 @@ def allDiff [BEq α] (as : Array α) : Bool :=
   else
     cs
 termination_by as.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 @[inline] def zipWith (as : Array α) (bs : Array β) (f : α → β → γ) : Array γ :=
   zipWithAux f as bs 0 #[]

src/Init/Data/Array/BasicAux.lean

@@ -48,7 +48,6 @@ where
       let b ← f as[i]
       go (i+1) ⟨acc.val.push b, by simp [acc.property]⟩ hlt
   termination_by as.size - i
-  decreasing_by decreasing_trivial_pre_omega
 
 @[inline] private unsafe def mapMonoMImp [Monad m] (as : Array α) (f : α → m α) : m (Array α) :=
   go 0 as

src/Init/Data/Array/DecidableEq.lean

@@ -21,8 +21,6 @@ theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size)
     subst heq
     exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)
 termination_by a.size - i
-decreasing_by decreasing_trivial_pre_omega
-
 
 theorem eq_of_isEqv [DecidableEq α] (a b : Array α) : Array.isEqv a b (fun x y => x = y) → a = b := by
   simp [Array.isEqv]
@@ -39,7 +37,6 @@ theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux
   case inl h => simp [h, isEqvAux_self a (i+1)]
   case inr h => simp [h]
 termination_by a.size - i
-decreasing_by decreasing_trivial_pre_omega
 
 theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (fun x y => x = y) = true := by
   simp [isEqv, isEqvAux_self]

src/Init/Data/Array/Lemmas.lean

@@ -131,7 +131,6 @@ where
       simp [aux (i+1), map_eq_pure_bind]; rfl
     · rw [List.drop_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
   termination_by arr.size - i
-  decreasing_by decreasing_trivial_pre_omega
 
 @[simp] theorem map_data (f : α → β) (arr : Array α) : (arr.map f).data = arr.data.map f := by
   rw [map, mapM_eq_foldlM]

src/Init/Data/Array/Mem.lean

@@ -27,20 +27,13 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a <
   cases as with | _ as =>
   exact Nat.lt_trans (List.sizeOf_get ..) (by simp_arith)
 
-@[simp] theorem sizeOf_getElem [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) :
-  sizeOf (as[i]'h) < sizeOf as := sizeOf_get _ _
-
 /-- This tactic, added to the `decreasing_trivial` toolbox, proves that
 `sizeOf arr[i] < sizeOf arr`, which is useful for well founded recursions
 over a nested inductive like `inductive T | mk : Array T → T`. -/
 macro "array_get_dec" : tactic =>
   `(tactic| first
-    -- subsumed by simp
-    -- | with_reducible apply sizeOf_get
-    -- | with_reducible apply sizeOf_getElem
-    | (with_reducible apply Nat.lt_trans (sizeOf_get ..)); simp_arith
-    | (with_reducible apply Nat.lt_trans (sizeOf_getElem ..)); simp_arith
-    )
+    | apply sizeOf_get
+    | apply Nat.lt_trans (sizeOf_get ..); simp_arith)
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_get_dec)
 
@@ -50,10 +43,9 @@ provided that `a ∈ arr` which is useful for well founded recursions over a nes
 -- NB: This is analogue to tactic `sizeOf_list_dec`
 macro "array_mem_dec" : tactic =>
   `(tactic| first
-    | with_reducible apply Array.sizeOf_lt_of_mem; assumption; done
-    | with_reducible
-        apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h)
-        case' h => assumption
+    | apply Array.sizeOf_lt_of_mem; assumption; done
+    | apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h)
+      case' h => assumption
       simp_arith)
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_mem_dec)

src/Init/Data/Array/QSort.lean

@@ -27,7 +27,6 @@ def qpartition (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat ×
       let as := as.swap! i hi
       (i, as)
     termination_by hi - j
-    decreasing_by all_goals simp_wf; decreasing_trivial_pre_omega
   loop as lo lo
 
 @[inline] partial def qsort (as : Array α) (lt : α → α → Bool) (low := 0) (high := as.size - 1) : Array α :=

src/Init/Data/Fin/Fold.lean

@@ -12,7 +12,6 @@ import Init.Data.Nat.Linear
   loop (x : α) (i : Nat) : α :=
     if h : i < n then loop (f x ⟨i, h⟩) (i+1) else x
   termination_by n - i
-  decreasing_by decreasing_trivial_pre_omega
 
 /-- Folds over `Fin n` from the right: `foldr 3 f x = f 0 (f 1 (f 2 x))`. -/
 @[inline] def foldr (n) (f : Fin n → α → α) (init : α) : α := loop ⟨n, Nat.le_refl n⟩ init where

src/Init/Data/Fin/Iterate.lean

@@ -23,7 +23,6 @@ def hIterateFrom (P : Nat → Sort _) {n} (f : ∀(i : Fin n), P i.val → P (i.
     have p : i = n := (or_iff_left g).mp (Nat.eq_or_lt_of_le ubnd)
     _root_.cast (congrArg P p) a
   termination_by n - i
-  decreasing_by decreasing_trivial_pre_omega
 
 /--
 `hIterate` is a heterogenous iterative operation that applies a

src/Init/Data/Fin/Lemmas.lean

@@ -602,7 +602,6 @@ A version of `Fin.succRec` taking `i : Fin n` as the first argument. -/
     @Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ) := by
   cases i; rfl
 
-
 /-- Define `motive i` by induction on `i : Fin (n + 1)` via induction on the underlying `Nat` value.
 This function has two arguments: `zero` handles the base case on `motive 0`,
 and `succ` defines the inductive step using `motive i.castSucc`.
@@ -611,12 +610,8 @@ and `succ` defines the inductive step using `motive i.castSucc`.
 @[elab_as_elim] def induction {motive : Fin (n + 1) → Sort _} (zero : motive 0)
     (succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
     ∀ i : Fin (n + 1), motive i
-  | ⟨i, hi⟩ => go i hi
-where
-  -- Use a curried function so that this is structurally recursive
-  go : ∀ (i : Nat) (hi : i < n + 1), motive ⟨i, hi⟩
-  | 0, hi => by rwa [Fin.mk_zero]
-  | i+1, hi => succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ (go i (Nat.lt_of_succ_lt hi))
+  | ⟨0, hi⟩ => by rwa [Fin.mk_zero]
+  | ⟨i+1, hi⟩ => succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ (induction zero succ ⟨i, Nat.lt_of_succ_lt hi⟩)
 
 @[simp] theorem induction_zero {motive : Fin (n + 1) → Sort _} (zero : motive 0)
     (hs : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :

src/Init/Data/List/BasicAux.lean

@@ -226,10 +226,9 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a <
 over a nested inductive like `inductive T | mk : List T → T`. -/
 macro "sizeOf_list_dec" : tactic =>
   `(tactic| first
-    | with_reducible apply sizeOf_lt_of_mem; assumption; done
-    | with_reducible
-        apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
-        case' h => assumption
+    | apply sizeOf_lt_of_mem; assumption; done
+    | apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
+      case' h => assumption
       simp_arith)
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| sizeOf_list_dec)

src/Init/Data/String/Extra.lean

@@ -132,17 +132,13 @@ theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext)
   cases i; rename_i s pos; simp [Iterator.next, Iterator.sizeOf_eq]; simp [Iterator.hasNext] at h
   exact Nat.sub_lt_sub_left h (String.lt_next s pos)
 
-macro_rules
-| `(tactic| decreasing_trivial) =>
-  `(tactic| with_reducible apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
+macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
 
 theorem Iterator.sizeOf_next_lt_of_atEnd (i : String.Iterator) (h : ¬ i.atEnd = true) : sizeOf i.next < sizeOf i :=
   have h : i.hasNext := decide_eq_true <| Nat.gt_of_not_le <| mt decide_eq_true h
   sizeOf_next_lt_of_hasNext i h
 
-macro_rules
-| `(tactic| decreasing_trivial) =>
-  `(tactic| with_reducible apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)
+macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)
 
 namespace Iterator
 

src/Init/Meta.lean

@@ -1057,7 +1057,6 @@ where
     else
       Syntax.mkCApp (Name.mkStr2 "Array" ("mkArray" ++ toString xs.size)) args
   termination_by xs.size - i
-  decreasing_by decreasing_trivial_pre_omega
 
 instance [Quote α `term] : Quote (Array α) `term where
   quote := quoteArray

src/Init/Notation.lean

@@ -296,7 +296,7 @@ macro_rules | `($x - $y)   => `(binop% HSub.hSub $x $y)
 macro_rules | `($x * $y)   => `(binop% HMul.hMul $x $y)
 macro_rules | `($x / $y)   => `(binop% HDiv.hDiv $x $y)
 macro_rules | `($x % $y)   => `(binop% HMod.hMod $x $y)
--- exponentiation should be considered a right action (#2854)
+-- exponentiation should be considered a right action (#2220)
 macro_rules | `($x ^ $y)   => `(rightact% HPow.hPow $x $y)
 macro_rules | `($x ++ $y)  => `(binop% HAppend.hAppend $x $y)
 macro_rules | `(- $x)      => `(unop% Neg.neg $x)

src/Init/WFTactics.lean

@@ -25,16 +25,9 @@ syntax "decreasing_trivial" : tactic
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp (config := { arith := true, failIfUnchanged := false })) <;> done)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| omega)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| assumption)
-
-/--
-Variant of `decreasing_trivial` that does not use `omega`, intended to be used in core modules
-before `omega` is available.
--/
-syntax "decreasing_trivial_pre_omega" : tactic
-macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
-macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i
-macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt; assumption)  -- i-1 < i if i ≠ 0
-
+macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
+macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i
+macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt; assumption)  -- i-1 < i if i ≠ 0
 
 /-- Constructs a proof of decreasing along a well founded relation, by applying
 lexicographic order lemmas and using `ts` to solve the base case. If it fails,

src/Lean/Compiler/ExternAttr.lean

@@ -66,13 +66,12 @@ builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
     descr := "builtin and foreign functions"
     getParam := fun _ stx => syntaxToExternAttrData stx
     afterSet := fun declName _ => do
-      let env ← getEnv
-      if env.isProjectionFn declName || env.isConstructor declName then
-        if let some (.thmInfo ..) := env.find? declName then
-          -- We should not mark theorems as extern
-          return ()
-        let env ← ofExcept <| addExtern env declName
+      let mut env ← getEnv
+      if env.isProjectionFn declName || env.isConstructor declName then do
+        env ← ofExcept <| addExtern env declName
         setEnv env
+      else
+        pure ()
   }
 
 @[export lean_get_extern_attr_data]
@@ -156,7 +155,7 @@ private def getExternConstArity (declName : Name) : CoreM Nat := do
 @[export lean_get_extern_const_arity]
 def getExternConstArityExport (env : Environment) (declName : Name) : IO (Option Nat) := do
   try
-    let (arity, _) ← (getExternConstArity declName).toIO { fileName := "<compiler>", fileMap := default, diag := false } { env := env }
+    let (arity, _) ← (getExternConstArity declName).toIO { fileName := "<compiler>", fileMap := default } { env := env }
     return some arity
   catch
    | IO.Error.userError _   => return none

src/Lean/Compiler/IR/RC.lean

@@ -9,10 +9,9 @@ import Lean.Compiler.IR.CompilerM
 import Lean.Compiler.IR.LiveVars
 
 namespace Lean.IR.ExplicitRC
-/-!
-Insert explicit RC instructions. So, it assumes the input code does not contain `inc` nor `dec` instructions.
-This transformation is applied before lower level optimizations
-that introduce the instructions `release` and `set`
+/-! Insert explicit RC instructions. So, it assumes the input code does not contain `inc` nor `dec` instructions.
+   This transformation is applied before lower level optimizations
+   that introduce the instructions `release` and `set`
 -/
 
 structure VarInfo where

src/Lean/Compiler/IR/ResetReuse.lean

@@ -9,24 +9,21 @@ import Lean.Compiler.IR.LiveVars
 import Lean.Compiler.IR.Format
 
 namespace Lean.IR.ResetReuse
-/-!
-Remark: the insertResetReuse transformation is applied before we have
-inserted `inc/dec` instructions, and performed lower level optimizations
-that introduce the instructions `release` and `set`.
--/
+/-! Remark: the insertResetReuse transformation is applied before we have
+   inserted `inc/dec` instructions, and performed lower level optimizations
+   that introduce the instructions `release` and `set`. -/
 
-/-!
-Remark: the functions `S`, `D` and `R` defined here implement the
-corresponding functions in the paper "Counting Immutable Beans"
+/-! Remark: the functions `S`, `D` and `R` defined here implement the
+  corresponding functions in the paper "Counting Immutable Beans"
 
-Here are the main differences:
-- We use the State monad to manage the generation of fresh variable names.
-- Support for join points, and `uset` and `sset` instructions for unboxed data.
-- `D` uses the auxiliary function `Dmain`.
-- `Dmain` returns a pair `(b, found)` to avoid quadratic behavior when checking
-  the last occurrence of the variable `x`.
-- Because we have join points in the actual implementation, a variable may be live even if it
-  does not occur in a function body. See example at `livevars.lean`.
+  Here are the main differences:
+  - We use the State monad to manage the generation of fresh variable names.
+  - Support for join points, and `uset` and `sset` instructions for unboxed data.
+  - `D` uses the auxiliary function `Dmain`.
+  - `Dmain` returns a pair `(b, found)` to avoid quadratic behavior when checking
+    the last occurrence of the variable `x`.
+  - Because we have join points in the actual implementation, a variable may be live even if it
+    does not occur in a function body. See example at `livevars.lean`.
 -/
 
 private def mayReuse (c₁ c₂ : CtorInfo) : Bool :=
@@ -36,68 +33,39 @@ private def mayReuse (c₁ c₂ : CtorInfo) : Bool :=
      because it produces counterintuitive behavior. -/
   c₁.name.getPrefix == c₂.name.getPrefix
 
-/--
-Replace `ctor` applications with `reuse` applications if compatible.
-`w` contains the "memory cell" being reused.
--/
 private partial def S (w : VarId) (c : CtorInfo) : FnBody → FnBody
-  | .vdecl x t v@(.ctor c' ys) b   =>
+  | FnBody.vdecl x t v@(Expr.ctor c' ys) b   =>
     if mayReuse c c' then
       let updtCidx := c.cidx != c'.cidx
-      .vdecl x t (.reuse w c' updtCidx ys) b
+      FnBody.vdecl x t (Expr.reuse w c' updtCidx ys) b
     else
-      .vdecl x t v (S w c b)
-  | .jdecl j ys v b   =>
+      FnBody.vdecl x t v (S w c b)
+  | FnBody.jdecl j ys v b   =>
     let v' := S w c v
-    if v == v' then
-      .jdecl j ys v (S w c b)
-    else
-      .jdecl j ys v' b
-  | .case tid x xType alts =>
-    .case tid x xType <| alts.map fun alt => alt.modifyBody (S w c)
+    if v == v' then FnBody.jdecl j ys v (S w c b)
+    else FnBody.jdecl j ys v' b
+  | FnBody.case tid x xType alts    => FnBody.case tid x xType <| alts.map fun alt => alt.modifyBody (S w c)
   | b =>
-    if b.isTerminal then
-      b
+    if b.isTerminal then b
     else let
       (instr, b) := b.split
       instr.setBody (S w c b)
 
-structure Context where
-  lctx      : LocalContext := {}
-  /--
-  Contains all variables in `cases` statements in the current path.
-  We use this information to prevent double-reset in code such as
-  ```
-  case x_i : obj of
-  Prod.mk →
-    case x_i : obj of
-    Prod.mk →
-    ...
-  ```
-  -/
-  casesVars : PHashSet VarId := {}
-
 /-- We use `Context` to track join points in scope. -/
-abbrev M := ReaderT Context (StateT Index Id)
+abbrev M := ReaderT LocalContext (StateT Index Id)
 
 private def mkFresh : M VarId := do
-  let idx ← getModify fun n => n + 1
-  return { idx := idx }
+  let idx ← getModify (fun n => n + 1)
+  pure { idx := idx }
 
-/--
-Helper function for applying `S`. We only introduce a `reset` if we managed
-to replace a `ctor` withe `reuse` in `b`.
--/
 private def tryS (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody := do
   let w ← mkFresh
   let b' := S w c b
-  if b == b' then
-    return b
-  else
-    return .vdecl w IRType.object (.reset c.size x) b'
+  if b == b' then pure b
+  else pure $ FnBody.vdecl w IRType.object (Expr.reset c.size x) b'
 
 private def Dfinalize (x : VarId) (c : CtorInfo) : FnBody × Bool → M FnBody
-  | (b, true)  => return b
+  | (b, true)  => pure b
   | (b, false) => tryS x c b
 
 private def argsContainsVar (ys : Array Arg) (x : VarId) : Bool :=
@@ -107,85 +75,75 @@ private def argsContainsVar (ys : Array Arg) (x : VarId) : Bool :=
 
 private def isCtorUsing (b : FnBody) (x : VarId) : Bool :=
   match b with
-  | .vdecl _ _ (.ctor _ ys) _ => argsContainsVar ys x
+  | (FnBody.vdecl _ _ (Expr.ctor _ ys) _) => argsContainsVar ys x
   | _ => false
 
-/--
-Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`,
-and `flag == true` if `x` is live in `b`.
+/-- Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`,
+   and `flag == true` if `x` is live in `b`.
 
-Note that, in the function `D` defined in the paper, for each `let x := e; F`,
-`D` checks whether `x` is live in `F` or not. This is great for clarity but it
-is expensive: `O(n^2)` where `n` is the size of the function body. -/
-private partial def Dmain (x : VarId) (c : CtorInfo) (e : FnBody) : M (FnBody × Bool) := do
-  match e with
-  | .case tid y yType alts =>
-    if e.hasLiveVar (← read).lctx x then
+   Note that, in the function `D` defined in the paper, for each `let x := e; F`,
+   `D` checks whether `x` is live in `F` or not. This is great for clarity but it
+   is expensive: `O(n^2)` where `n` is the size of the function body. -/
+private partial def Dmain (x : VarId) (c : CtorInfo) : FnBody → M (FnBody × Bool)
+  | e@(FnBody.case tid y yType alts) => do
+    let ctx ← read
+    if e.hasLiveVar ctx x then do
       /- If `x` is live in `e`, we recursively process each branch. -/
       let alts ← alts.mapM fun alt => alt.mmodifyBody fun b => Dmain x c b >>= Dfinalize x c
-      return (.case tid y yType alts, true)
-    else
-      return (e, false)
-  | .jdecl j ys v b =>
-    let (b, found) ← withReader (fun ctx => { ctx with lctx := ctx.lctx.addJP j ys v }) (Dmain x c b)
+      pure (FnBody.case tid y yType alts, true)
+    else pure (e, false)
+  | FnBody.jdecl j ys v b   => do
+    let (b, found) ← withReader (fun ctx => ctx.addJP j ys v) (Dmain x c b)
     let (v, _ /- found' -/) ← Dmain x c v
     /- If `found' == true`, then `Dmain b` must also have returned `(b, true)` since
        we assume the IR does not have dead join points. So, if `x` is live in `j` (i.e., `v`),
        then it must also live in `b` since `j` is reachable from `b` with a `jmp`.
        On the other hand, `x` may be live in `b` but dead in `j` (i.e., `v`). -/
-    return (.jdecl j ys v b, found)
-  | e =>
+    pure (FnBody.jdecl j ys v b, found)
+  | e => do
+    let ctx ← read
     if e.isTerminal then
-      return (e, e.hasLiveVar (← read).lctx x)
+      pure (e, e.hasLiveVar ctx x)
     else do
       let (instr, b) := e.split
       if isCtorUsing instr x then
         /- If the scrutinee `x` (the one that is providing memory) is being
            stored in a constructor, then reuse will probably not be able to reuse memory at runtime.
            It may work only if the new cell is consumed, but we ignore this case. -/
-        return (e, true)
+        pure (e, true)
       else
         let (b, found) ← Dmain x c b
         /- Remark: it is fine to use `hasFreeVar` instead of `hasLiveVar`
-           since `instr` is not a `FnBody.jmp` (it is not a terminal) nor
-           it is a `FnBody.jdecl`. -/
+           since `instr` is not a `FnBody.jmp` (it is not a terminal) nor it is a `FnBody.jdecl`. -/
         if found || !instr.hasFreeVar x then
-          return (instr.setBody b, found)
+          pure (instr.setBody b, found)
         else
           let b ← tryS x c b
-          return (instr.setBody b, true)
+          pure (instr.setBody b, true)
 
 private def D (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody :=
   Dmain x c b >>= Dfinalize x c
 
-partial def R (e : FnBody) : M FnBody := do
-  match e with
-  | .case tid x xType alts =>
-    let alreadyFound := (← read).casesVars.contains x
-    withReader (fun ctx => { ctx with casesVars := ctx.casesVars.insert x }) do
+partial def R : FnBody → M FnBody
+  | FnBody.case tid x xType alts   => do
       let alts ← alts.mapM fun alt => do
         let alt ← alt.mmodifyBody R
         match alt with
-        | .ctor c b =>
-          if c.isScalar || alreadyFound then
-            -- If `alreadyFound`, then we don't try to reuse memory cell to avoid
-            -- double reset.
-            return alt
-          else
-            .ctor c <$> D x c b
-        | _ => return alt
-      return .case tid x xType alts
-  | .jdecl j ys v b =>
+        | Alt.ctor c b =>
+          if c.isScalar then pure alt
+          else Alt.ctor c <$> D x c b
+        | _            => pure alt
+      pure $ FnBody.case tid x xType alts
+  | FnBody.jdecl j ys v b   => do
     let v ← R v
-    let b ← withReader (fun ctx => { ctx with lctx := ctx.lctx.addJP j ys v }) (R b)
-    return .jdecl j ys v b
-  | e =>
-    if e.isTerminal then
-      return e
-    else
+    let b ← withReader (fun ctx => ctx.addJP j ys v) (R b)
+    pure $ FnBody.jdecl j ys v b
+  | e => do
+    if e.isTerminal then pure e
+    else do
       let (instr, b) := e.split
       let b ← R b
-      return instr.setBody b
+      pure (instr.setBody b)
 
 end ResetReuse
 
@@ -193,7 +151,7 @@ open ResetReuse
 
 def Decl.insertResetReuse (d : Decl) : Decl :=
   match d with
-  | .fdecl (body := b) .. =>
+  | .fdecl (body := b) ..=>
     let nextIndex := d.maxIndex + 1
     let bNew      := (R b {}).run' nextIndex
     d.updateBody! bNew

src/Lean/CoreM.lean

@@ -13,25 +13,13 @@ import Lean.Elab.InfoTree.Types
 import Lean.MonadEnv
 
 namespace Lean
-register_builtin_option diagnostics : Bool := {
-  defValue := false
-  group    := "diagnostics"
-  descr    := "collect diagnostic information"
-}
-
-register_builtin_option diagnostics.threshold : Nat := {
-  defValue := 20
-  group    := "diagnostics"
-  descr    := "only diagnostic counters above this threshold are reported by the definitional equality"
-}
+namespace Core
 
 register_builtin_option maxHeartbeats : Nat := {
   defValue := 200000
   descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
 }
 
-namespace Core
-
 builtin_initialize registerTraceClass `Kernel
 
 def getMaxHeartbeats (opts : Options) : Nat :=
@@ -84,11 +72,6 @@ structure Context where
   Recall that runtime exceptions are `maxRecDepth` or `maxHeartbeats`.
   -/
   catchRuntimeEx : Bool := false
-  /--
-  If `diag := true`, different parts of the system collect diagnostics.
-  Use the `set_option diag true` to set it to true.
-  -/
-  diag           : Bool := false
   deriving Nonempty
 
 /-- CoreM is a monad for manipulating the Lean environment.
@@ -223,7 +206,7 @@ def mkFreshUserName (n : Name) : CoreM Name :=
 instance [MetaEval α] : MetaEval (CoreM α) where
   eval env opts x _ := do
     let x : CoreM α := do try x finally printTraces
-    let (a, s) ← x.toIO { maxRecDepth := maxRecDepth.get opts, options := opts, fileName := "<CoreM>", fileMap := default, diag := diagnostics.get opts } { env := env }
+    let (a, s) ← x.toIO { maxRecDepth := maxRecDepth.get opts, options := opts, fileName := "<CoreM>", fileMap := default } { env := env }
     MetaEval.eval s.env opts a (hideUnit := true)
 
 -- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`
@@ -389,17 +372,9 @@ def addAndCompile (decl : Declaration) : CoreM Unit := do
   addDecl decl;
   compileDecl decl
 
-def getDiag (opts : Options) : Bool :=
-  diagnostics.get opts
-
-/-- Return `true` if diagnostic information collection is enabled. -/
-def isDiagnosticsEnabled : CoreM Bool :=
-  return (← read).diag
-
 def ImportM.runCoreM (x : CoreM α) : ImportM α := do
   let ctx ← read
-  let opts := ctx.opts
-  let (a, _) ← x.toIO { options := opts, fileName := "<ImportM>", fileMap := default, diag := getDiag opts } { env := ctx.env }
+  let (a, _) ← x.toIO { options := ctx.opts, fileName := "<ImportM>", fileMap := default } { env := ctx.env }
   return a
 
 /-- Return `true` if the exception was generated by one our resource limits. -/

src/Lean/Data/HashMap.lean

@@ -92,7 +92,6 @@ def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (targ
      moveEntries (i+1) source target
   else target
 termination_by source.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
   let bucketsNew : HashMapBucket α β := ⟨

src/Lean/Data/HashSet.lean

@@ -84,7 +84,6 @@ def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (target : Has
   else
     target
 termination_by source.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
   let bucketsNew : HashSetBucket α := ⟨

src/Lean/Elab/BuiltinNotation.lean

@@ -409,8 +409,6 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
          let h ← elabTerm hStx none
          let hType ← inferType h
          let hTypeAbst ← kabstract hType lhs
-         unless hTypeAbst.hasLooseBVars do
-           throwError "invalid `▸` notation, the equality{indentExpr heq}\nhas type {indentExpr heqType}\nbut its left hand side is not mentioned in the type{indentExpr hType}"
          let motive ← mkMotive lhs hTypeAbst
          unless (← isTypeCorrect motive) do
            throwError "invalid `▸` notation, failed to compute motive for the substitution"

src/Lean/Elab/BuiltinTerm.lean

@@ -313,7 +313,7 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
 
 @[builtin_term_elab «set_option»] def elabSetOption : TermElab := fun stx expectedType? => do
   let options ← Elab.elabSetOption stx[1] stx[3]
-  withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options, diag := getDiag options }) do
+  withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
     elabTerm stx[5] expectedType?
 
 @[builtin_term_elab withAnnotateTerm] def elabWithAnnotateTerm : TermElab := fun stx expectedType? => do

src/Lean/Elab/Command.lean

@@ -138,8 +138,7 @@ private def mkCoreContext (ctx : Context) (s : State) (heartbeats : Nat) : Core.
     currNamespace  := scope.currNamespace
     openDecls      := scope.openDecls
     initHeartbeats := heartbeats
-    currMacroScope := ctx.currMacroScope
-    diag           := getDiag scope.opts }
+    currMacroScope := ctx.currMacroScope }
 
 private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog := Id.run do
   if traceState.traces.isEmpty then return log
@@ -412,7 +411,7 @@ def liftTermElabM (x : TermElabM α) : CommandElabM α := do
   -- make sure `observing` below also catches runtime exceptions (like we do by default in
   -- `CommandElabM`)
   let _ := MonadAlwaysExcept.except (m := TermElabM)
-  let x : MetaM _      := (observing (try x finally Meta.reportDiag)).run (mkTermContext ctx s) { levelNames := scope.levelNames }
+  let x : MetaM _      := (observing x).run (mkTermContext ctx s) { levelNames := scope.levelNames }
   let x : CoreM _      := x.run mkMetaContext {}
   let x : EIO _ _      := x.run (mkCoreContext ctx s heartbeats) { env := s.env, ngen := s.ngen, nextMacroScope := s.nextMacroScope, infoState.enabled := s.infoState.enabled, traceState := s.traceState }
   let (((ea, _), _), coreS) ← liftEIO x

src/Lean/Elab/Extra.lean

@@ -96,7 +96,7 @@ Here are brief descriptions of each of the operator types:
 - `rightact% f a b` elaborates `f a b` as a right action (the `b` operand "acts upon" the `a` operand).
   Only `a` participates in the protocol since `b` can have an unrelated type.
   This is used by `HPow` since, for example, there are both `Real -> Nat -> Real` and `Real -> Real -> Real`
-  exponentiation functions, and we prefer the former in the case of `x ^ 2`, but `binop%` would choose the latter. (#2854)
+  exponentiation functions, and we prefer the former in the case of `x ^ 2`, but `binop%` would choose the latter. (#2220)
 - There are also `binrel%` and `binrel_no_prop%` (see the docstring for `elabBinRelCore`).
 
 The elaborator works as follows:
@@ -449,7 +449,7 @@ def elabOp : TermElab := fun stx expectedType? => do
 
   - `binrel% R x y` elaborates `R x y` using the `binop%/...` expression trees in both `x` and `y`.
     It is similar to how `binop% R x y` elaborates but with a significant difference:
-    it does not use the expected type when computing the types of the operands.
+    it does not use the expected type when computing the types of the operads.
   - `binrel_no_prop% R x y` elaborates `R x y` like `binrel% R x y`, but if the resulting type for `x` and `y`
     is `Prop` they are coerced to `Bool`.
     This is used for relations such as `==` which do not support `Prop`, but we still want

src/Lean/Elab/InfoTree/Main.lean

@@ -102,8 +102,7 @@ def ContextInfo.runCoreM (info : ContextInfo) (x : CoreM α) : IO α := do
     have been used in `lctx` and `info.mctx`.
   -/
   (·.1) <$>
-    x.toIO { options := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls
-             fileName := "<InfoTree>", fileMap := default, diag := getDiag info.options }
+    x.toIO { options := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls, fileName := "<InfoTree>", fileMap := default }
            { env := info.env, ngen := info.ngen }
 
 def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do

src/Lean/Elab/StructInst.lean

@@ -821,9 +821,7 @@ partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do
     | some r => reduce structNames r
     | none   => return e.updateProj! (← reduce structNames b)
   | .app f .. =>
-    -- Recall that proposition fields are theorems. Thus, we must set transparency to .all
-    -- to ensure they are unfolded here
-    match (← withTransparency .all <| reduceProjOf? e structNames.contains) with
+    match (← reduceProjOf? e structNames.contains) with
     | some r => reduce structNames r
     | none   =>
       let f := f.getAppFn

src/Lean/Elab/Structure.lean

@@ -704,8 +704,8 @@ private def registerStructure (structName : Name) (infos : Array StructFieldInfo
           subobject? :=
             if info.kind == StructFieldKind.subobject then
               match env.find? info.declName with
-              | some info =>
-                match info.type.getForallBody.getAppFn with
+              | some (ConstantInfo.defnInfo val) =>
+                match val.type.getForallBody.getAppFn with
                 | Expr.const parentName .. => some parentName
                 | _ => panic! "ill-formed structure"
               | _ => panic! "ill-formed environment"

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -163,7 +163,7 @@ private def getOptRotation (stx : Syntax) : Nat :=
 
 @[builtin_tactic Parser.Tactic.set_option] def elabSetOption : Tactic := fun stx => do
   let options ← Elab.elabSetOption stx[1] stx[3]
-  withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options, diag := getDiag options }) do
+  withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
     evalTactic stx[5]
 
 @[builtin_tactic Parser.Tactic.allGoals] def evalAllGoals : Tactic := fun stx => do

src/Lean/Meta/Basic.lean

@@ -266,15 +266,6 @@ structure PostponedEntry where
   ctx? : Option DefEqContext
   deriving Inhabited
 
-structure Diagnostics where
-  /-- Number of times each declaration has been unfolded -/
-  unfoldCounter : PHashMap Name Nat := {}
-  /-- Number of times `f a =?= f b` heuristic has been used per function `f`. -/
-  heuristicCounter : PHashMap Name Nat := {}
-  /-- Number of times a TC instance is used. -/
-  instanceCounter : PHashMap Name Nat := {}
-  deriving Inhabited
-
 /--
   `MetaM` monad state.
 -/
@@ -285,7 +276,6 @@ structure State where
   zetaDeltaFVarIds : FVarIdSet := {}
   /-- Array of postponed universe level constraints -/
   postponed        : PersistentArray PostponedEntry := {}
-  diag             : Diagnostics := {}
   deriving Inhabited
 
 /--
@@ -323,12 +313,6 @@ structure Context where
   progress processing universe constraints.
   -/
   univApprox        : Bool := false
-  /--
-  `inTypeClassResolution := true` when `isDefEq` is invoked at `tryResolve` in the type class
-   resolution module. We don't use `isDefEqProjDelta` when performing TC resolution due to performance issues.
-   This is not a great solution, but a proper solution would require a more sophisticased caching mechanism.
-  -/
-  inTypeClassResolution : Bool := false
 
 /--
 The `MetaM` monad is a core component of Lean's metaprogramming framework, facilitating the
@@ -450,7 +434,7 @@ section Methods
 variable [MonadControlT MetaM n] [Monad n]
 
 @[inline] def modifyCache (f : Cache → Cache) : MetaM Unit :=
-  modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache := f cache, zetaDeltaFVarIds, postponed, diag }
+  modify fun { mctx, cache, zetaDeltaFVarIds, postponed } => { mctx, cache := f cache, zetaDeltaFVarIds, postponed }
 
 @[inline] def modifyInferTypeCache (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
   modifyCache fun ⟨ic, c1, c2, c3, c4, c5, c6⟩ => ⟨f ic, c1, c2, c3, c4, c5, c6⟩
@@ -464,70 +448,6 @@ variable [MonadControlT MetaM n] [Monad n]
 @[inline] def resetDefEqPermCaches : MetaM Unit :=
   modifyDefEqPermCache fun _ => {}
 
-@[inline] def modifyDiag (f : Diagnostics → Diagnostics) : MetaM Unit := do
-  if (← isDiagnosticsEnabled) then
-    modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache, zetaDeltaFVarIds, postponed, diag := f diag }
-
-/-- If diagnostics are enabled, record that `declName` has been unfolded. -/
-def recordUnfold (declName : Name) : MetaM Unit := do
-  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter } =>
-    let newC := if let some c := unfoldCounter.find? declName then c + 1 else 1
-    { unfoldCounter := unfoldCounter.insert declName newC, heuristicCounter, instanceCounter }
-
-/-- If diagnostics are enabled, record that heuristic for solving `f a =?= f b` has been used. -/
-def recordDefEqHeuristic (declName : Name) : MetaM Unit := do
-  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter } =>
-    let newC := if let some c := heuristicCounter.find? declName then c + 1 else 1
-    { unfoldCounter, heuristicCounter := heuristicCounter.insert declName newC, instanceCounter }
-
-/-- If diagnostics are enabled, record that instance `declName` was used during TC resolution. -/
-def recordInstance (declName : Name) : MetaM Unit := do
-  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter } =>
-    let newC := if let some c := instanceCounter.find? declName then c + 1 else 1
-    { unfoldCounter, heuristicCounter, instanceCounter := instanceCounter.insert declName newC }
-
-def collectAboveThreshold (counters : PHashMap Name Nat) (threshold : Nat) : Array (Name × Nat) := Id.run do
-  let mut r := #[]
-  for (declName, counter) in counters do
-    if counter > threshold then
-      r := r.push (declName, counter)
-  return r.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then d₁.lt d₂ else c₁ > c₂
-
-def mkMessageBodyFor? (counters : PHashMap Name Nat) (threshold : Nat) : Option MessageData := Id.run do
-  let entries := collectAboveThreshold counters threshold
-  if entries.isEmpty then
-    return none
-  else
-    let mut m := MessageData.nil
-    for (declName, counter) in entries do
-      if m matches .nil then
-        m := m!"{declName} ↦ {counter}"
-      else
-        m := m ++ m!"\n{declName} ↦ {counter}"
-    return some m
-
-def appendOptMessageData (m : MessageData) (header : String) (m? : Option MessageData) : MessageData :=
-  if let some m' := m? then
-    if m matches .nil then
-      header ++ indentD m'
-    else
-      m ++ "\n" ++ header ++ indentD m'
-  else
-    m
-
-def reportDiag : MetaM Unit := do
-  if (← isDiagnosticsEnabled) then
-    let threshold := diagnostics.threshold.get (← getOptions)
-    let unfold? := mkMessageBodyFor? (← get).diag.unfoldCounter threshold
-    let heu?    := mkMessageBodyFor? (← get).diag.heuristicCounter threshold
-    let inst?   := mkMessageBodyFor? (← get).diag.instanceCounter threshold
-    if unfold?.isSome || heu?.isSome || inst?.isSome then
-      let m := appendOptMessageData MessageData.nil "unfolded declarations:" unfold?
-      let m := appendOptMessageData m "used instances:" inst?
-      let m := appendOptMessageData m "`isDefEq` heuristic:" heu?
-      let m := m ++ "\nuse `set_option diag.threshold <num>` to control threshold for reporting counters"
-      logInfo m
-
 def getLocalInstances : MetaM LocalInstances :=
   return (← read).localInstances
 

src/Lean/Meta/ExprDefEq.lean

@@ -10,18 +10,6 @@ import Lean.Util.OccursCheck
 
 namespace Lean.Meta
 
-register_builtin_option backward.isDefEq.lazyProjDelta : Bool := {
-  defValue := true
-  group    := "backward compatibility"
-  descr    := "use lazy delta reduction when solving unification constrains of the form `(f a).i =?= (g b).i`"
-}
-
-register_builtin_option backward.isDefEq.lazyWhnfCore : Bool := {
-  defValue := true
-  group    := "backward compatibility"
-  descr    := "specifies transparency mode when normalizing constraints of the form `(f a).i =?= s`, if `true` only reducible definitions and instances are unfolded when reducing `f a`. Otherwise, the default setting is used"
-}
-
 /--
   Return `true` if `e` is of the form `fun (x_1 ... x_n) => ?m y_1 ... y_k)`, and `?m` is unassigned.
   Remark: `n`, `k` may be 0.
@@ -1251,7 +1239,6 @@ private def tryHeuristic (t s : Expr) : MetaM Bool := do
     unless t.hasExprMVar || s.hasExprMVar do
       return false
   withTraceNodeBefore `Meta.isDefEq.delta (return m!"{t} =?= {s}") do
-    recordDefEqHeuristic tFn.constName!
     /-
       We process arguments before universe levels to reduce a source of brittleness in the TC procedure.
 
@@ -1772,7 +1759,7 @@ private def isDefEqDeltaStep (t s : Expr) : MetaM DeltaStepResult := do
     | .eq =>
       -- Remark: if `t` and `s` are both some `f`-application, we use `tryHeuristic`
       -- if `f` is not a projection. The projection case generates a performance regression.
-      if tInfo.name == sInfo.name then
+      if tInfo.name == sInfo.name && !(← isProjectionFn tInfo.name) then
         if t.isApp && s.isApp && (← tryHeuristic t s) then
           return .eq
         else
@@ -1816,13 +1803,8 @@ where
     | _, _ => Meta.isExprDefEqAux t s
 
 private def isDefEqProj : Expr → Expr → MetaM Bool
-  | .proj m i t, .proj n j s => do
-    if (← read).inTypeClassResolution then
-      -- See comment at `inTypeClassResolution`
-      pure (i == j && m == n) <&&> Meta.isExprDefEqAux t s
-    else if !backward.isDefEq.lazyProjDelta.get (← getOptions) then
-      pure (i == j && m == n) <&&> Meta.isExprDefEqAux t s
-    else if i == j && m == n then
+  | .proj m i t, .proj n j s =>
+    if i == j && m == n then
       isDefEqProjDelta t s i
     else
       return false
@@ -1995,12 +1977,6 @@ private def cacheResult (keyInfo : DefEqCacheKeyInfo) (result : Bool) : MetaM Un
     let key := (← instantiateMVars key.1, ← instantiateMVars key.2)
     modifyDefEqTransientCache fun c => c.update mode key result
 
-private def whnfCoreAtDefEq (e : Expr) : MetaM Expr := do
-  if backward.isDefEq.lazyWhnfCore.get (← getOptions) then
-    whnfCore e (config := { proj := .yesWithDeltaI })
-  else
-    whnfCore e
-
 @[export lean_is_expr_def_eq]
 partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecDepth do
   withTraceNodeBefore `Meta.isDefEq (return m!"{t} =?= {s}") do
@@ -2013,7 +1989,7 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
     we only want to unify negation (and not all other field operations as well).
     Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986
 
-    Note that we use `proj := .yesWithDeltaI` to ensure `whnfAtMostI` is used to reduce the projection structure.
+    Note that ew use `proj := .yesWithDeltaI` to ensure `whnfAtMostI` is used to reduce the projection structure.
     We added this refinement to address a performance issue in code such as
     ```
     let val : Test := bar c1 key
@@ -2042,8 +2018,8 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
     `whnfCore t (config := { proj := .yes })` which more conservative than `.yesWithDeltaI`,
     and it only created performance issues when handling TC unification problems.
   -/
-  let t' ← whnfCoreAtDefEq t
-  let s' ← whnfCoreAtDefEq s
+  let t' ← whnfCore t (config := { proj := .yesWithDeltaI })
+  let s' ← whnfCore s (config := { proj := .yesWithDeltaI })
   if t != t' || s != s' then
     isExprDefEqAuxImpl t' s'
   else

src/Lean/Meta/ExprLens.lean

@@ -21,28 +21,27 @@ section ExprLens
 
 open Lean.SubExpr
 
-variable [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadError M]
+variable {M} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadError M]
 
 /-- Given a constructor index for Expr, runs `g` on the value of that subexpression and replaces it.
 If the subexpression is under a binder it will instantiate and abstract the binder body correctly.
 Mdata is ignored. An index of 3 is interpreted as the type of the expression. An index of 3 will throw since we can't replace types.
 
 See also `Lean.Meta.transform`, `Lean.Meta.traverseChildren`. -/
-private def lensCoord (g : Expr → M Expr) (n : Nat) (e : Expr) : M Expr := do
-  match n, e with
-  | 0, .app f a         => return e.updateApp! (← g f) a
-  | 1, .app f a         => return e.updateApp! f (← g a)
-  | 0, .lam _ y b _     => return e.updateLambdaE! (← g y) b
-  | 1, .lam n y b c     => withLocalDecl n c y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x]
-  | 0, .forallE _ y b _ => return e.updateForallE! (← g y) b
-  | 1, .forallE n y b c => withLocalDecl n c y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x]
-  | 0, .letE _ y a b _  => return e.updateLet! (← g y) a b
-  | 1, .letE _ y a b _  => return e.updateLet! y (← g a) b
-  | 2, .letE n y a b _  => withLetDecl n y a fun x => do mkLetFVars #[x] <|← g <| b.instantiateRev #[x]
-  | 0, .proj _ _ b      => e.updateProj! <$> g b
-  | n, .mdata _ a       => e.updateMData! <$> lensCoord g n a
-  | 3, _                => throwError "Lensing on types is not supported"
-  | c, e                => throwError "Invalid coordinate {c} for {e}"
+private def lensCoord (g : Expr → M Expr) : Nat → Expr → M Expr
+  | 0, e@(Expr.app f a)         => return e.updateApp! (← g f) a
+  | 1, e@(Expr.app f a)         => return e.updateApp! f (← g a)
+  | 0, e@(Expr.lam _ y b _)     => return e.updateLambdaE! (← g y) b
+  | 1,   (Expr.lam n y b c)     => withLocalDecl n c y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x]
+  | 0, e@(Expr.forallE _ y b _) => return e.updateForallE! (← g y) b
+  | 1,   (Expr.forallE n y b c) => withLocalDecl n c y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x]
+  | 0, e@(Expr.letE _ y a b _)  => return e.updateLet! (← g y) a b
+  | 1, e@(Expr.letE _ y a b _)  => return e.updateLet! y (← g a) b
+  | 2,   (Expr.letE n y a b _)  => withLetDecl n y a fun x => do mkLetFVars #[x] <|← g <| b.instantiateRev #[x]
+  | 0, e@(Expr.proj _ _ b)      => e.updateProj! <$> g b
+  | n, e@(Expr.mdata _ a)       => e.updateMData! <$> lensCoord g n a
+  | 3, _                        => throwError "Lensing on types is not supported"
+  | c, e                        => throwError "Invalid coordinate {c} for {e}"
 
 private def lensAux (g : Expr → M Expr) : List Nat → Expr → M Expr
   | [], e => g e
@@ -57,21 +56,20 @@ def replaceSubexpr (replace : (subexpr : Expr) → M Expr) (p : Pos) (root : Exp
 /-- Runs `k` on the given coordinate, including handling binders properly.
 The subexpression value passed to `k` is not instantiated with respect to the
 array of free variables. -/
-private def viewCoordAux (k : Array Expr → Expr → M α) (fvars: Array Expr) (n : Nat) (e : Expr) : M α := do
-  match n, e with
-  | 3, _                => throwError "Internal: Types should be handled by viewAux"
-  | 0, .app f _         => k fvars f
-  | 1, .app _ a         => k fvars a
-  | 0, .lam _ y _ _     => k fvars y
-  | 1, .lam n y b c     => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
-  | 0, .forallE _ y _ _ => k fvars y
-  | 1, .forallE n y b c => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
-  | 0, .letE _ y _ _ _  => k fvars y
-  | 1, .letE _ _ a _ _  => k fvars a
-  | 2, .letE n y a b _  => withLetDecl n (y.instantiateRev fvars) (a.instantiateRev fvars) fun x => k (fvars.push x) b
-  | 0, .proj _ _ b      => k fvars b
-  | n, .mdata _ a       => viewCoordAux k fvars n a
-  | c, e                => throwError "Invalid coordinate {c} for {e}"
+private def viewCoordAux (k : Array Expr → Expr → M α) (fvars: Array Expr) : Nat → Expr → M α
+  | 3, _                      => throwError "Internal: Types should be handled by viewAux"
+  | 0, (Expr.app f _)         => k fvars f
+  | 1, (Expr.app _ a)         => k fvars a
+  | 0, (Expr.lam _ y _ _)     => k fvars y
+  | 1, (Expr.lam n y b c)     => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
+  | 0, (Expr.forallE _ y _ _) => k fvars y
+  | 1, (Expr.forallE n y b c) => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
+  | 0, (Expr.letE _ y _ _ _)  => k fvars y
+  | 1, (Expr.letE _ _ a _ _)  => k fvars a
+  | 2, (Expr.letE n y a b _)  => withLetDecl n (y.instantiateRev fvars) (a.instantiateRev fvars) fun x => k (fvars.push x) b
+  | 0, (Expr.proj _ _ b)      => k fvars b
+  | n, (Expr.mdata _ a)       => viewCoordAux k fvars n a
+  | c, e                      => throwError "Invalid coordinate {c} for {e}"
 
 private def viewAux (k : Array Expr → Expr → M α) (fvars : Array Expr) : List Nat → Expr → M α
   | [],         e => k fvars <| e.instantiateRev fvars
@@ -121,24 +119,24 @@ open Lean.SubExpr
 
 section ViewRaw
 
-variable [Monad M] [MonadError M]
+variable {M} [Monad M] [MonadError M]
 
 /-- Get the raw subexpression without performing any instantiation. -/
-private def viewCoordRaw (e : Expr) (n : Nat) : M Expr := do
-  match e, n with
-  | e,                3 => throwError "Can't viewRaw the type of {e}"
-  | .app f _,         0 => pure f
-  | .app _ a,         1 => pure a
-  | .lam _ y _ _,     0 => pure y
-  | .lam _ _ b _,     1 => pure b
-  | .forallE _ y _ _, 0 => pure y
-  | .forallE _ _ b _, 1 => pure b
-  | .letE _ y _ _ _,  0 => pure y
-  | .letE _ _ a _ _,  1 => pure a
-  | .letE _ _ _ b _,  2 => pure b
-  | .proj _ _ b,      0 => pure b
-  | .mdata _ a,       n => viewCoordRaw a n
-  | e,                c => throwError "Bad coordinate {c} for {e}"
+private def viewCoordRaw: Expr → Nat → M Expr
+  | e                     , 3 => throwError "Can't viewRaw the type of {e}"
+  | (Expr.app f _)        , 0 => pure f
+  | (Expr.app _ a)        , 1 => pure a
+  | (Expr.lam _ y _ _)    , 0 => pure y
+  | (Expr.lam _ _ b _)    , 1 => pure b
+  | (Expr.forallE _ y _ _), 0 => pure y
+  | (Expr.forallE _ _ b _), 1 => pure b
+  | (Expr.letE _ y _ _ _) , 0 => pure y
+  | (Expr.letE _ _ a _ _) , 1 => pure a
+  | (Expr.letE _ _ _ b _) , 2 => pure b
+  | (Expr.proj _ _ b)     , 0 => pure b
+  | (Expr.mdata _ a)      , n => viewCoordRaw a n
+  | e                     , c => throwError "Bad coordinate {c} for {e}"
+
 
 /-- Given a valid `SubExpr`, return the raw current expression without performing any instantiation.
 If the given `SubExpr` has a type subexpression coordinate, then throw an error.
@@ -150,20 +148,21 @@ def viewSubexpr (p : Pos) (root : Expr) : M Expr :=
   p.foldlM viewCoordRaw root
 
 private def viewBindersCoord : Nat → Expr → Option (Name × Expr)
-  | 1, .lam n y _ _     => some (n, y)
-  | 1, .forallE n y _ _ => some (n, y)
-  | 2, .letE n y _ _ _  => some (n, y)
-  | _, _                => none
+  | 1, (Expr.lam n y _ _)     => some (n, y)
+  | 1, (Expr.forallE n y _ _) => some (n, y)
+  | 2, (Expr.letE n y _ _ _)  => some (n, y)
+  | _, _                      => none
 
 /-- `viewBinders p e` returns a list of all of the binders (name, type) above the given position `p` in the root expression `e` -/
 def viewBinders (p : Pos) (root : Expr) : M (Array (Name × Expr)) := do
-  let (acc, _) ← p.foldlM (init := (#[], root)) fun (acc, e) c => do
+  let (acc, _) ← p.foldlM (fun (acc, e) c => do
     let e₂ ← viewCoordRaw e c
     let acc :=
       match viewBindersCoord c e with
       | none => acc
       | some b => acc.push b
     return (acc, e₂)
+  ) (#[], root)
   return acc
 
 /-- Returns the number of binders above a given subexpr position. -/

src/Lean/Meta/LazyDiscrTree.lean

@@ -978,13 +978,12 @@ def createImportedDiscrTree [Monad m] [MonadLog m] [AddMessageContext m] [MonadO
 
 /-- Creates the core context used for initializing a tree using the current context. -/
 private def createTreeCtx (ctx : Core.Context) : Core.Context := {
-    fileName := ctx.fileName
-    fileMap := ctx.fileMap
-    options := ctx.options
-    maxRecDepth := ctx.maxRecDepth
-    maxHeartbeats := 0
-    ref := ctx.ref
-    diag := getDiag ctx.options
+    fileName := ctx.fileName,
+    fileMap := ctx.fileMap,
+    options := ctx.options,
+    maxRecDepth := ctx.maxRecDepth,
+    maxHeartbeats := 0,
+    ref := ctx.ref,
   }
 
 def findImportMatches

src/Lean/Meta/SynthInstance.lean

@@ -25,12 +25,6 @@ register_builtin_option synthInstance.maxSize : Nat := {
   descr := "maximum number of instances used to construct a solution in the type class instance synthesis procedure"
 }
 
-register_builtin_option backward.synthInstance.canonInstances : Bool := {
-  defValue := true
-  group    := "backward compatibility"
-  descr := "use optimization that relies on 'morally canonical' instances during type class resolution"
-}
-
 namespace SynthInstance
 
 def getMaxHeartbeats (opts : Options) : Nat :=
@@ -362,9 +356,6 @@ private def mkLambdaFVars' (xs : Array Expr) (e : Expr) : MetaM Expr :=
   If it succeeds, the result is a new updated metavariable context and a new list of subgoals.
   A subgoal is created for each instance implicit parameter of `inst`. -/
 def tryResolve (mvar : Expr) (inst : Instance) : MetaM (Option (MetavarContext × List Expr)) := do
-  if (← isDiagnosticsEnabled) then
-    if let .const declName _ := inst.val.getAppFn then
-      recordInstance declName
   let mvarType   ← inferType mvar
   let lctx       ← getLCtx
   let localInsts ← getLocalInstances
@@ -425,7 +416,7 @@ private def mkAnswer (cNode : ConsumerNode) : MetaM Answer :=
 def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
   withMCtx cNode.mctx do
   if cNode.size ≥ (← read).maxResultSize then
-    trace[Meta.synthInstance.answer] "{crossEmoji} {← instantiateMVars (← inferType cNode.mvar)}{Format.line}(size: {cNode.size} ≥ {(← read).maxResultSize})"
+      trace[Meta.synthInstance.answer] "{crossEmoji} {← instantiateMVars (← inferType cNode.mvar)}{Format.line}(size: {cNode.size} ≥ {(← read).maxResultSize})"
   else
     withTraceNode `Meta.synthInstance.answer
       (fun _ => return m!"{checkEmoji} {← instantiateMVars (← inferType cNode.mvar)}") do
@@ -558,17 +549,16 @@ def generate : SynthM Unit := do
     let mctx := gNode.mctx
     let mvar := gNode.mvar
     /- See comment at `typeHasMVars` -/
-    if backward.synthInstance.canonInstances.get (← getOptions) then
-      unless gNode.typeHasMVars do
-        if let some entry := (← get).tableEntries.find? key then
-          unless entry.answers.isEmpty do
-            /-
-            We already have an answer for this node, and since its type does not have metavariables,
-            we can skip other solutions because we assume instances are "morally canonical".
-            We have added this optimization to address issue #3996.
-            -/
-            modify fun s => { s with generatorStack := s.generatorStack.pop }
-            return
+    unless gNode.typeHasMVars do
+      if let some entry := (← get).tableEntries.find? key then
+        unless entry.answers.isEmpty do
+          /-
+          We already have an answer for this node, and since its type does not have metavariables,
+          we can skip other solutions because we assume instances are "morally canonical".
+          We have added this optimization to address issue #3996.
+          -/
+          modify fun s => { s with generatorStack := s.generatorStack.pop }
+          return
     discard do withMCtx mctx do
       withTraceNode `Meta.synthInstance
         (return m!"{exceptOptionEmoji ·} apply {inst.val} to {← instantiateMVars (← inferType mvar)}") do
@@ -721,7 +711,6 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
     (return m!"{exceptOptionEmoji ·} {← instantiateMVars type}") do
   withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances,
                                           foApprox := true, ctxApprox := true, constApprox := false, univApprox := false }) do
-  withReader (fun ctx => { ctx with inTypeClassResolution := true }) do
     let localInsts ← getLocalInstances
     let type ← instantiateMVars type
     let type ← preprocess type

src/Lean/Meta/Tactic/LinearArith/Solver.lean

@@ -81,7 +81,6 @@ def Poly.add (e₁ e₂ : Poly) : Poly :=
       else
         { val := r }
     termination_by (e₁.size - i₁, e₂.size - i₂)
-    decreasing_by all_goals decreasing_with decreasing_trivial_pre_omega
   go 0 0 #[]
 
 def Poly.combine (d₁ : Int) (e₁ : Poly) (d₂ : Int) (e₂ : Poly) : Poly :=
@@ -109,7 +108,6 @@ def Poly.combine (d₁ : Int) (e₁ : Poly) (d₂ : Int) (e₂ : Poly) : Poly :=
       else
         { val := r }
     termination_by (e₁.size - i₁, e₂.size - i₂)
-    decreasing_by all_goals decreasing_with decreasing_trivial_pre_omega
   go 0 0 #[]
 
 def Poly.eval? (e : Poly) (a : Assignment) : Option Rat := Id.run do

src/Lean/Meta/WHNF.lean

@@ -344,7 +344,7 @@ inductive ProjReductionKind where
   | yesWithDelta
   /--
   Projections `s.i` are reduced at `whnfCore`, and `whnfAtMostI` is used at `s` during the process.
-  Recall that `whnfAtMostI` is like `whnf` but uses transparency at most `instances`.
+  Recall that `whnfAtMostII` is like `whnf` but uses transparency at most `instances`.
   This option is stronger than `yes`, but weaker than `yesWithDelta`.
   We use this option to ensure we reduce projections to prevent expensive defeq checks when unifying TC operations.
   When unifying e.g. `(@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1`,
@@ -608,11 +608,10 @@ where
           | .notMatcher   =>
             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)
+              | .recInfo rec    => reduceRec rec lvls e.getAppArgs (fun _ => return e) go
+              | .quotInfo rec   => reduceQuotRec rec e.getAppArgs (fun _ => return e) go
               | c@(.defnInfo _) => do
                 if (← isAuxDef c.name) then
-                  recordUnfold c.name
                   deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => return e) go
                 else
                   return e
@@ -707,7 +706,7 @@ mutual
         | some e =>
           match (← withReducibleAndInstances <| reduceProj? e.getAppFn) with
           | none   => return none
-          | some r => recordUnfold declName; return mkAppN r e.getAppArgs |>.headBeta
+          | some r => return mkAppN r e.getAppArgs |>.headBeta
       | _ => return none
     | _ => return none
 
@@ -730,9 +729,8 @@ mutual
         if fInfo.levelParams.length != fLvls.length then
           return none
         else
-          let unfoldDefault (_ : Unit) : MetaM (Option Expr) := do
+          let unfoldDefault (_ : Unit) : MetaM (Option Expr) :=
             if fInfo.hasValue then
-              recordUnfold fInfo.name
               deltaBetaDefinition fInfo fLvls e.getAppRevArgs (fun _ => pure none) (fun e => pure (some e))
             else
               return none
@@ -780,13 +778,11 @@ mutual
                   Thus, we should keep `return some r` until Mathlib has been ported to Lean 3.
                   Note that the `Vector` example above does not even work in Lean 3.
                 -/
-                let some recArgPos ← getStructuralRecArgPos? fInfo.name
-                  | recordUnfold fInfo.name; return some r
+                let some recArgPos ← getStructuralRecArgPos? fInfo.name | return some r
                 let numArgs := e.getAppNumArgs
                 if recArgPos >= numArgs then return none
                 let recArg := e.getArg! recArgPos numArgs
                 if !(← isConstructorApp (← whnfMatcher recArg)) then return none
-                recordUnfold fInfo.name
                 return some r
             | _ =>
               if (← getMatcherInfo? fInfo.name).isSome then
@@ -804,7 +800,7 @@ mutual
         unless cinfo.hasValue do return none
         deltaDefinition cinfo lvls
           (fun _ => pure none)
-          (fun e => do recordUnfold declName; pure (some e))
+          (fun e => pure (some e))
     | _ => return none
 end
 
@@ -837,11 +833,11 @@ def reduceRecMatcher? (e : Expr) : MetaM (Option Expr) := do
     | .reduced e => return e
     | _ => 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))
+      | .recInfo «rec»  => reduceRec «rec» lvls e.getAppArgs (fun _ => pure none) (fun e => pure (some e))
+      | .quotInfo «rec» => reduceQuotRec «rec» e.getAppArgs (fun _ => pure none) (fun e => pure (some e))
       | c@(.defnInfo _) =>
         if (← isAuxDef c.name) then
-          deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => pure none) (fun e => do recordUnfold c.name; pure (some e))
+          deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => pure none) (fun e => pure (some e))
         else
           return none
       | _ => return none

src/Lean/Parser/Term.lean

@@ -870,7 +870,7 @@ def matchExprElseAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (ho
 def matchExprAlts (rhsParser : Parser) :=
   leading_parser withPosition $
     many (ppLine >> checkColGe "irrelevant" >> notFollowedBy (symbol "| " >> " _ ") "irrelevant" >> matchExprAlt rhsParser)
-    >> (ppLine >> checkColGe "else-alternative for `match_expr`, i.e., `| _ => ...`" >> matchExprElseAlt rhsParser)
+    >> (ppLine >> checkColGe "irrelevant" >> matchExprElseAlt rhsParser)
 @[builtin_term_parser] def matchExpr := leading_parser:leadPrec
   "match_expr " >> termParser >> " with" >> ppDedent (matchExprAlts termParser)
 

src/Lean/PrettyPrinter.lean

@@ -13,10 +13,7 @@ import Lean.ParserCompiler
 namespace Lean
 
 def PPContext.runCoreM {α : Type} (ppCtx : PPContext) (x : CoreM α) : IO α :=
-  Prod.fst <$> x.toIO { options := ppCtx.opts, currNamespace := ppCtx.currNamespace
-                        openDecls := ppCtx.openDecls
-                        fileName := "<PrettyPrinter>", fileMap := default
-                        diag     := getDiag ppCtx.opts }
+  Prod.fst <$> x.toIO { options := ppCtx.opts, currNamespace := ppCtx.currNamespace, openDecls := ppCtx.openDecls, fileName := "<PrettyPrinter>", fileMap := default }
                       { env := ppCtx.env, ngen := { namePrefix := `_pp_uniq } }
 
 def PPContext.runMetaM {α : Type} (ppCtx : PPContext) (x : MetaM α) : IO α :=
@@ -51,9 +48,7 @@ def ppExprWithInfos (e : Expr) (optsPerPos : Delaborator.OptionsPerPos := {}) (d
 
 @[export lean_pp_expr]
 def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format :=
-  Prod.fst <$> ((ppExpr e).run' { lctx := lctx } { mctx := mctx }).toIO {
-    options := opts, fileName := "<PrettyPrinter>", fileMap := default, diag := getDiag opts
-  } { env := env }
+  Prod.fst <$> ((ppExpr e).run' { lctx := lctx } { mctx := mctx }).toIO { options := opts, fileName := "<PrettyPrinter>", fileMap := default } { env := env }
 
 def ppTactic (stx : TSyntax `tactic) : CoreM Format := ppCategory `tactic stx
 

src/Lean/ReducibilityAttrs.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Attributes
-import Lean.ScopedEnvExtension
 
 namespace Lean
 
@@ -16,98 +15,34 @@ inductive ReducibilityStatus where
   | reducible | semireducible | irreducible
   deriving Inhabited, Repr
 
-builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × ReducibilityStatus) (Name × ReducibilityStatus) (NameMap ReducibilityStatus) ←
-  registerPersistentEnvExtension {
-    name            := `reducibilityCore
-    mkInitial       := pure {}
-    addImportedFn   := fun _ _ => pure {}
-    addEntryFn      := fun (s : NameMap ReducibilityStatus) (p : Name × ReducibilityStatus) => s.insert p.1 p.2
-    exportEntriesFn := fun m =>
-      let r : Array (Name × ReducibilityStatus) := m.fold (fun a n p => a.push (n, p)) #[]
-      r.qsort (fun a b => Name.quickLt a.1 b.1)
-    statsFn         := fun s => "reducibility attribute core extension" ++ Format.line ++ "number of local entries: " ++ format s.size
-  }
-
-builtin_initialize reducibilityExtraExt : SimpleScopedEnvExtension (Name × ReducibilityStatus) (SMap Name ReducibilityStatus) ←
-  registerSimpleScopedEnvExtension {
-    name := `reducibilityExtra
-    initial := {}
-    addEntry := fun d (declName, status) => d.insert declName status
-    finalizeImport := fun d => d.switch
-  }
+/--
+Environment extension for storing the reducibility attribute for definitions.
+-/
+builtin_initialize reducibilityAttrs : EnumAttributes ReducibilityStatus ←
+  registerEnumAttributes
+    [(`reducible, "reducible", ReducibilityStatus.reducible),
+     (`semireducible, "semireducible", ReducibilityStatus.semireducible),
+     (`irreducible, "irreducible", ReducibilityStatus.irreducible)]
 
 @[export lean_get_reducibility_status]
-def getReducibilityStatusCore (env : Environment) (declName : Name) : ReducibilityStatus :=
-  let m := reducibilityExtraExt.getState env
-  if let some status := m.find? declName then
-    status
-  else match env.getModuleIdxFor? declName with
-  | some modIdx =>
-    match (reducibilityCoreExt.getModuleEntries env modIdx).binSearch (declName, .semireducible) (fun a b => Name.quickLt a.1 b.1) with
-    | some (_, status) => status
-    | none => .semireducible
-  | none => (reducibilityCoreExt.getState env).find? declName |>.getD .semireducible
-
-def setReducibilityStatusCore (env : Environment) (declName : Name) (status : ReducibilityStatus) (attrKind : AttributeKind) (currNamespace : Name) : Environment :=
-  if attrKind matches .global then
-    match env.getModuleIdxFor? declName with
-    | some _ =>
-      -- Trying to set the attribute of a declaration defined in an imported module.
-      reducibilityExtraExt.addEntry env (declName, status)
-    | none =>
-      --
-      reducibilityCoreExt.addEntry env (declName, status)
-  else
-    -- `scoped` and `local` must be handled by `reducibilityExtraExt`
-    reducibilityExtraExt.addCore env (declName, status) attrKind currNamespace
+private def getReducibilityStatusImp (env : Environment) (declName : Name) : ReducibilityStatus :=
+  match reducibilityAttrs.getValue env declName with
+  | some s => s
+  | none   => ReducibilityStatus.semireducible
 
 @[export lean_set_reducibility_status]
-private def setReducibilityStatusImp (env : Environment) (declName : Name) (status : ReducibilityStatus) : Environment :=
-  setReducibilityStatusCore env declName status .global .anonymous
-
-builtin_initialize
-  registerBuiltinAttribute {
-    ref             := by exact decl_name%
-    name            := `irreducible
-    descr           := "irreducible declaration"
-    add             := fun declName stx attrKind => do
-      Attribute.Builtin.ensureNoArgs stx
-      let ns ← getCurrNamespace
-      modifyEnv fun env => setReducibilityStatusCore env declName .irreducible attrKind ns
-    applicationTime := .afterTypeChecking
- }
-
-builtin_initialize
-  registerBuiltinAttribute {
-    ref             := by exact decl_name%
-    name            := `reducible
-    descr           := "reducible declaration"
-    add             := fun declName stx attrKind => do
-      Attribute.Builtin.ensureNoArgs stx
-      let ns ← getCurrNamespace
-      modifyEnv fun env => setReducibilityStatusCore env declName .reducible attrKind ns
-    applicationTime := .afterTypeChecking
- }
-
-builtin_initialize
-  registerBuiltinAttribute {
-    ref             := by exact decl_name%
-    name            := `semireducible
-    descr           := "semireducible declaration"
-    add             := fun declName stx attrKind => do
-      Attribute.Builtin.ensureNoArgs stx
-      let ns ← getCurrNamespace
-      modifyEnv fun env => setReducibilityStatusCore env declName .reducible attrKind ns
-    applicationTime := .afterTypeChecking
- }
+private def setReducibilityStatusImp (env : Environment) (declName : Name) (s : ReducibilityStatus) : Environment :=
+  match reducibilityAttrs.setValue env declName s with
+  | Except.ok env => env
+  | _ => env -- TODO(Leo): we should extend EnumAttributes.setValue in the future and ensure it never fails
 
 /-- Return the reducibility attribute for the given declaration. -/
 def getReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) : m ReducibilityStatus := do
-  return getReducibilityStatusCore (← getEnv) declName
+  return getReducibilityStatusImp (← getEnv) declName
 
 /-- Set the reducibility attribute for the given declaration. -/
 def setReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit := do
-  modifyEnv fun env => setReducibilityStatusCore env declName s .global .anonymous
+  modifyEnv fun env => setReducibilityStatusImp env declName s
 
 /-- Set the given declaration as `[reducible]` -/
 def setReducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := do
@@ -116,13 +51,13 @@ def setReducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := d
 /-- Return `true` if the given declaration has been marked as `[reducible]`. -/
 def isReducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   match (← getReducibilityStatus declName) with
-  | .reducible => return true
+  | ReducibilityStatus.reducible => return true
   | _ => return false
 
 /-- Return `true` if the given declaration has been marked as `[irreducible]` -/
 def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   match (← getReducibilityStatus declName) with
-  | .irreducible => return true
+  | ReducibilityStatus.irreducible => return true
   | _ => return false
 
 end Lean

src/Lean/Replay.lean

@@ -50,7 +50,7 @@ def isTodo (name : Name) : M Bool := do
 
 /-- Use the current `Environment` to throw a `KernelException`. -/
 def throwKernelException (ex : KernelException) : M Unit := do
-    let ctx := { fileName := "", options := ({} : KVMap), fileMap := default, diag := false }
+    let ctx := { fileName := "", options := ({} : KVMap), fileMap := default }
     let state := { env := (← get).env }
     Prod.fst <$> (Lean.Core.CoreM.toIO · ctx state) do Lean.throwKernelException ex
 

src/Lean/ScopedEnvExtension.lean

@@ -146,15 +146,11 @@ def ScopedEnvExtension.addLocalEntry (ext : ScopedEnvExtension α β σ) (env :
     let top := { top with state := ext.descr.addEntry top.state b }
     ext.ext.setState env { s with stateStack := top :: states }
 
-def ScopedEnvExtension.addCore (env : Environment) (ext : ScopedEnvExtension α β σ) (b : β) (kind : AttributeKind) (namespaceName : Name) : Environment :=
-  match kind with
-  | AttributeKind.global => ext.addEntry env b
-  | AttributeKind.local  => ext.addLocalEntry env b
-  | AttributeKind.scoped => ext.addScopedEntry env namespaceName b
-
 def ScopedEnvExtension.add [Monad m] [MonadResolveName m] [MonadEnv m] (ext : ScopedEnvExtension α β σ) (b : β) (kind := AttributeKind.global) : m Unit := do
-  let ns ← getCurrNamespace
-  modifyEnv (ext.addCore · b kind ns)
+  match kind with
+  | AttributeKind.global => modifyEnv (ext.addEntry · b)
+  | AttributeKind.local  => modifyEnv (ext.addLocalEntry · b)
+  | AttributeKind.scoped => modifyEnv (ext.addScopedEntry · (← getCurrNamespace) b)
 
 def ScopedEnvExtension.getState [Inhabited σ] (ext : ScopedEnvExtension α β σ) (env : Environment) : σ :=
   match ext.ext.getState env |>.stateStack with

src/Lean/SubExpr.lean

@@ -54,24 +54,24 @@ def push (p : Pos) (c : Nat) : Pos :=
 variable {α : Type} [Inhabited α]
 
 /-- Fold over the position starting at the root and heading to the leaf-/
-partial def foldl  (f : α → Nat → α) (init : α) (p : Pos) : α :=
-  if p.isRoot then init else f (foldl f init p.tail) p.head
+partial def foldl  (f : α → Nat → α) (a : α) (p : Pos) : α :=
+  if p.isRoot then a else f (foldl f a p.tail) p.head
 
 /-- Fold over the position starting at the leaf and heading to the root-/
-partial def foldr  (f : Nat → α → α) (p : Pos) (init : α) : α :=
-  if p.isRoot then init else foldr f p.tail (f p.head init)
+partial def foldr  (f : Nat → α → α) (p : Pos) (a : α) : α :=
+  if p.isRoot then a else foldr f p.tail (f p.head a)
 
 /-- monad-fold over the position starting at the root and heading to the leaf -/
-partial def foldlM  [Monad M] (f : α → Nat → M α) (init : α) (p : Pos) : M α :=
+partial def foldlM  [Monad M] (f : α → Nat → M α) (a : α) (p : Pos) : M α :=
   have : Inhabited (M α) := inferInstance
-  if p.isRoot then pure init else do foldlM f init p.tail >>= (f · p.head)
+  if p.isRoot then pure a else do foldlM f a p.tail >>= (f · p.head)
 
 /-- monad-fold over the position starting at the leaf and finishing at the root. -/
-partial def foldrM [Monad M] (f : Nat → α → M α) (p : Pos) (init : α) : M α :=
-  if p.isRoot then pure init else f p.head init >>= foldrM f p.tail
+partial def foldrM [Monad M] (f : Nat → α → M α) (p : Pos) (a : α) : M α :=
+  if p.isRoot then pure a else f p.head a >>= foldrM f p.tail
 
 def depth (p : Pos) :=
-  p.foldr (init := 0) fun _ => Nat.succ
+  p.foldr (fun _ => Nat.succ) 0
 
 /-- Returns true if `pred` is true for each coordinate in `p`.-/
 def all (pred : Nat → Bool) (p : Pos) : Bool :=
@@ -134,8 +134,8 @@ protected def fromString? : String → Except String Pos
 
 protected def fromString! (s : String) : Pos :=
   match Pos.fromString? s with
-  | .ok a => a
-  | .error e => panic! e
+  | Except.ok a => a
+  | Except.error e => panic! e
 
 instance : Ord Pos := show Ord Nat by infer_instance
 instance : DecidableEq Pos := show DecidableEq Nat by infer_instance
@@ -213,7 +213,7 @@ open SubExpr in
 `SubExpr.Pos` argument for tracking subexpression position. -/
 def Expr.traverseAppWithPos {M} [Monad M] (visit : Pos → Expr → M Expr) (p : Pos) (e : Expr) : M Expr :=
   match e with
-  | .app f a =>
+  | Expr.app f a =>
     e.updateApp!
       <$> traverseAppWithPos visit p.pushAppFn f
       <*> visit p.pushAppArg a

src/kernel/CMakeLists.txt

@@ -2,4 +2,4 @@ add_library(kernel OBJECT level.cpp expr.cpp expr_eq_fn.cpp
 for_each_fn.cpp replace_fn.cpp abstract.cpp instantiate.cpp
 local_ctx.cpp declaration.cpp environment.cpp type_checker.cpp
 init_module.cpp expr_cache.cpp equiv_manager.cpp quot.cpp
-inductive.cpp trace.cpp)
+inductive.cpp)

src/kernel/declaration.cpp

@@ -205,10 +205,6 @@ declaration mk_definition(environment const & env, name const & n, names const &
     return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Definition), mk_definition_val(env, n, params, t, v, safety)));
 }
 
-declaration mk_theorem(name const & n, names const & lparams, expr const & type, expr const & val) {
-    return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Theorem), theorem_val(n, lparams, type, val)));
-}
-
 declaration mk_opaque(name const & n, names const & params, expr const & t, expr const & v, bool is_unsafe) {
     return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Opaque), opaque_val(n, params, t, v, is_unsafe, names(n))));
 }

src/kernel/declaration.h

@@ -223,12 +223,10 @@ inline optional<declaration> none_declaration() { return optional<declaration>()
 inline optional<declaration> some_declaration(declaration const & o) { return optional<declaration>(o); }
 inline optional<declaration> some_declaration(declaration && o) { return optional<declaration>(std::forward<declaration>(o)); }
 
-bool use_unsafe(environment const & env, expr const & e);
 declaration mk_definition(name const & n, names const & lparams, expr const & t, expr const & v,
                           reducibility_hints const & hints, definition_safety safety = definition_safety::safe);
 declaration mk_definition(environment const & env, name const & n, names const & lparams, expr const & t, expr const & v,
                           definition_safety safety = definition_safety::safe);
-declaration mk_theorem(name const & n, names const & lparams, expr const & type, expr const & val);
 declaration mk_opaque(name const & n, names const & lparams, expr const & t, expr const & v, bool unsafe);
 declaration mk_axiom(name const & n, names const & lparams, expr const & t, bool unsafe = false);
 declaration mk_inductive_decl(names const & lparams, nat const & nparams, inductive_types const & types, bool is_unsafe);

src/kernel/init_module.cpp

@@ -12,7 +12,6 @@ Author: Leonardo de Moura
 #include "kernel/local_ctx.h"
 #include "kernel/inductive.h"
 #include "kernel/quot.h"
-#include "kernel/trace.h"
 
 namespace lean {
 void initialize_kernel_module() {
@@ -24,11 +23,9 @@ void initialize_kernel_module() {
     initialize_local_ctx();
     initialize_inductive();
     initialize_quot();
-    initialize_trace();
 }
 
 void finalize_kernel_module() {
-    finalize_trace();
     finalize_quot();
     finalize_inductive();
     finalize_local_ctx();

src/lake/Lake/CLI/Translate.lean

@@ -28,7 +28,7 @@ def Package.mkConfigString (pkg : Package) (lang : ConfigLang) : LogIO String :=
   | .lean => do
     let env ← importModulesUsingCache #[`Lake] {} 1024
     let pp := ppModule <| descopeTSyntax <| pkg.mkLeanConfig
-    match (← pp.toIO {fileName := "", fileMap := default, diag := false} {env} |>.toBaseIO) with
+    match (← pp.toIO {fileName := "", fileMap := default} {env} |>.toBaseIO) with
     | .ok (fmt, _) => pure <| (toString fmt).trim ++ "\n"
     | .error ex =>
       error s!"(internal) failed to pretty print Lean configuration: {ex.toString}"

src/lake/Lake/Toml/Load.lean

@@ -22,7 +22,7 @@ def loadToml (ictx : InputContext) : EIO MessageLog Table := do
     throw <|  MessageLog.empty.add <| mkParserErrorMessage ictx s errorMsg
   else if ictx.input.atEnd s.pos then
     let act := elabToml ⟨s.stxStack.back⟩
-    match (← act.run {fileName := ictx.fileName, fileMap := ictx.fileMap, diag := false} {env} |>.toBaseIO) with
+    match (← act.run {fileName := ictx.fileName, fileMap := ictx.fileMap} {env} |>.toBaseIO) with
     | .ok (t, s) =>
       if s.messages.hasErrors then
         throw s.messages

src/library/CMakeLists.txt

@@ -4,6 +4,6 @@ add_library(library OBJECT expr_lt.cpp
   class.cpp util.cpp print.cpp annotation.cpp
   protected.cpp reducible.cpp init_module.cpp
   projection.cpp
-  aux_recursors.cpp
+  aux_recursors.cpp trace.cpp
   profiling.cpp time_task.cpp
   formatter.cpp)

src/library/compiler/borrowed_annotation.cpp

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/instantiate.h"
-#include "kernel/trace.h"
+#include "library/trace.h"
 #include "library/annotation.h"
 #include "library/compiler/util.h"
 #include "library/compiler/llnf.h"

src/library/compiler/compiler.cpp

@@ -8,8 +8,8 @@ Author: Leonardo de Moura
 #include "util/io.h"
 #include "kernel/type_checker.h"
 #include "kernel/kernel_exception.h"
-#include "kernel/trace.h"
 #include "library/max_sharing.h"
+#include "library/trace.h"
 #include "library/time_task.h"
 #include "library/compiler/util.h"
 #include "library/compiler/lcnf.h"

src/library/compiler/csimp.cpp

@@ -15,10 +15,10 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/inductive.h"
 #include "kernel/kernel_exception.h"
-#include "kernel/trace.h"
 #include "library/util.h"
 #include "library/constants.h"
 #include "library/class.h"
+#include "library/trace.h"
 #include "library/expr_pair_maps.h"
 #include "library/compiler/util.h"
 #include "library/compiler/cse.h"

src/library/compiler/eager_lambda_lifting.cpp

@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/for_each_fn.h"
 #include "kernel/type_checker.h"
 #include "kernel/inductive.h"
-#include "kernel/trace.h"
+#include "library/trace.h"
 #include "library/class.h"
 #include "library/compiler/util.h"
 #include "library/compiler/csimp.h"

src/library/compiler/extract_closed.cpp

@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/expr_maps.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/inductive.h"
-#include "kernel/trace.h"
+#include "library/trace.h"
 #include "library/compiler/util.h"
 #include "library/compiler/closed_term_cache.h"
 #include "library/compiler/reduce_arity.h"

src/library/compiler/ir.cpp

@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "util/nat.h"
 #include "kernel/instantiate.h"
 #include "kernel/type_checker.h"
-#include "kernel/trace.h"
+#include "library/trace.h"
 #include "library/compiler/util.h"
 #include "library/compiler/llnf.h"
 #include "library/compiler/extern_attribute.h"

src/library/compiler/ir_interpreter.cpp

@@ -40,8 +40,8 @@ functions, which have a (relatively) homogeneous ABI that we can use without run
 #include "runtime/io.h"
 #include "runtime/option_ref.h"
 #include "runtime/array_ref.h"
-#include "kernel/trace.h"
 #include "library/time_task.h"
+#include "library/trace.h"
 #include "library/compiler/ir.h"
 #include "library/compiler/init_attribute.h"
 #include "util/nat.h"

src/library/compiler/lambda_lifting.cpp

@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/inductive.h"
-#include "kernel/trace.h"
+#include "library/trace.h"
 #include "library/compiler/util.h"
 #include "library/compiler/closed_term_cache.h"
 

src/library/compiler/llnf.cpp

@@ -16,8 +16,8 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/inductive.h"
-#include "kernel/trace.h"
 #include "library/util.h"
+#include "library/trace.h"
 #include "library/compiler/util.h"
 #include "library/compiler/llnf.h"
 #include "library/compiler/ll_infer_type.h"

src/library/compiler/specialize.cpp

@@ -10,8 +10,8 @@ Author: Leonardo de Moura
 #include "kernel/for_each_fn.h"
 #include "kernel/abstract.h"
 #include "kernel/inductive.h"
-#include "kernel/trace.h"
 #include "library/class.h"
+#include "library/trace.h"
 #include "library/compiler/util.h"
 #include "library/compiler/csimp.h"
 

src/library/compiler/struct_cases_on.cpp

@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/type_checker.h"
 #include "kernel/inductive.h"
-#include "kernel/trace.h"
+#include "library/trace.h"
 #include "library/suffixes.h"
 #include "library/compiler/util.h"
 

src/library/compiler/util.cpp

@@ -18,12 +18,12 @@ Author: Leonardo de Moura
 #include "kernel/inductive.h"
 #include "kernel/instantiate.h"
 #include "kernel/kernel_exception.h"
-#include "kernel/trace.h"
 #include "library/util.h"
 #include "library/suffixes.h"
 #include "library/aux_recursors.h"
 #include "library/replace_visitor.h"
 #include "library/constants.h"
+#include "library/trace.h"
 #include "library/compiler/lambda_lifting.h"
 #include "library/compiler/eager_lambda_lifting.h"
 #include "library/compiler/util.h"

src/library/constructions/projection.cpp

@@ -86,8 +86,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
             throw exception(sstream() << "generating projection '" << proj_name << "', '"
                             << n << "' does not have sufficient data");
         expr result_type   = consume_type_annotations(binding_domain(cnstr_type));
-        bool is_prop       = type_checker(new_env, lctx).is_prop(result_type);
-        if (is_predicate && !is_prop) {
+        if (is_predicate && !type_checker(new_env, lctx).is_prop(result_type)) {
             throw exception(sstream() << "failed to generate projection '" << proj_name << "' for '" << n << "', "
                             << "type is an inductive predicate, but field is not a proposition");
         }
@@ -98,27 +97,13 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
         proj_type      = infer_implicit_params(proj_type, nparams, implicit_infer_kind::RelaxedImplicit);
         expr proj_val  = mk_proj(n, i, c);
         proj_val = lctx.mk_lambda(proj_args, proj_val);
-        declaration new_d;
-        // TODO: replace `if (false) {` with `if (is_prop) {`.
-        // Mathlib is crashing when prop fields are theorems.
-        // The crash is in the ir_interpreter. Kyle suspects this is an use-after-free bug in the interpreter.
-        if (false) { // if (is_prop) {
-            bool unsafe = use_unsafe(env, proj_type) || use_unsafe(env, proj_val);
-            if (unsafe) {
-                // theorems cannot be unsafe
-                new_d = mk_opaque(proj_name, lvl_params, proj_type, proj_val, unsafe);
-            } else {
-                new_d = mk_theorem(proj_name, lvl_params, proj_type, proj_val);
-            }
-        } else {
-            new_d = mk_definition_inferring_unsafe(env, proj_name, lvl_params, proj_type, proj_val,
+        declaration new_d = mk_definition_inferring_unsafe(env, proj_name, lvl_params, proj_type, proj_val,
                                                            reducibility_hints::mk_abbreviation());
-        }
         new_env = new_env.add(new_d);
-        if (!inst_implicit && !is_prop)
+        if (!inst_implicit)
             new_env = set_reducible(new_env, proj_name, reducible_status::Reducible, true);
         new_env = save_projection_info(new_env, proj_name, cnstr_info.get_name(), nparams, i, inst_implicit);
-        expr proj    = mk_app(mk_app(mk_constant(proj_name, lvls), params), c);
+        expr proj         = mk_app(mk_app(mk_constant(proj_name, lvls), params), c);
         cnstr_type   = instantiate(binding_body(cnstr_type), proj);
         i++;
     }

src/library/init_module.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "library/trace.h"
 #include "library/constants.h"
 #include "library/class.h"
 #include "library/num.h"
@@ -20,9 +21,11 @@ void initialize_library_core_module() {
     initialize_formatter();
     initialize_constants();
     initialize_profiling();
+    initialize_trace();
 }
 
 void finalize_library_core_module() {
+    finalize_trace();
     finalize_profiling();
     finalize_constants();
     finalize_formatter();

src/library/time_task.cpp

@@ -7,7 +7,7 @@ Author: Sebastian Ullrich
 #include <string>
 #include <map>
 #include "library/time_task.h"
-#include "kernel/trace.h"
+#include "library/trace.h"
 
 namespace lean {
 

src/library/trace.cpp

@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "util/option_declarations.h"
 #include "kernel/environment.h"
 #include "kernel/local_ctx.h"
-#include "kernel/trace.h"
+#include "library/trace.h"
 
 namespace lean {
 static name_set *            g_trace_classes = nullptr;

src/util/shell.cpp

@@ -29,11 +29,11 @@ Author: Leonardo de Moura
 #include "util/option_declarations.h"
 #include "kernel/environment.h"
 #include "kernel/kernel_exception.h"
-#include "kernel/trace.h"
 #include "library/formatter.h"
 #include "library/module.h"
 #include "library/time_task.h"
 #include "library/compiler/ir.h"
+#include "library/trace.h"
 #include "library/print.h"
 #include "initialize/init.h"
 #include "library/compiler/ir_interpreter.h"