fix: disable USize simprocs

.github/workflows/ci.yml

@@ -410,8 +410,7 @@ jobs:
         run: |
           cd build
           ulimit -c unlimited # coredumps
-          # clean rebuild in case of Makefile changes
-          make update-stage0 && rm -rf ./stage* && make -j4
+          make update-stage0 && make -j4
         if: matrix.name == 'Linux' && needs.configure.outputs.quick == 'false'
       - name: CCache stats
         run: ccache -s

RELEASES.md

@@ -18,10 +18,6 @@ v4.7.0 (development in progress)
 
 * `pp.proofs.withType` is now set to false by default to reduce noise in the info view.
 
-* The pretty printer for applications now handles the case of over-application itself when applying app unexpanders.
-  In particular, the ``| `($_ $a $b $xs*) => `(($a + $b) $xs*)`` case of an `app_unexpander` is no longer necessary.
-  [#3495](https://github.com/leanprover/lean4/pull/3495).
-
 * New `simp` (and `dsimp`) configuration option: `zetaDelta`. It is `false` by default.
   The `zeta` option is still `true` by default, but their meaning has changed.
   - When `zeta := true`, `simp` and `dsimp` reduce terms of the form
@@ -30,7 +26,7 @@ v4.7.0 (development in progress)
     the context. For example, suppose the context contains `x := val`. Then,
     any occurrence of `x` is replaced with `val`.
 
-  See [issue #2682](https://github.com/leanprover/lean4/pull/2682) for additional details. Here are some examples:
+  See issue [#2682](https://github.com/leanprover/lean4/pull/2682) for additional details. Here are some examples:
   ```
   example (h : z = 9) : let x := 5; let y := 4; x + y = z := by
     intro x
@@ -71,7 +67,7 @@ v4.7.0 (development in progress)
   ```
 
 * When adding new local theorems to `simp`, the system assumes that the function application arguments
-  have been annotated with `no_index`. This modification, which addresses [issue #2670](https://github.com/leanprover/lean4/issues/2670),
+  have been annotated with `no_index`. This modification, which addresses issue [#2670](https://github.com/leanprover/lean4/issues/2670),
   restores the Lean 3 behavior that users expect. With this modification, the following examples are now operational:
   ```
   example {α β : Type} {f : α × β → β → β} (h : ∀ p : α × β, f p p.2 = p.2)
@@ -85,30 +81,6 @@ v4.7.0 (development in progress)
   In both cases, `h` is applicable because `simp` does not index f-arguments anymore when adding `h` to the `simp`-set.
   It's important to note, however, that global theorems continue to be indexed in the usual manner.
 
-* Improved the error messages produced by the `decide` tactic. [#3422](https://github.com/leanprover/lean4/pull/3422)
-
-* Improved auto-completion performance. [#3460](https://github.com/leanprover/lean4/pull/3460)
-
-* Improved initial language server startup performance. [#3552](https://github.com/leanprover/lean4/pull/3552)
-
-* Changed call hierarchy to sort entries and strip private header from names displayed in the call hierarchy. [#3482](https://github.com/leanprover/lean4/pull/3482)
-
-* There is now a low-level error recovery combinator in the parsing framework, primarily intended for DSLs. [#3413](https://github.com/leanprover/lean4/pull/3413)
-* The Library search `exact?` and `apply?` tactics that were originally in
-* The library search tactics `exact?` and `apply?` that were originally in
-  Mathlib are now available in Lean itself.  These use the implementation using
-  lazy discrimination trees from `Std`, and thus do not require a disk cache but
-  have a slightly longer startup time.  The order used for selection lemmas has
-  changed as well to favor goals purely based on how many terms in the head
-  pattern match the current goal.
-
-* The `solve_by_elim` tactic has been ported from `Std` to Lean so that library
-  search can use it.
-
-* New `#check_tactic` and `#check_simp` commands have been added.  These are
-  useful for checking tactics (particularly `simp`) behave as expected in test
-  suites.
-
 Breaking changes:
 * `Lean.withTraceNode` and variants got a stronger `MonadAlwaysExcept` assumption to
   fix trace trees not being built on elaboration runtime exceptions. Instances for most elaboration
@@ -118,67 +90,67 @@ v4.6.0
 ---------
 
 * Add custom simplification procedures (aka `simproc`s) to `simp`. Simprocs can be triggered by the simplifier on a specified term-pattern. Here is an small example:
-  ```lean
-  import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
+```lean
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 
-  def foo (x : Nat) : Nat :=
-    x + 10
+def foo (x : Nat) : Nat :=
+  x + 10
 
-  /--
-  The `simproc` `reduceFoo` is invoked on terms that match the pattern `foo _`.
-  -/
-  simproc reduceFoo (foo _) :=
-    /- A term of type `Expr → SimpM Step -/
-    fun e => do
-      /-
-      The `Step` type has three constructors: `.done`, `.visit`, `.continue`.
-      * The constructor `.done` instructs `simp` that the result does
-        not need to be simplied further.
-      * The constructor `.visit` instructs `simp` to visit the resulting expression.
-      * The constructor `.continue` instructs `simp` to try other simplification procedures.
-
-      All three constructors take a `Result`. The `.continue` contructor may also take `none`.
-      `Result` has two fields `expr` (the new expression), and `proof?` (an optional proof).
-       If the new expression is definitionally equal to the input one, then `proof?` can be omitted or set to `none`.
-      -/
-      /- `simp` uses matching modulo reducibility. So, we ensure the term is a `foo`-application. -/
-      unless e.isAppOfArity ``foo 1 do
-        return .continue
-      /- `Nat.fromExpr?` tries to convert an expression into a `Nat` value -/
-      let some n ← Nat.fromExpr? e.appArg!
-        | return .continue
-      return .done { expr := Lean.mkNatLit (n+10) }
-  ```
-  We disable simprocs support by using the command `set_option simprocs false`. This command is particularly useful when porting files to v4.6.0.
-  Simprocs can be scoped, manually added to `simp` commands, and suppressed using `-`. They are also supported by `simp?`. `simp only` does not execute any `simproc`. Here are some examples for the `simproc` defined above.
-  ```lean
-  example : x + foo 2 = 12 + x := by
-    set_option simprocs false in
-      /- This `simp` command does not make progress since `simproc`s are disabled. -/
-      fail_if_success simp
-    simp_arith
-
-  example : x + foo 2 = 12 + x := by
-    /- `simp only` must not use the default simproc set. -/
-    fail_if_success simp only
-    simp_arith
-
-  example : x + foo 2 = 12 + x := by
+/--
+The `simproc` `reduceFoo` is invoked on terms that match the pattern `foo _`.
+-/
+simproc reduceFoo (foo _) :=
+  /- A term of type `Expr → SimpM Step -/
+  fun e => do
     /-
-    `simp only` does not use the default simproc set,
-    but we can provide simprocs as arguments. -/
-    simp only [reduceFoo]
-    simp_arith
+    The `Step` type has three constructors: `.done`, `.visit`, `.continue`.
+    * The constructor `.done` instructs `simp` that the result does
+      not need to be simplied further.
+    * The constructor `.visit` instructs `simp` to visit the resulting expression.
+    * The constructor `.continue` instructs `simp` to try other simplification procedures.
 
-  example : x + foo 2 = 12 + x := by
-    /- We can use `-` to disable `simproc`s. -/
-    fail_if_success simp [-reduceFoo]
-    simp_arith
-  ```
-  The command `register_simp_attr <id>` now creates a `simp` **and** a `simproc` set with the name `<id>`. The following command instructs Lean to insert the `reduceFoo` simplification procedure into the set `my_simp`. If no set is specified, Lean uses the default `simp` set.
-  ```lean
-  simproc [my_simp] reduceFoo (foo _) := ...
-  ```
+    All three constructors take a `Result`. The `.continue` contructor may also take `none`.
+    `Result` has two fields `expr` (the new expression), and `proof?` (an optional proof).
+     If the new expression is definitionally equal to the input one, then `proof?` can be omitted or set to `none`.
+    -/
+    /- `simp` uses matching modulo reducibility. So, we ensure the term is a `foo`-application. -/
+    unless e.isAppOfArity ``foo 1 do
+      return .continue
+    /- `Nat.fromExpr?` tries to convert an expression into a `Nat` value -/
+    let some n ← Nat.fromExpr? e.appArg!
+      | return .continue
+    return .done { expr := Lean.mkNatLit (n+10) }
+```
+We disable simprocs support by using the command `set_option simprocs false`. This command is particularly useful when porting files to v4.6.0.
+Simprocs can be scoped, manually added to `simp` commands, and suppressed using `-`. They are also supported by `simp?`. `simp only` does not execute any `simproc`. Here are some examples for the `simproc` defined above.
+```lean
+example : x + foo 2 = 12 + x := by
+  set_option simprocs false in
+    /- This `simp` command does not make progress since `simproc`s are disabled. -/
+    fail_if_success simp
+  simp_arith
+
+example : x + foo 2 = 12 + x := by
+  /- `simp only` must not use the default simproc set. -/
+  fail_if_success simp only
+  simp_arith
+
+example : x + foo 2 = 12 + x := by
+  /-
+  `simp only` does not use the default simproc set,
+  but we can provide simprocs as arguments. -/
+  simp only [reduceFoo]
+  simp_arith
+
+example : x + foo 2 = 12 + x := by
+  /- We can use `-` to disable `simproc`s. -/
+  fail_if_success simp [-reduceFoo]
+  simp_arith
+```
+The command `register_simp_attr <id>` now creates a `simp` **and** a `simproc` set with the name `<id>`. The following command instructs Lean to insert the `reduceFoo` simplification procedure into the set `my_simp`. If no set is specified, Lean uses the default `simp` set.
+```lean
+simproc [my_simp] reduceFoo (foo _) := ...
+```
 
 * The syntax of the `termination_by` and `decreasing_by` termination hints is overhauled:
 
@@ -317,7 +289,7 @@ v4.6.0
   and hence greatly reduces the reliance on costly structure eta reduction. This has a large impact on mathlib,
   reducing total CPU instructions by 3% and enabling impactful refactors like leanprover-community/mathlib4#8386
   which reduces the build time by almost 20%.
-  See [PR #2478](https://github.com/leanprover/lean4/pull/2478) and [RFC #2451](https://github.com/leanprover/lean4/issues/2451).
+  See PR [#2478](https://github.com/leanprover/lean4/pull/2478) and RFC [#2451](https://github.com/leanprover/lean4/issues/2451).
 
 * Add pretty printer settings to omit deeply nested terms (`pp.deepTerms false` and `pp.deepTerms.threshold`) ([PR #3201](https://github.com/leanprover/lean4/pull/3201))
 
@@ -336,7 +308,7 @@ Other improvements:
 * produce simpler proof terms in `rw` [#3121](https://github.com/leanprover/lean4/pull/3121)
 * fuse nested `mkCongrArg` calls in proofs generated by `simp` [#3203](https://github.com/leanprover/lean4/pull/3203)
 * `induction using` followed by a general term [#3188](https://github.com/leanprover/lean4/pull/3188)
-* allow generalization in `let` [#3060](https://github.com/leanprover/lean4/pull/3060), fixing [#3065](https://github.com/leanprover/lean4/issues/3065)
+* allow generalization in `let` [#3060](https://github.com/leanprover/lean4/pull/3060, fixing [#3065](https://github.com/leanprover/lean4/issues/3065)
 * reducing out-of-bounds `swap!` should return `a`, not `default`` [#3197](https://github.com/leanprover/lean4/pull/3197), fixing [#3196](https://github.com/leanprover/lean4/issues/3196)
 * derive `BEq` on structure with `Prop`-fields [#3191](https://github.com/leanprover/lean4/pull/3191), fixing [#3140](https://github.com/leanprover/lean4/issues/3140)
 * refine through more `casesOnApp`/`matcherApp` [#3176](https://github.com/leanprover/lean4/pull/3176), fixing [#3175](https://github.com/leanprover/lean4/pull/3175)

script/prepare-llvm-linux.sh

@@ -25,8 +25,6 @@ cp -L llvm/bin/llvm-ar stage1/bin/
 # dependencies of the above
 $CP llvm/lib/lib{clang-cpp,LLVM}*.so* stage1/lib/
 $CP $ZLIB/lib/libz.so* stage1/lib/
-# general clang++ dependency, breaks cross-library C++ exceptions if linked statically
-$CP $GCC_LIB/lib/libgcc_s.so* stage1/lib/
 # bundle libatomic (referenced by LLVM >= 15, and required by the lean executable to run)
 $CP $GCC_LIB/lib/libatomic.so* stage1/lib/
 
@@ -62,7 +60,7 @@ fi
 # use `-nostdinc` to make sure headers are not visible by default (in particular, not to `#include_next` in the clang headers),
 # but do not change sysroot so users can still link against system libs
 echo -n " -DLEANC_INTERNAL_FLAGS='-nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a -Wl,--as-needed -static-libgcc -Wl,-Bstatic -lgmp -lunwind -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
 # when not using the above flags, link GMP dynamically/as usual
 echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -Wl,--no-as-needed'"
 # do not set `LEAN_CC` for tests

src/CMakeLists.txt

@@ -501,18 +501,24 @@ string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
 # (also looks nicer in the build log)
 file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
 
-# set up libInit_shared only on Windows; see also stdlib.make.in
-if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
+if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
+  string(APPEND INIT_SHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a")
+else()
+  string(APPEND INIT_SHARED_LINKER_FLAGS " -Wl,--whole-archive -lInit ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive")
+  if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+    string(APPEND INIT_SHARED_LINKER_FLAGS " -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
+  endif()
 endif()
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
-  set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
-elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
+  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a")
 else()
-  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
+  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive")
+  if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+    string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
+  endif()
 endif()
+string(APPEND LEANSHARED_LINKER_FLAGS " -lInit_shared")
 
 if (${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
   # We do not use dynamic linking via leanshared for Emscripten to keep things

src/Init/Coe.lean

@@ -321,7 +321,7 @@ Helper definition used by the elaborator. It is not meant to be used directly by
 This is used for coercions between monads, in the case where we want to apply
 a monad lift and a coercion on the result type at the same time.
 -/
-@[coe_decl] abbrev Lean.Internal.liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u}
+@[inline, coe_decl] def Lean.Internal.liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u}
     [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β := do
   let a ← liftM x
   pure (CoeT.coe a)
@@ -331,7 +331,7 @@ Helper definition used by the elaborator. It is not meant to be used directly by
 
 This is used for coercing the result type under a monad.
 -/
-@[coe_decl] abbrev Lean.Internal.coeM {m : Type u → Type v} {α β : Type u}
+@[inline, coe_decl] def Lean.Internal.coeM {m : Type u → Type v} {α β : Type u}
     [∀ a, CoeT α a β] [Monad m] (x : m α) : m β := do
   let a ← x
   pure (CoeT.coe a)

src/Init/Data/Array/Lemmas.lean

@@ -185,84 +185,3 @@ theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start
 
 theorem mem_def (a : α) (as : Array α) : a ∈ as ↔ a ∈ as.data :=
   ⟨fun | .mk h => h, Array.Mem.mk⟩
-
-/-- # get -/
-@[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl
-
-theorem getElem?_lt
-    (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some (a[i]) := dif_pos h
-
-theorem getElem?_ge
-    (a : Array α) {i : Nat} (h : i ≥ a.size) : a[i]? = none := dif_neg (Nat.not_lt_of_le h)
-
-@[simp] theorem get?_eq_getElem? (a : Array α) (i : Nat) : a.get? i = a[i]? := rfl
-
-theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = none := by
-  simp [getElem?_ge, h]
-
-theorem getD_get? (a : Array α) (i : Nat) (d : α) :
-  Option.getD a[i]? d = if p : i < a.size then a[i]'p else d := by
-  if h : i < a.size then
-    simp [setD, h, getElem?]
-  else
-    have p : i ≥ a.size := Nat.le_of_not_gt h
-    simp [setD, getElem?_len_le _ p, h]
-
-@[simp] theorem getD_eq_get? (a : Array α) (n d) : a.getD n d = (a[n]?).getD d := by
-  simp only [getD, get_eq_getElem, get?_eq_getElem?]; split <;> simp [getD_get?, *]
-
-theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default := rfl
-
-@[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) : a.get! i = (a.get? i).getD default := by
-  by_cases p : i < a.size <;> simp [getD_get?, get!_eq_getD, p]
-
-/-- # set -/
-
-@[simp] theorem getElem_set_eq (a : Array α) (i : Fin a.size) (v : α) {j : Nat}
-      (eq : i.val = j) (p : j < (a.set i v).size) :
-    (a.set i v)[j]'p = v := by
-  simp [set, getElem_eq_data_get, ←eq]
-
-@[simp] theorem getElem_set_ne (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (pj : j < (a.set i v).size)
-    (h : i.val ≠ j) : (a.set i v)[j]'pj = a[j]'(size_set a i v ▸ pj) := by
-  simp only [set, getElem_eq_data_get, List.get_set_ne _ h]
-
-theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
-    (h : j < (a.set i v).size) :
-    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v ▸ h) := by
-  by_cases p : i.1 = j <;> simp [p]
-
-@[simp] theorem getElem?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
-    (a.set i v)[i.1]? = v := by simp [getElem?_lt, i.2]
-
-@[simp] theorem getElem?_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α)
-    (ne : i.val ≠ j) : (a.set i v)[j]? = a[j]? := by
-  by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
-
-/- # setD -/
-
-@[simp] theorem set!_is_setD : @set! = @setD := rfl
-
-@[simp] theorem size_setD (a : Array α) (index : Nat) (val : α) :
-  (Array.setD a index val).size = a.size := by
-  if h : index < a.size  then
-    simp [setD, h]
-  else
-    simp [setD, h]
-
-@[simp] theorem getElem_setD_eq (a : Array α) {i : Nat} (v : α) (h : _) :
-  (setD a i v)[i]'h = v := by
-  simp at h
-  simp only [setD, h, dite_true, getElem_set, ite_true]
-
-@[simp]
-theorem getElem?_setD_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a.setD i v)[i]? = some v := by
-  simp [getElem?_lt, p]
-
-/-- Simplifies a normal form from `get!` -/
-@[simp] theorem getD_get?_setD (a : Array α) (i : Nat) (v d : α) :
-  Option.getD (setD a i v)[i]? d = if i < a.size then v else d := by
-  by_cases h : i < a.size <;>
-    simp [setD, Nat.not_lt_of_le, h,  getD_get?]
-
-end Array

src/Init/Data/BitVec/Basic.lean

@@ -124,20 +124,13 @@ section Int
 
 /-- Interpret the bitvector as an integer stored in two's complement form. -/
 protected def toInt (a : BitVec n) : Int :=
-  if 2 * a.toNat < 2^n then
-    a.toNat
-  else
-    (a.toNat : Int) - (2^n : Nat)
+  if a.msb then Int.ofNat a.toNat - Int.ofNat (2^n) else a.toNat
 
 /-- The `BitVec` with value `(2^n + (i mod 2^n)) mod 2^n`.  -/
-protected def ofInt (n : Nat) (i : Int) : BitVec n := .ofNatLt (i % (Int.ofNat (2^n))).toNat (by
-  apply (Int.toNat_lt _).mpr
-  · apply Int.emod_lt_of_pos
-    exact Int.ofNat_pos.mpr (Nat.two_pow_pos _)
-  · apply Int.emod_nonneg
-    intro eq
-    apply Nat.ne_of_gt (Nat.two_pow_pos n)
-    exact Int.ofNat_inj.mp eq)
+protected def ofInt (n : Nat) (i : Int) : BitVec n :=
+  match i with
+  | Int.ofNat x => .ofNat n x
+  | Int.negSucc x => BitVec.ofNatLt (2^n - x % 2^n - 1) (by omega)
 
 instance : IntCast (BitVec w) := ⟨BitVec.ofInt w⟩
 

src/Init/Data/BitVec/Lemmas.lean

@@ -133,35 +133,21 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
   · simp [BitVec.eq_nil x]
   · simp
 
-@[bv_toNat] theorem getLsb_last (x : BitVec w) :
-    x.getLsb (w-1) = decide (2 ^ (w-1) ≤ x.toNat) := by
-  rcases w with rfl | w
-  · simp
-  · simp only [Nat.zero_lt_succ, decide_True, getLsb, Nat.testBit, Nat.succ_sub_succ_eq_sub,
+@[bv_toNat] theorem getLsb_last (x : BitVec (w + 1)) :
+    x.getLsb w = decide (2 ^ w ≤ x.toNat) := by
+  simp only [Nat.zero_lt_succ, decide_True, getLsb, Nat.testBit, Nat.succ_sub_succ_eq_sub,
     Nat.sub_zero, Nat.and_one_is_mod, Bool.true_and, Nat.shiftRight_eq_div_pow]
-    rcases (Nat.lt_or_ge (BitVec.toNat x) (2 ^ w)) with h | h
-    · simp [Nat.div_eq_of_lt h, h]
-    · simp only [h]
-      rw [Nat.div_eq_sub_div (Nat.two_pow_pos w) h, Nat.div_eq_of_lt]
-      · decide
-      · have : BitVec.toNat x < 2^w + 2^w := by simpa [Nat.pow_succ, Nat.mul_two] using x.isLt
-        omega
+  rcases (Nat.lt_or_ge (BitVec.toNat x) (2 ^ w)) with h | h
+  · simp [Nat.div_eq_of_lt h, h]
+  · simp only [h]
+    rw [Nat.div_eq_sub_div (Nat.two_pow_pos w) h, Nat.div_eq_of_lt]
+    · decide
+    · have : BitVec.toNat x < 2^w + 2^w := by simpa [Nat.pow_succ, Nat.mul_two] using x.isLt
+      omega
 
-@[bv_toNat] theorem getLsb_succ_last (x : BitVec (w + 1)) :
-    x.getLsb w = decide (2 ^ w ≤ x.toNat) := getLsb_last x
-
-@[bv_toNat] theorem msb_eq_decide (x : BitVec w) : BitVec.msb x = decide (2 ^ (w-1) ≤ x.toNat) := by
+@[bv_toNat] theorem msb_eq_decide (x : BitVec (w + 1)) : BitVec.msb x = decide (2 ^ w ≤ x.toNat) := by
   simp [msb_eq_getLsb_last, getLsb_last]
 
-theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat ≥ 2^(n-1) := by
-  match n with
-  | 0 =>
-    simp [BitVec.msb, BitVec.getMsb] at p
-  | n + 1 =>
-    simp [BitVec.msb_eq_decide] at p
-    simp only [Nat.add_sub_cancel]
-    exact p
-
 /-! ### cast -/
 
 @[simp, bv_toNat] theorem toNat_cast (h : w = v) (x : BitVec w) : (cast h x).toNat = x.toNat := rfl
@@ -177,53 +163,6 @@ theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat
 @[simp] theorem msb_cast (h : w = v) (x : BitVec w) : (cast h x).msb = x.msb := by
   simp [BitVec.msb]
 
-/-! ### toInt/ofInt -/
-
-/-- Prove equality of bitvectors in terms of nat operations. -/
-theorem toInt_eq_toNat_cond (i : BitVec n) :
-    i.toInt =
-      if 2*i.toNat < 2^n then
-        (i.toNat : Int)
-      else
-        (i.toNat : Int) - (2^n : Nat) := by
-  unfold BitVec.toInt
-  split <;> omega
-
-theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := by
-  simp only [toInt_eq_toNat_cond]
-  split
-  case inl g =>
-    rw [Int.bmod_pos] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
-    omega
-  case inr g =>
-    rw [Int.bmod_neg] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
-    omega
-
-/-- Prove equality of bitvectors in terms of nat operations. -/
-theorem eq_of_toInt_eq {i j : BitVec n} : i.toInt = j.toInt → i = j := by
-  intro eq
-  simp [toInt_eq_toNat_cond] at eq
-  apply eq_of_toNat_eq
-  revert eq
-  have _ilt := i.isLt
-  have _jlt := j.isLt
-  split <;> split <;> omega
-
-@[simp] theorem toNat_ofInt {n : Nat} (i : Int) :
-  (BitVec.ofInt n i).toNat = (i % (2^n : Nat)).toNat := by
-  unfold BitVec.ofInt
-  simp
-
-theorem toInt_ofNat {n : Nat} (x : Nat) :
-  (BitVec.ofNat n x).toInt = (x : Int).bmod (2^n) := by
-  simp [toInt_eq_toNat_bmod]
-
-@[simp] theorem toInt_ofInt {n : Nat} (i : Int) :
-  (BitVec.ofInt n i).toInt = i.bmod (2^n) := by
-  have _ := Nat.two_pow_pos n
-  have p : 0 ≤ i % (2^n : Nat) := by omega
-  simp [toInt_eq_toNat_bmod, Int.toNat_of_nonneg p]
-
 /-! ### zeroExtend and truncate -/
 
 @[simp, bv_toNat] theorem toNat_zeroExtend' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
@@ -259,24 +198,6 @@ theorem toInt_ofNat {n : Nat} (x : Nat) :
   apply eq_of_toNat_eq
   simp
 
-/-- Moves one-sided left toNat equality to BitVec equality. -/
-theorem toNat_eq_nat (x : BitVec w) (y : Nat)
-  : (x.toNat = y) ↔ (y < 2^w ∧ (x = y#w)) := by
-  apply Iff.intro
-  · intro eq
-    simp at eq
-    have lt := x.isLt
-    simp [eq] at lt
-    simp [←eq, lt, x.isLt]
-  · intro eq
-    simp [Nat.mod_eq_of_lt, eq]
-
-/-- Moves one-sided right toNat equality to BitVec equality. -/
-theorem nat_eq_toNat (x : BitVec w) (y : Nat)
-  : (y = x.toNat) ↔ (y < 2^w ∧ (x = y#w)) := by
-  rw [@eq_comm _ _ x.toNat]
-  apply toNat_eq_nat
-
 @[simp] theorem getLsb_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
     getLsb (zeroExtend' ge x) i = getLsb x i := by
   simp [getLsb, toNat_zeroExtend']
@@ -678,18 +599,4 @@ protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x
   simp
   exact Nat.lt_of_le_of_ne
 
-/- ! ### intMax -/
-
-/-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/
-def intMax (w : Nat) : BitVec w  := (2^w - 1)#w
-
-theorem getLsb_intMax_eq (w : Nat) : (intMax w).getLsb i = decide (i < w) := by
-  simp [intMax, getLsb]
-
-theorem toNat_intMax_eq : (intMax w).toNat = 2^w - 1 := by
-  have h : 2^w - 1 < 2^w := by
-    have pos : 2^w > 0 := Nat.pow_pos (by decide)
-    omega
-  simp [intMax, Nat.shiftLeft_eq, Nat.one_mul, natCast_eq_ofNat, toNat_ofNat, Nat.mod_eq_of_lt h]
-
 end BitVec

src/Init/Data/Int/DivMod.lean

@@ -158,44 +158,4 @@ instance : Div Int where
 instance : Mod Int where
   mod := Int.emod
 
-/-!
-# `bmod` ("balanced" mod)
-
-Balanced mod (and balanced div) are a division and modulus pair such
-that `b * (Int.bdiv a b) + Int.bmod a b = a` and `b/2 ≤ Int.bmod a b <
-b/2` for all `a : Int` and `b > 0`.
-
-This is used in Omega as well as signed bitvectors.
--/
-
-/--
-Balanced modulus.  This version of Integer modulus uses the
-balanced rounding convention, which guarantees that
-`m/2 ≤ bmod x m < m/2` for `m ≠ 0` and `bmod x m` is congruent
-to `x` modulo `m`.
-
-If `m = 0`, then `bmod x m = x`.
--/
-def bmod (x : Int) (m : Nat) : Int :=
-  let r := x % m
-  if r < (m + 1) / 2 then
-    r
-  else
-    r - m
-
-/--
-Balanced division.  This returns the unique integer so that
-`b * (Int.bdiv a b) + Int.bmod a b = a`.
--/
-def bdiv (x : Int) (m : Nat) : Int :=
-  if m = 0 then
-    0
-  else
-    let q := x / m
-    let r := x % m
-    if r < (m + 1) / 2 then
-      q
-    else
-      q + 1
-
 end Int

src/Init/Data/Int/DivModLemmas.lean

@@ -325,78 +325,23 @@ theorem sub_ediv_of_dvd (a : Int) {b c : Int}
   rw [Int.sub_eq_add_neg, Int.sub_eq_add_neg, Int.add_ediv_of_dvd_right (Int.dvd_neg.2 hcb)]
   congr; exact Int.neg_ediv_of_dvd hcb
 
-@[simp] theorem ediv_one : ∀ a : Int, a / 1 = a
-  | (_:Nat) => congrArg Nat.cast (Nat.div_one _)
-  | -[_+1]  => congrArg negSucc (Nat.div_one _)
+/-!
+# `bmod` ("balanced" mod)
 
-@[simp] theorem emod_one (a : Int) : a % 1 = 0 := by
-  simp [emod_def, Int.one_mul, Int.sub_self]
+We use balanced mod in the omega algorithm,
+to make ±1 coefficients appear in equations without them.
+-/
 
-@[simp] protected theorem ediv_self {a : Int} (H : a ≠ 0) : a / a = 1 := by
-  have := Int.mul_ediv_cancel 1 H; rwa [Int.one_mul] at this
-
-@[simp]
-theorem Int.emod_sub_cancel (x y : Int): (x - y)%y = x%y := by
-  if h : y = 0 then
-    simp [h]
+/--
+Balanced mod, taking values in the range [- m/2, (m - 1)/2].
+-/
+def bmod (x : Int) (m : Nat) : Int :=
+  let r := x % m
+  if r < (m + 1) / 2 then
+    r
   else
-    simp only [Int.emod_def, Int.sub_ediv_of_dvd, Int.dvd_refl, Int.ediv_self h, Int.mul_sub]
-    simp [Int.mul_one, Int.sub_sub, Int.add_comm y]
-
-/-! bmod -/
+    r - m
 
 @[simp] theorem bmod_emod : bmod x m % m = x % m := by
   dsimp [bmod]
   split <;> simp [Int.sub_emod]
-
-@[simp]
-theorem emod_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n) n = Int.bmod x n := by
-  simp [bmod, Int.emod_emod]
-
-theorem bmod_def (x : Int) (m : Nat) : bmod x m =
-  if (x % m) < (m + 1) / 2 then
-    x % m
-  else
-    (x % m) - m :=
-  rfl
-
-theorem bmod_pos (x : Int) (m : Nat) (p : x % m < (m + 1) / 2) : bmod x m = x % m := by
-  simp [bmod_def, p]
-
-theorem bmod_neg (x : Int) (m : Nat) (p : x % m ≥ (m + 1) / 2) : bmod x m = (x % m) - m := by
-  simp [bmod_def, Int.not_lt.mpr p]
-
-@[simp]
-theorem bmod_one_is_zero (x : Int) : Int.bmod x 1 = 0 := by
-  simp [Int.bmod]
-
-@[simp]
-theorem bmod_add_cancel (x : Int) (n : Nat) : Int.bmod (x + n) n = Int.bmod x n := by
-  simp [bmod_def]
-
-@[simp]
-theorem bmod_add_mul_cancel (x : Int) (n : Nat) (k : Int) : Int.bmod (x + n * k) n = Int.bmod x n := by
-  simp [bmod_def]
-
-@[simp]
-theorem bmod_sub_cancel (x : Int) (n : Nat) : Int.bmod (x - n) n = Int.bmod x n := by
-  simp [bmod_def]
-
-@[simp]
-theorem emod_add_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n + y) n = Int.bmod (x + y) n := by
-  simp [Int.emod_def, Int.sub_eq_add_neg]
-  rw [←Int.mul_neg, Int.add_right_comm,  Int.bmod_add_mul_cancel]
-
-@[simp]
-theorem bmod_add_bmod_congr : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n := by
-  rw [bmod_def x n]
-  split
-  case inl p =>
-    simp
-  case inr p =>
-    rw [Int.sub_eq_add_neg, Int.add_right_comm, ←Int.sub_eq_add_neg]
-    simp
-
-@[simp]
-theorem add_bmod_bmod : Int.bmod (x + Int.bmod y n) n = Int.bmod (x + y) n := by
-  rw [Int.add_comm x, Int.bmod_add_bmod_congr, Int.add_comm y]

src/Init/Data/Int/Lemmas.lean

@@ -321,27 +321,6 @@ theorem toNat_sub (m n : Nat) : toNat (m - n) = m - n := by
   · exact (Nat.add_sub_cancel_left ..).symm
   · dsimp; rw [Nat.add_assoc, Nat.sub_eq_zero_of_le (Nat.le_add_right ..)]; rfl
 
-/- ## add/sub injectivity -/
-
-@[simp]
-protected theorem add_right_inj (i j k : Int) : (i + k = j + k) ↔ i = j := by
-  apply Iff.intro
-  · intro p
-    rw [←Int.add_sub_cancel i k, ←Int.add_sub_cancel j k, p]
-  · exact congrArg (· + k)
-
-@[simp]
-protected theorem add_left_inj (i j k : Int) : (k + i = k + j) ↔ i = j := by
-  simp [Int.add_comm k]
-
-@[simp]
-protected theorem sub_left_inj (i j k : Int) : (k - i = k - j) ↔ i = j := by
-  simp [Int.sub_eq_add_neg, Int.neg_inj]
-
-@[simp]
-protected theorem sub_right_inj (i j k : Int) : (i - k = j - k) ↔ i = j := by
-  simp [Int.sub_eq_add_neg]
-
 /- ## Ring properties -/
 
 @[simp] theorem ofNat_mul_negSucc (m n : Nat) : (m : Int) * -[n+1] = -↑(m * succ n) := rfl
@@ -499,33 +478,10 @@ theorem eq_one_of_mul_eq_self_left {a b : Int} (Hpos : a ≠ 0) (H : b * a = a)
 theorem eq_one_of_mul_eq_self_right {a b : Int} (Hpos : b ≠ 0) (H : b * a = b) : a = 1 :=
   Int.eq_of_mul_eq_mul_left Hpos <| by rw [Int.mul_one, H]
 
-/-! # pow -/
-
-protected theorem pow_zero (b : Int) : b^0 = 1 := rfl
-
 protected theorem pow_succ (b : Int) (e : Nat) : b ^ (e+1) = (b ^ e) * b := rfl
 protected theorem pow_succ' (b : Int) (e : Nat) : b ^ (e+1) = b * (b ^ e) := by
   rw [Int.mul_comm, Int.pow_succ]
 
-theorem pow_le_pow_of_le_left {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i
-  | 0      => Nat.le_refl _
-  | succ i => Nat.mul_le_mul (pow_le_pow_of_le_left h i) h
-
-theorem pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤ j → n^i ≤ n^j
-  | 0,      h =>
-    have : i = 0 := eq_zero_of_le_zero h
-    this.symm ▸ Nat.le_refl _
-  | succ j, h =>
-    match le_or_eq_of_le_succ h with
-    | Or.inl h => show n^i ≤ n^j * n from
-      have : n^i * 1 ≤ n^j * n := Nat.mul_le_mul (pow_le_pow_of_le_right hx h) hx
-      Nat.mul_one (n^i) ▸ this
-    | Or.inr h =>
-      h.symm ▸ Nat.le_refl _
-
-theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
-  pow_le_pow_of_le_right h (Nat.zero_le _)
-
 /-! NatCast lemmas -/
 
 /-!
@@ -545,10 +501,4 @@ theorem natCast_one : ((1 : Nat) : Int) = (1 : Int) := rfl
 @[simp] theorem natCast_mul (a b : Nat) : ((a * b : Nat) : Int) = (a : Int) * (b : Int) := by
   simp
 
-theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by
-  match n with
-  | 0 => rfl
-  | n + 1 =>
-    simp only [Nat.pow_succ, Int.pow_succ, natCast_mul, natCast_pow _ n]
-
 end Int

src/Init/Data/Int/Order.lean

@@ -192,11 +192,6 @@ protected theorem min_le_right (a b : Int) : min a b ≤ b := by rw [Int.min_def
 
 protected theorem min_le_left (a b : Int) : min a b ≤ a := Int.min_comm .. ▸ Int.min_le_right ..
 
-protected theorem min_eq_left {a b : Int} (h : a ≤ b) : min a b = a := by simp [Int.min_def, h]
-
-protected theorem min_eq_right {a b : Int} (h : b ≤ a) : min a b = b := by
-  rw [Int.min_comm a b]; exact Int.min_eq_left h
-
 protected theorem le_min {a b c : Int} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c :=
   ⟨fun h => ⟨Int.le_trans h (Int.min_le_left ..), Int.le_trans h (Int.min_le_right ..)⟩,
    fun ⟨h₁, h₂⟩ => by rw [Int.min_def]; split <;> assumption⟩
@@ -215,12 +210,6 @@ protected theorem max_le {a b c : Int} : max a b ≤ c ↔ a ≤ c ∧ b ≤ c :
   ⟨fun h => ⟨Int.le_trans (Int.le_max_left ..) h, Int.le_trans (Int.le_max_right ..) h⟩,
    fun ⟨h₁, h₂⟩ => by rw [Int.max_def]; split <;> assumption⟩
 
-protected theorem max_eq_right {a b : Int} (h : a ≤ b) : max a b = b := by
-  simp [Int.max_def, h, Int.not_lt.2 h]
-
-protected theorem max_eq_left {a b : Int} (h : b ≤ a) : max a b = a := by
-  rw [← Int.max_comm b a]; exact Int.max_eq_right h
-
 theorem eq_natAbs_of_zero_le {a : Int} (h : 0 ≤ a) : a = natAbs a := by
   let ⟨n, e⟩ := eq_ofNat_of_zero_le h
   rw [e]; rfl
@@ -447,54 +436,3 @@ theorem natAbs_of_nonneg {a : Int} (H : 0 ≤ a) : (natAbs a : Int) = a :=
 
 theorem ofNat_natAbs_of_nonpos {a : Int} (H : a ≤ 0) : (natAbs a : Int) = -a := by
   rw [← natAbs_neg, natAbs_of_nonneg (Int.neg_nonneg_of_nonpos H)]
-
-/-! ### toNat -/
-
-theorem toNat_eq_max : ∀ a : Int, (toNat a : Int) = max a 0
-  | (n : Nat) => (Int.max_eq_left (ofNat_zero_le n)).symm
-  | -[n+1] => (Int.max_eq_right (Int.le_of_lt (negSucc_lt_zero n))).symm
-
-@[simp] theorem toNat_zero : (0 : Int).toNat = 0 := rfl
-
-@[simp] theorem toNat_one : (1 : Int).toNat = 1 := rfl
-
-@[simp] theorem toNat_of_nonneg {a : Int} (h : 0 ≤ a) : (toNat a : Int) = a := by
-  rw [toNat_eq_max, Int.max_eq_left h]
-
-@[simp] theorem toNat_ofNat (n : Nat) : toNat ↑n = n := rfl
-
-@[simp] theorem toNat_ofNat_add_one {n : Nat} : ((n : Int) + 1).toNat = n + 1 := rfl
-
-theorem self_le_toNat (a : Int) : a ≤ toNat a := by rw [toNat_eq_max]; apply Int.le_max_left
-
-@[simp] theorem le_toNat {n : Nat} {z : Int} (h : 0 ≤ z) : n ≤ z.toNat ↔ (n : Int) ≤ z := by
-  rw [← Int.ofNat_le, Int.toNat_of_nonneg h]
-
-@[simp] theorem toNat_lt {n : Nat} {z : Int} (h : 0 ≤ z) : z.toNat < n ↔ z < (n : Int) := by
-  rw [← Int.not_le, ← Nat.not_le, Int.le_toNat h]
-
-theorem toNat_add {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : (a + b).toNat = a.toNat + b.toNat :=
-  match a, b, eq_ofNat_of_zero_le ha, eq_ofNat_of_zero_le hb with
-  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => rfl
-
-theorem toNat_add_nat {a : Int} (ha : 0 ≤ a) (n : Nat) : (a + n).toNat = a.toNat + n :=
-  match a, eq_ofNat_of_zero_le ha with | _, ⟨_, rfl⟩ => rfl
-
-@[simp] theorem pred_toNat : ∀ i : Int, (i - 1).toNat = i.toNat - 1
-  | 0 => rfl
-  | (n+1:Nat) => by simp [ofNat_add]
-  | -[n+1] => rfl
-
-@[simp] theorem toNat_sub_toNat_neg : ∀ n : Int, ↑n.toNat - ↑(-n).toNat = n
-  | 0 => rfl
-  | (_+1:Nat) => Int.sub_zero _
-  | -[_+1] => Int.zero_sub _
-
-@[simp] theorem toNat_add_toNat_neg_eq_natAbs : ∀ n : Int, n.toNat + (-n).toNat = n.natAbs
-  | 0 => rfl
-  | (_+1:Nat) => Nat.add_zero _
-  | -[_+1] => Nat.zero_add _
-
-@[simp] theorem toNat_neg_nat : ∀ n : Nat, (-(n : Int)).toNat = 0
-  | 0 => rfl
-  | _+1 => rfl

src/Init/Data/List/BasicAux.lean

@@ -227,23 +227,4 @@ where
     else
       go xs acc₁ (acc₂.push x)
 
-/--
-Given a function `f : α → β ⊕ γ`, `partitionMap f l` maps the list by `f`
-whilst partitioning the result it into a pair of lists, `List β × List γ`,
-partitioning the `.inl _` into the left list, and the `.inr _` into the right List.
-```
-partitionMap (id : Nat ⊕ Nat → Nat ⊕ Nat) [inl 0, inr 1, inl 2] = ([0, 2], [1])
-```
--/
-@[inline] def partitionMap (f : α → β ⊕ γ) (l : List α) : List β × List γ := go l #[] #[] where
-  /-- Auxiliary for `partitionMap`:
-  `partitionMap.go f l acc₁ acc₂ = (acc₁.toList ++ left, acc₂.toList ++ right)`
-  if `partitionMap f l = (left, right)`. -/
-  @[specialize] go : List α → Array β → Array γ → List β × List γ
-  | [], acc₁, acc₂ => (acc₁.toList, acc₂.toList)
-  | x :: xs, acc₁, acc₂ =>
-    match f x with
-    | .inl a => go xs (acc₁.push a) acc₂
-    | .inr b => go xs acc₁ (acc₂.push b)
-
 end List

src/Init/Data/List/Lemmas.lean

@@ -665,44 +665,3 @@ theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·
     exact congrArg some <| anti.1
       ((le_minimum?_iff le_min_iff (xs := x::xs) rfl _).1 (le_refl _) _ h₁)
       (h₂ _ (minimum?_mem min_eq_or (xs := x::xs) rfl))
-
-@[simp] theorem get_cons_succ {as : List α} {h : i + 1 < (a :: as).length} :
-  (a :: as).get ⟨i+1, h⟩ = as.get ⟨i, Nat.lt_of_succ_lt_succ h⟩ := rfl
-
-@[simp] theorem get_cons_succ' {as : List α} {i : Fin as.length} :
-  (a :: as).get i.succ = as.get i := rfl
-
-@[simp] theorem set_nil (n : Nat) (a : α) : [].set n a = [] := rfl
-
-@[simp] theorem set_zero (x : α) (xs : List α) (a : α) :
-  (x :: xs).set 0 a = a :: xs := rfl
-
-@[simp] theorem set_succ (x : α) (xs : List α) (n : Nat) (a : α) :
-  (x :: xs).set n.succ a = x :: xs.set n a := rfl
-
-@[simp] theorem get_set_eq (l : List α) (i : Nat) (a : α) (h : i < (l.set i a).length) :
-    (l.set i a).get ⟨i, h⟩ = a :=
-  match l, i with
-  | [], _ => by
-    simp at h
-    contradiction
-  | _ :: _, 0 => by
-    simp
-  | _ :: l, i + 1 => by
-    simp [get_set_eq l]
-
-@[simp] 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⟩ :=
-  match l, i, j with
-  | [], _, _ => by
-    simp
-  | _ :: _, 0, 0 => by
-    contradiction
-  | _ :: _, 0, _ + 1 => by
-    simp
-  | _ :: _, _ + 1, 0 => by
-    simp
-  | _ :: l, i + 1, j + 1 => by
-    have g : i ≠ j := h ∘ congrArg (· + 1)
-    simp [get_set_ne l g]

src/Init/Data/Nat/Basic.lean

@@ -189,7 +189,7 @@ protected theorem mul_comm : ∀ (n m : Nat), n * m = m * n
   Nat.mul_comm n 1 ▸ Nat.mul_one n
 
 protected theorem left_distrib (n m k : Nat) : n * (m + k) = n * m + n * k := by
-  induction n with
+  induction n generalizing m k with
   | zero      => repeat rw [Nat.zero_mul]
   | succ n ih => simp [succ_mul, ih]; rw [Nat.add_assoc, Nat.add_assoc (n*m)]; apply congrArg; apply Nat.add_left_comm
 
@@ -503,10 +503,10 @@ theorem eq_of_mul_eq_mul_right {n m k : Nat} (hm : 0 < m) (h : n * m = k * m) :
 
 /-! # power -/
 
-protected theorem pow_succ (n m : Nat) : n^(succ m) = n^m * n :=
+theorem pow_succ (n m : Nat) : n^(succ m) = n^m * n :=
   rfl
 
-protected theorem pow_zero (n : Nat) : n^0 = 1 := rfl
+theorem pow_zero (n : Nat) : n^0 = 1 := rfl
 
 theorem pow_le_pow_of_le_left {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i
   | 0      => Nat.le_refl _

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -239,7 +239,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
     rw [Nat.sub_eq_zero_iff_le] at i_sub_j_eq
     exact Nat.not_le_of_gt j_lt_i i_sub_j_eq
   | d+1 =>
-    simp [Nat.pow_succ, Nat.mul_comm _ 2,  Nat.mul_add_mod]
+    simp [pow_succ, Nat.mul_comm _ 2,  Nat.mul_add_mod]
 
 @[simp] theorem testBit_mod_two_pow (x j i : Nat) :
     testBit (x % 2^j) i = (decide (i < j) && testBit x i) := by
@@ -287,7 +287,7 @@ theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
     simp only [testBit_succ]
     match n with
     | 0 =>
-      simp only [Nat.pow_zero, succ_sub_succ_eq_sub, Nat.zero_sub, Nat.zero_div, zero_testBit]
+      simp only [pow_zero, succ_sub_succ_eq_sub, Nat.zero_sub, Nat.zero_div, zero_testBit]
       rw [decide_eq_false] <;> simp
     | n+1 =>
       rw [Nat.two_pow_succ_sub_succ_div_two, ih]
@@ -352,7 +352,7 @@ private theorem eq_0_of_lt (x : Nat) : x < 2^ 0 ↔ x = 0 := eq_0_of_lt_one x
 private theorem zero_lt_pow (n : Nat) : 0 < 2^n := by
   induction n
   case zero => simp [eq_0_of_lt]
-  case succ n hyp => simpa [Nat.pow_succ]
+  case succ n hyp => simpa [pow_succ]
 
 private theorem div_two_le_of_lt_two {m n : Nat} (p : m < 2 ^ succ n) : m / 2 < 2^n := by
   simp [div_lt_iff_lt_mul Nat.zero_lt_two]
@@ -377,7 +377,7 @@ theorem bitwise_lt_two_pow (left : x < 2^n) (right : y < 2^n) : (Nat.bitwise f x
       simp only [x_zero, y_zero, if_neg]
       have hyp1 := hyp (div_two_le_of_lt_two left) (div_two_le_of_lt_two right)
       by_cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) = true <;>
-        simp [p, Nat.pow_succ, mul_succ, Nat.add_assoc]
+        simp [p, pow_succ, mul_succ, Nat.add_assoc]
       case pos =>
         apply lt_of_succ_le
         simp only [← Nat.succ_add]

src/Init/Data/Nat/Lemmas.lean

@@ -742,7 +742,7 @@ theorem shiftLeft_eq (a b : Nat) : a <<< b = a * 2 ^ b :=
   match b with
   | 0 => (Nat.mul_one _).symm
   | b+1 => (shiftLeft_eq _ b).trans <| by
-    simp [Nat.pow_succ, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]
+    simp [pow_succ, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]
 
 theorem one_shiftLeft (n : Nat) : 1 <<< n = 2 ^ n := by rw [shiftLeft_eq, Nat.one_mul]
 

src/Init/Meta.lean

@@ -1362,19 +1362,6 @@ structure OmegaConfig where
 
 end Omega
 
-namespace CheckTactic
-
-/--
-Type used to lift an arbitrary value into a type parameter so it can
-appear in a proof goal.
-
-It is used by the #check_tactic command.
--/
-inductive CheckGoalType {α : Sort u} : (val : α) → Prop where
-| intro : (val : α) → CheckGoalType val
-
-end CheckTactic
-
 end Meta
 
 namespace Parser

src/Init/Notation.lean

@@ -503,25 +503,6 @@ applications of this function as `↑` when printing expressions.
 -/
 syntax (name := Attr.coe) "coe" : attr
 
-/--
-This attribute marks a code action, which is used to suggest new tactics or replace existing ones.
-
-* `@[command_code_action kind]`: This is a code action which applies to applications of the command
-  `kind` (a command syntax kind), which can replace the command or insert things before or after it.
-
-* `@[command_code_action kind₁ kind₂]`: shorthand for
-  `@[command_code_action kind₁, command_code_action kind₂]`.
-
-* `@[command_code_action]`: This is a command code action that applies to all commands.
-  Use sparingly.
--/
-syntax (name := command_code_action) "command_code_action" (ppSpace ident)* : attr
-
-/--
-Builtin command code action. See `command_code_action`.
--/
-syntax (name := builtin_command_code_action) "builtin_command_code_action" (ppSpace ident)* : attr
-
 /--
 When `parent_dir` contains the current Lean file, `include_str "path" / "to" / "file"` becomes
 a string literal with the contents of the file at `"parent_dir" / "path" / "to" / "file"`. If this
@@ -551,92 +532,3 @@ except that it doesn't print an empty diagnostic.
 (This is effectively a synonym for `run_elab`.)
 -/
 syntax (name := runMeta) "run_meta " doSeq : command
-
-/-- Element that can be part of a `#guard_msgs` specification. -/
-syntax guardMsgsSpecElt := &"drop"? (&"info" <|> &"warning" <|> &"error" <|> &"all")
-
-/-- Specification for `#guard_msgs` command. -/
-syntax guardMsgsSpec := "(" guardMsgsSpecElt,* ")"
-
-/--
-`#guard_msgs` captures the messages generated by another command and checks that they
-match the contents of the docstring attached to the `#guard_msgs` command.
-
-Basic example:
-```lean
-/--
-error: unknown identifier 'x'
--/
-#guard_msgs in
-example : α := x
-```
-This checks that there is such an error and then consumes the message entirely.
-
-By default, the command intercepts all messages, but there is a way to specify which types
-of messages to consider. For example, we can select only warnings:
-```lean
-/--
-warning: declaration uses 'sorry'
--/
-#guard_msgs(warning) in
-example : α := sorry
-```
-or only errors
-```lean
-#guard_msgs(error) in
-example : α := sorry
-```
-In this last example, since the message is not intercepted there is a warning on `sorry`.
-We can drop the warning completely with
-```lean
-#guard_msgs(error, drop warning) in
-example : α := sorry
-```
-
-Syntax description:
-```
-#guard_msgs (drop? info|warning|error|all,*)? in cmd
-```
-
-If there is no specification, `#guard_msgs` intercepts all messages.
-Otherwise, if there is one, the specification is considered in left-to-right order, and the first
-that applies chooses the outcome of the message:
-- `info`, `warning`, `error`: intercept a message with the given severity level.
-- `all`: intercept any message (so `#guard_msgs in cmd` and `#guard_msgs (all) in cmd`
-  are equivalent).
-- `drop info`, `drop warning`, `drop error`: intercept a message with the given severity
-  level and then drop it. These messages are not checked.
-- `drop all`: intercept a message and drop it.
-
-For example, `#guard_msgs (error, drop all) in cmd` means to check warnings and then drop
-everything else.
--/
-syntax (name := guardMsgsCmd)
-  (docComment)? "#guard_msgs" (ppSpace guardMsgsSpec)? " in" ppLine command : command
-
-namespace Parser
-
-/--
-`#check_tactic t ~> r by commands` runs the tactic sequence `commands`
-on a goal with `t` and sees if the resulting expression has reduced it
-to `r`.
--/
-syntax (name := checkTactic) "#check_tactic " term "~>" term "by" tactic : command
-
-/--
-`#check_tactic_failure t by tac` runs the tactic `tac`
-on a goal with `t` and verifies it fails.
--/
-syntax  (name := checkTacticFailure) "#check_tactic_failure " term "by" tactic : command
-
-/--
-`#check_simp t ~> r` checks `simp` reduces `t` to `r`.
--/
-syntax (name := checkSimp) "#check_simp " term "~>" term : command
-
-/--
-`#check_simp t !~>` checks `simp` fails on reducing `t`.
--/
-syntax (name := checkSimpFailure) "#check_simp " term "!~>" : command
-
-end Parser

src/Init/NotationExtra.lean

@@ -170,6 +170,19 @@ See [Theorem Proving in Lean 4][tpil4] for more information.
 -/
 syntax (name := calcTactic) "calc" calcSteps : tactic
 
+/--
+Denotes a term that was omitted by the pretty printer.
+This is only used for pretty printing, and it cannot be elaborated.
+The presence of `⋯` is controlled by the `pp.deepTerms` and `pp.proofs` options.
+-/
+syntax "⋯" : term
+
+macro_rules | `(⋯) => Macro.throwError "\
+  Error: The '⋯' token is used by the pretty printer to indicate omitted terms, \
+  and it cannot be elaborated.\
+  \n\nIts presence in pretty printing output is controlled by the 'pp.deepTerms' and `pp.proofs` options. \
+  These options can be further adjusted using `pp.deepTerms.threshold` and `pp.proofs.threshold`."
+
 @[app_unexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `(())
 
@@ -453,19 +466,3 @@ syntax "{" term,+ "}" : term
 macro_rules
   | `({$x:term}) => `(singleton $x)
   | `({$x:term, $xs:term,*}) => `(insert $x {$xs:term,*})
-
-namespace Lean
-
-/-- Unexpander for the `{ x }` notation. -/
-@[app_unexpander singleton]
-def singletonUnexpander : Lean.PrettyPrinter.Unexpander
-  | `($_ $a) => `({ $a:term })
-  | _ => throw ()
-
-/-- Unexpander for the `{ x, y, ... }` notation. -/
-@[app_unexpander insert]
-def insertUnexpander : Lean.PrettyPrinter.Unexpander
-  | `($_ $a { $ts:term,* }) => `({$a:term, $ts,*})
-  | _ => throw ()
-
-end Lean

src/Init/Prelude.lean

@@ -947,8 +947,7 @@ return `t` or `e` depending on whether `c` is true or false. The explicit argume
 determines how to evaluate `c` to true or false. Write `if h : c then t else e`
 instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
 that `c` is true/false.
--/
-/-
+
 Because Lean uses a strict (call-by-value) evaluation strategy, the signature of this
 function is problematic in that it would require `t` and `e` to be evaluated before
 calling the `ite` function, which would cause both sides of the `if` to be evaluated.

src/Init/Tactics.lean

@@ -1306,26 +1306,6 @@ used when closing the goal.
 -/
 syntax (name := apply?) "apply?" (" using " (colGt term),+)? : tactic
 
-/--
-`show_term tac` runs `tac`, then prints the generated term in the form
-"exact X Y Z" or "refine X ?_ Z" if there are remaining subgoals.
-
-(For some tactics, the printed term will not be human readable.)
--/
-syntax (name := showTerm) "show_term " tacticSeq : tactic
-
-/--
-`show_term e` elaborates `e`, then prints the generated term.
--/
-macro (name := showTermElab) tk:"show_term " t:term : term =>
-  `(term| no_implicit_lambda% (show_term_elab%$tk $t))
-
-/--
-The command `by?` will print a suggestion for replacing the proof block with a proof term
-using `show_term`.
--/
-macro (name := by?) tk:"by?" t:tacticSeq : term => `(show_term%$tk by%$tk $t)
-
 end Tactic
 
 namespace Attr
@@ -1445,14 +1425,13 @@ macro_rules | `(‹$type›) => `((by assumption : $type))
 by the notation `arr[i]` to prove any side conditions that arise when
 constructing the term (e.g. the index is in bounds of the array).
 The default behavior is to just try `trivial` (which handles the case
-where `i < arr.size` is in the context) and `simp_arith` and `omega`
+where `i < arr.size` is in the context) and `simp_arith`
 (for doing linear arithmetic in the index).
 -/
 syntax "get_elem_tactic_trivial" : tactic
 
-macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| omega)
-macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp (config := { arith := true }); done)
 macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| trivial)
+macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp (config := { arith := true }); done)
 
 /--
 `get_elem_tactic` is the tactic automatically called by the notation `arr[i]`
@@ -1463,24 +1442,6 @@ users are encouraged to extend `get_elem_tactic_trivial` instead of this tactic.
 -/
 macro "get_elem_tactic" : tactic =>
   `(tactic| first
-      /-
-      Recall that `macro_rules` are tried in reverse order.
-      We want `assumption` to be tried first.
-      This is important for theorems such as
-      ```
-      [simp] theorem getElem_pop (a : Array α) (i : Nat) (hi : i < a.pop.size) :
-      a.pop[i] = a[i]'(Nat.lt_of_lt_of_le (a.size_pop ▸ hi) (Nat.sub_le _ _)) :=
-      ```
-      There is a proof embedded in the right-hand-side, and we want it to be just `hi`.
-      If `omega` is used to "fill" this proof, we will have a more complex proof term that
-      cannot be inferred by unification.
-      We hardcoded `assumption` here to ensure users cannot accidentaly break this IF
-      they add new `macro_rules` for `get_elem_tactic_trivial`.
-
-      TODO: Implement priorities for `macro_rules`.
-      TODO: Ensure we have a **high-priority** macro_rules for `get_elem_tactic_trivial` which is just `assumption`.
-      -/
-    | assumption
     | get_elem_tactic_trivial
     | fail "failed to prove index is valid, possible solutions:
   - Use `have`-expressions to prove the index is valid

src/Init/WFTactics.lean

@@ -22,8 +22,7 @@ macro_rules | `(tactic| decreasing_trivial) => `(tactic| linarith)
 -/
 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| (simp (config := { arith := true, failIfUnchanged := false })); done)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| assumption)
 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

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.ProjFns
-import Lean.Meta.CtorRecognizer
 import Lean.Compiler.BorrowedAnnotation
 import Lean.Compiler.LCNF.Types
 import Lean.Compiler.LCNF.Bind
@@ -620,7 +619,7 @@ where
       let rhs ← liftMetaM do Meta.whnf args[inductVal.numParams + inductVal.numIndices + 2]!
       let lhs := lhs.toCtorIfLit
       let rhs := rhs.toCtorIfLit
-      match (← liftMetaM <| Meta.isConstructorApp? lhs), (← liftMetaM <| Meta.isConstructorApp? rhs) with
+      match lhs.isConstructorApp? (← getEnv), rhs.isConstructorApp? (← getEnv) with
       | some lhsCtorVal, some rhsCtorVal =>
         if lhsCtorVal.name == rhsCtorVal.name then
           etaIfUnderApplied e (arity+1) do

src/Lean/Data/Json/Basic.lean

@@ -8,7 +8,6 @@ prelude
 import Init.Data.List.Control
 import Init.Data.Range
 import Init.Data.OfScientific
-import Init.Data.Hashable
 import Lean.Data.RBMap
 namespace Lean
 
@@ -16,7 +15,7 @@ namespace Lean
 structure JsonNumber where
   mantissa : Int
   exponent : Nat
-  deriving DecidableEq, Hashable
+  deriving DecidableEq
 
 namespace JsonNumber
 
@@ -206,19 +205,6 @@ private partial def beq' : Json → Json → Bool
 instance : BEq Json where
   beq := beq'
 
-private partial def hash' : Json → UInt64
-  | null   => 11
-  | bool b => mixHash 13 <| hash b
-  | num n  => mixHash 17 <| hash n
-  | str s  => mixHash 19 <| hash s
-  | arr elems =>
-    mixHash 23 <| elems.foldl (init := 7) fun r a => mixHash r (hash' a)
-  | obj kvPairs =>
-    mixHash 29 <| kvPairs.fold (init := 7) fun r k v => mixHash r <| mixHash (hash k) (hash' v)
-
-instance : Hashable Json where
-  hash := hash'
-
 -- HACK(Marc): temporary ugliness until we can use RBMap for JSON objects
 def mkObj (o : List (String × Json)) : Json :=
   obj <| Id.run do

src/Lean/Data/Lsp/LanguageFeatures.lean

@@ -47,19 +47,19 @@ structure CompletionItem where
   documentation? : Option MarkupContent := none
   kind?          : Option CompletionItemKind := none
   textEdit?      : Option InsertReplaceEdit := none
-  sortText?      : Option String := none
-  data?          : Option Json := none
   /-
   tags? : CompletionItemTag[]
   deprecated? : boolean
   preselect? : boolean
+  sortText? : string
   filterText? : string
   insertText? : string
   insertTextFormat? : InsertTextFormat
   insertTextMode? : InsertTextMode
   additionalTextEdits? : TextEdit[]
   commitCharacters? : string[]
-  command? : Command -/
+  command? : Command
+  data? : any -/
   deriving FromJson, ToJson, Inhabited
 
 structure CompletionList where
@@ -274,7 +274,7 @@ structure CallHierarchyItem where
   uri            : DocumentUri
   range          : Range
   selectionRange : Range
-  data?          : Option Json := none
+  -- data? : Option unknown
   deriving FromJson, ToJson, BEq, Hashable, Inhabited
 
 structure CallHierarchyIncomingCallsParams where

src/Lean/Data/Lsp/Utf16.lean

@@ -86,10 +86,6 @@ def leanPosToLspPos (text : FileMap) : Lean.Position → Lsp.Position
 def utf8PosToLspPos (text : FileMap) (pos : String.Pos) : Lsp.Position :=
   text.leanPosToLspPos (text.toPosition pos)
 
-/-- Gets the LSP range from a `String.Range`. -/
-def utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
-  { start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
-
 end FileMap
 end Lean
 

src/Lean/Elab.lean

@@ -47,6 +47,3 @@ import Lean.Elab.Eval
 import Lean.Elab.Calc
 import Lean.Elab.InheritDoc
 import Lean.Elab.ParseImportsFast
-import Lean.Elab.GuardMsgs
-import Lean.Elab.CheckTactic
-import Lean.Elab.MatchExpr

src/Lean/Elab/BuiltinCommand.lean

@@ -534,10 +534,10 @@ open Meta
 def elabCheckCore (ignoreStuckTC : Bool) : CommandElab
   | `(#check%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_check do
     -- show signature for `#check id`/`#check @id`
-    if let `($id:ident) := term then
+    if let `($_:ident) := term then
       try
         for c in (← resolveGlobalConstWithInfos term) do
-          addCompletionInfo <| .id term id.getId (danglingDot := false) {} none
+          addCompletionInfo <| .id term c (danglingDot := false) {} none
           logInfoAt tk <| .ofPPFormat { pp := fun
             | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature c
             | none     => return f!"{c}"  -- should never happen

src/Lean/Elab/BuiltinTerm.lean

@@ -99,14 +99,6 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
         else
           throwError "synthetic hole has already been defined with an incompatible local context"
 
-@[builtin_term_elab Lean.Parser.Term.omission] def elabOmission : TermElab := fun stx expectedType? => do
-  logWarning m!"\
-    The '⋯' token is used by the pretty printer to indicate omitted terms, and it should not be used directly. \
-    It logs this warning and then elaborates like `_`.\
-    \n\nThe presence of `⋯` in pretty printing output is controlled by the 'pp.deepTerms' and `pp.proofs` options. \
-    These options can be further adjusted using `pp.deepTerms.threshold` and `pp.proofs.threshold`."
-  elabHole stx expectedType?
-
 @[builtin_term_elab «letMVar»] def elabLetMVar : TermElab := fun stx expectedType? => do
   match stx with
   | `(let_mvar% ? $n := $e; $b) =>
@@ -166,10 +158,7 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
 @[builtin_term_elab noImplicitLambda] def elabNoImplicitLambda : TermElab := fun stx expectedType? =>
   elabTerm stx[1] (mkNoImplicitLambdaAnnotation <$> expectedType?)
 
-@[builtin_term_elab Lean.Parser.Term.cdot] def elabBadCDot : TermElab := fun stx expectedType? => do
-  if stx[0].getAtomVal == "." then
-    -- Users may input bad cdots because they are trying to auto-complete them using the expected type
-    addCompletionInfo <| CompletionInfo.dotId stx .anonymous (← getLCtx) expectedType?
+@[builtin_term_elab Lean.Parser.Term.cdot] def elabBadCDot : TermElab := fun _ _ =>
   throwError "invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)"
 
 @[builtin_term_elab str] def elabStrLit : TermElab := fun stx _ => do

src/Lean/Elab/CheckTactic.lean

@@ -1,95 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joe Hendrix
--/
-prelude
-import Lean.Elab.Tactic.ElabTerm
-import Lean.Elab.Command
-import Lean.Elab.Tactic.Meta
-
-/-!
-Commands to validate tactic results.
--/
-
-namespace Lean.Elab.CheckTactic
-
-open Lean.Meta CheckTactic
-open Lean.Elab.Tactic
-open Lean.Elab.Command
-
-private def matchCheckGoalType (stx : Syntax) (goalType : Expr) : MetaM (Expr × Expr × Level) := do
-  let u ← mkFreshLevelMVar
-  let type ← mkFreshExprMVar (some (.sort u))
-  let val  ← mkFreshExprMVar (some type)
-  let extType := mkAppN (.const ``CheckGoalType [u]) #[type, val]
-  if !(← isDefEq goalType extType) then
-    throwErrorAt stx "Goal{indentExpr goalType}\nis expected to match {indentExpr extType}"
-  pure (val, type, u)
-
-@[builtin_command_elab Lean.Parser.checkTactic]
-def elabCheckTactic : CommandElab := fun stx => do
-  let `(#check_tactic $t ~> $result by $tac) := stx | throwUnsupportedSyntax
-  withoutModifyingEnv $ do
-    runTermElabM $ fun _vars => do
-      let u ← Lean.Elab.Term.elabTerm t none
-      let type ← inferType u
-      let lvl ← mkFreshLevelMVar
-      let checkGoalType : Expr := mkApp2 (mkConst ``CheckGoalType [lvl]) type u
-      let mvar ← mkFreshExprMVar (.some checkGoalType)
-      let (goals, _) ← Lean.Elab.runTactic mvar.mvarId! tac.raw
-      let expTerm ← Lean.Elab.Term.elabTerm result (.some type)
-      match goals with
-      | [] =>
-        throwErrorAt stx
-          m!"{tac} closed goal, but is expected to reduce to {indentExpr expTerm}."
-      | [next] => do
-        let (val, _, _) ← matchCheckGoalType stx (←next.getType)
-        if !(← Meta.withReducible <| isDefEq val expTerm) then
-          throwErrorAt stx
-            m!"Term reduces to{indentExpr val}\nbut is expected to reduce to {indentExpr expTerm}"
-      | _ => do
-        throwErrorAt stx
-          m!"{tac} produced multiple goals, but is expected to reduce to {indentExpr expTerm}."
-      pure ()
-
-@[builtin_command_elab Lean.Parser.checkTacticFailure]
-def elabCheckTacticFailure : CommandElab := fun stx => do
-  let `(#check_tactic_failure $t by $tactic) := stx | throwUnsupportedSyntax
-  withoutModifyingEnv $ do
-    runTermElabM $ fun _vars => do
-      let val ← Lean.Elab.Term.elabTerm t none
-      let type ← inferType val
-      let lvl ← mkFreshLevelMVar
-      let checkGoalType : Expr := mkApp2 (mkConst ``CheckGoalType [lvl]) type val
-      let mvar ← mkFreshExprMVar (.some checkGoalType)
-      let act := Lean.Elab.runTactic mvar.mvarId! tactic.raw
-      match ← try (Term.withoutErrToSorry (some <$> act)) catch _ => pure none with
-        | none =>
-          pure ()
-        | some (gls, _) =>
-          let ppGoal (g : MVarId) := do
-                let (val, _type, _u) ← matchCheckGoalType stx (← g.getType)
-                pure m!"{indentExpr val}"
-          let msg ←
-            match gls with
-              | [] => pure m!"{tactic} expected to fail on {val}, but closed goal."
-              | [g] =>
-                pure <| m!"{tactic} expected to fail on {val}, but returned: {←ppGoal g}"
-              | gls =>
-                let app m g := do pure <| m ++ (←ppGoal g)
-                let init := m!"{tactic} expected to fail on {val}, but returned goals:"
-                gls.foldlM (init := init) app
-          throwErrorAt stx msg
-
-@[builtin_macro Lean.Parser.checkSimp]
-def expandCheckSimp : Macro := fun stx => do
-  let `(#check_simp $t ~> $exp) := stx | Macro.throwUnsupported
-  `(command|#check_tactic $t ~> $exp by simp)
-
-@[builtin_macro Lean.Parser.checkSimpFailure]
-def expandCheckSimpFailure : Macro := fun stx => do
-  let `(#check_simp $t !~>) := stx | Macro.throwUnsupported
-  `(command|#check_tactic_failure $t by simp)
-
-end Lean.Elab.CheckTactic

src/Lean/Elab/Declaration.lean

@@ -347,21 +347,7 @@ def elabMutual : CommandElab := fun stx => do
   let attrs ← elabAttrs attrInsts
   let idents := stx[4].getArgs
   for ident in idents do withRef ident <| liftTermElabM do
-    /-
-    HACK to allow `attribute` command to disable builtin simprocs.
-    TODO: find a better solution. Example: have some "fake" declaration
-    for builtin simprocs.
-    -/
-    let declNames ←
-       try
-         resolveGlobalConst ident
-       catch _ =>
-         let name := ident.getId.eraseMacroScopes
-         if (← Simp.isBuiltinSimproc name) then
-           pure [name]
-         else
-           throwUnknownConstant name
-    let declName ← ensureNonAmbiguous ident declNames
+    let declName ← resolveGlobalConstNoOverloadWithInfo ident
     Term.applyAttributes declName attrs
     for attrName in toErase do
       Attribute.erase declName attrName

src/Lean/Elab/Do.lean

@@ -131,31 +131,12 @@ abbrev Var := Syntax  -- TODO: should be `Ident`
 
 /-- A `doMatch` alternative. `vars` is the array of variables declared by `patterns`. -/
 structure Alt (σ : Type) where
-  ref      : Syntax
-  vars     : Array Var
+  ref : Syntax
+  vars : Array Var
   patterns : Syntax
-  rhs      : σ
+  rhs : σ
   deriving Inhabited
 
-/-- A `doMatchExpr` alternative. -/
-structure AltExpr (σ : Type) where
-  ref     : Syntax
-  var?    : Option Var
-  funName : Syntax
-  pvars   : Array Syntax
-  rhs     : σ
-  deriving Inhabited
-
-def AltExpr.vars (alt : AltExpr σ) : Array Var := Id.run do
-  let mut vars := #[]
-  if let some var := alt.var? then
-    vars := vars.push var
-  for pvar in alt.pvars do
-    match pvar with
-    | `(_) => pure ()
-    | _ => vars := vars.push pvar
-  return vars
-
 /--
   Auxiliary datastructure for representing a `do` code block, and compiling "reassignments" (e.g., `x := x + 1`).
   We convert `Code` into a `Syntax` term representing the:
@@ -217,7 +198,6 @@ inductive Code where
   /-- Recall that an if-then-else may declare a variable using `optIdent` for the branches `thenBranch` and `elseBranch`. We store the variable name at `var?`. -/
   | ite          (ref : Syntax) (h? : Option Var) (optIdent : Syntax) (cond : Syntax) (thenBranch : Code) (elseBranch : Code)
   | match        (ref : Syntax) (gen : Syntax) (discrs : Syntax) (optMotive : Syntax) (alts : Array (Alt Code))
-  | matchExpr    (ref : Syntax) (meta : Bool) (discr : Syntax) (alts : Array (AltExpr Code)) (elseBranch : Code)
   | jmp          (ref : Syntax) (jpName : Name) (args : Array Syntax)
   deriving Inhabited
 
@@ -232,7 +212,6 @@ def Code.getRef? : Code → Option Syntax
   | .return ref _        => ref
   | .ite ref ..          => ref
   | .match ref ..        => ref
-  | .matchExpr ref ..    => ref
   | .jmp ref ..          => ref
 
 abbrev VarSet := RBMap Name Syntax Name.cmp
@@ -264,28 +243,19 @@ partial def CodeBlocl.toMessageData (codeBlock : CodeBlock) : MessageData :=
     | .match _ _ ds _ alts   =>
       m!"match {ds} with"
       ++ alts.foldl (init := m!"") fun acc alt => acc ++ m!"\n| {alt.patterns} => {loop alt.rhs}"
-    | .matchExpr _ meta d alts elseCode =>
-      let r := m!"match_expr {if meta then "" else "(meta := false)"} {d} with"
-      let r := r ++ alts.foldl (init := m!"") fun acc alt =>
-            let acc := acc ++ m!"\n| {if let some var := alt.var? then m!"{var}@" else ""}"
-            let acc := acc ++ m!"{alt.funName}"
-            let acc := acc ++ alt.pvars.foldl (init := m!"") fun acc pvar => acc ++ m!" {pvar}"
-            acc ++ m!" => {loop alt.rhs}"
-      r ++ m!"| _ => {loop elseCode}"
   loop codeBlock.code
 
 /-- Return true if the give code contains an exit point that satisfies `p` -/
 partial def hasExitPointPred (c : Code) (p : Code → Bool) : Bool :=
   let rec loop : Code → Bool
-    | .decl _ _ k             => loop k
-    | .reassign _ _ k         => loop k
-    | .joinpoint _ _ b k      => loop b || loop k
-    | .seq _ k                => loop k
-    | .ite _ _ _ _ t e        => loop t || loop e
-    | .match _ _ _ _ alts     => alts.any (loop ·.rhs)
-    | .matchExpr _ _ _ alts e => alts.any (loop ·.rhs) || loop e
-    | .jmp ..                 => false
-    | c                       => p c
+    | .decl _ _ k         => loop k
+    | .reassign _ _ k     => loop k
+    | .joinpoint _ _ b k  => loop b || loop k
+    | .seq _ k            => loop k
+    | .ite _ _ _ _ t e    => loop t || loop e
+    | .match _ _ _ _ alts => alts.any (loop ·.rhs)
+    | .jmp ..             => false
+    | c                   => p c
   loop c
 
 def hasExitPoint (c : Code) : Bool :=
@@ -330,18 +300,13 @@ partial def convertTerminalActionIntoJmp (code : Code) (jp : Name) (xs : Array V
     | .joinpoint n ps b k    => return .joinpoint n ps (← loop b) (← loop k)
     | .seq e k               => return .seq e (← loop k)
     | .ite ref x? h c t e    => return .ite ref x? h c (← loop t) (← loop e)
+    | .match ref g ds t alts => return .match ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← loop alt.rhs) })
     | .action e              => mkAuxDeclFor e fun y =>
       let ref := e
       -- We jump to `jp` with xs **and** y
       let jmpArgs := xs.push y
       return Code.jmp ref jp jmpArgs
-    | .match ref g ds t alts =>
-      return .match ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← loop alt.rhs) })
-    | .matchExpr ref meta d alts e => do
-      let alts ← alts.mapM fun alt => do pure { alt with rhs := (← loop alt.rhs) }
-      let e ← loop e
-      return .matchExpr ref meta d alts e
-    | c => return c
+    | c                            => return c
   loop code
 
 structure JPDecl where
@@ -407,13 +372,14 @@ def mkJmp (ref : Syntax) (rs : VarSet) (val : Syntax) (mkJPBody : Syntax → Mac
   return Code.jmp ref jp args
 
 /-- `pullExitPointsAux rs c` auxiliary method for `pullExitPoints`, `rs` is the set of update variable in the current path.  -/
-partial def pullExitPointsAux (rs : VarSet) (c : Code) : StateRefT (Array JPDecl) TermElabM Code := do
+partial def pullExitPointsAux (rs : VarSet) (c : Code) : StateRefT (Array JPDecl) TermElabM Code :=
   match c with
   | .decl xs stx k         => return .decl xs stx (← pullExitPointsAux (eraseVars rs xs) k)
   | .reassign xs stx k     => return .reassign xs stx (← pullExitPointsAux (insertVars rs xs) k)
   | .joinpoint j ps b k    => return .joinpoint j ps (← pullExitPointsAux rs b) (← pullExitPointsAux rs k)
   | .seq e k               => return .seq e (← pullExitPointsAux rs k)
   | .ite ref x? o c t e    => return .ite ref x? o c (← pullExitPointsAux (eraseOptVar rs x?) t) (← pullExitPointsAux (eraseOptVar rs x?) e)
+  | .match ref g ds t alts => return .match ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← pullExitPointsAux (eraseVars rs alt.vars) alt.rhs) })
   | .jmp ..                => return  c
   | .break ref             => mkSimpleJmp ref rs (.break ref)
   | .continue ref          => mkSimpleJmp ref rs (.continue ref)
@@ -423,13 +389,6 @@ partial def pullExitPointsAux (rs : VarSet) (c : Code) : StateRefT (Array JPDecl
     mkAuxDeclFor e fun y =>
       let ref := e
       mkJmp ref rs y (fun yFresh => return .action (← ``(Pure.pure $yFresh)))
-  | .match ref g ds t alts =>
-    let alts ← alts.mapM fun alt => do pure { alt with rhs := (← pullExitPointsAux (eraseVars rs alt.vars) alt.rhs) }
-    return .match ref g ds t alts
-  | .matchExpr ref meta d alts e =>
-    let alts ← alts.mapM fun alt => do pure { alt with rhs := (← pullExitPointsAux (eraseVars rs alt.vars) alt.rhs) }
-    let e ← pullExitPointsAux rs e
-    return .matchExpr ref meta d alts e
 
 /--
 Auxiliary operation for adding new variables to the collection of updated variables in a CodeBlock.
@@ -498,14 +457,6 @@ partial def extendUpdatedVarsAux (c : Code) (ws : VarSet) : TermElabM Code :=
         pullExitPoints c
       else
         return .match ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← update alt.rhs) })
-    | .matchExpr ref meta d alts e =>
-      if alts.any fun alt => alt.vars.any fun x => ws.contains x.getId then
-        -- If a pattern variable is shadowing a variable in ws, we `pullExitPoints`
-        pullExitPoints c
-      else
-        let alts ← alts.mapM fun alt => do pure { alt with rhs := (← update alt.rhs) }
-        let e ← update e
-        return .matchExpr ref meta d alts e
     | .ite ref none o c t e => return .ite ref none o c (← update t) (← update e)
     | .ite ref (some h) o cond t e =>
       if ws.contains h.getId then
@@ -619,16 +570,6 @@ def mkMatch (ref : Syntax) (genParam : Syntax) (discrs : Syntax) (optMotive : Sy
     return { ref := alt.ref, vars := alt.vars, patterns := alt.patterns, rhs := rhs.code : Alt Code }
   return { code := .match ref genParam discrs optMotive alts, uvars := ws }
 
-def mkMatchExpr (ref : Syntax) (meta : Bool) (discr : Syntax) (alts : Array (AltExpr CodeBlock)) (elseBranch : CodeBlock) : TermElabM CodeBlock := do
-  -- nary version of homogenize
-  let ws := alts.foldl (union · ·.rhs.uvars) {}
-  let ws := union ws elseBranch.uvars
-  let alts ← alts.mapM fun alt => do
-    let rhs ← extendUpdatedVars alt.rhs ws
-    return { alt with rhs := rhs.code : AltExpr Code }
-  let elseBranch ← extendUpdatedVars elseBranch ws
-  return { code := .matchExpr ref meta discr alts elseBranch.code, uvars := ws }
-
 /-- Return a code block that executes `terminal` and then `k` with the value produced by `terminal`.
    This method assumes `terminal` is a terminal -/
 def concat (terminal : CodeBlock) (kRef : Syntax) (y? : Option Var) (k : CodeBlock) : TermElabM CodeBlock := do
@@ -765,19 +706,6 @@ private def expandDoIf? (stx : Syntax) : MacroM (Option Syntax) := match stx wit
     return some e
   | _ => pure none
 
-/--
-  If the given syntax is a `doLetExpr` or `doLetMetaExpr`, return an equivalent `doIf` that has an `else` but no `else if`s or `if let`s.  -/
-private def expandDoLetExpr? (stx : Syntax) (doElems : List Syntax) : MacroM (Option Syntax) := match stx with
-  | `(doElem| let_expr $pat:matchExprPat := $discr:term | $elseBranch:doSeq) =>
-    return some (← `(doElem| match_expr (meta := false) $discr:term with
-                             | $pat:matchExprPat => $(mkDoSeq doElems.toArray)
-                             | _ => $elseBranch))
-  | `(doElem| let_expr $pat:matchExprPat ← $discr:term | $elseBranch:doSeq) =>
-    return some (← `(doElem| match_expr $discr:term with
-                             | $pat:matchExprPat => $(mkDoSeq doElems.toArray)
-                             | _ => $elseBranch))
-  | _ => return none
-
 structure DoIfView where
   ref        : Syntax
   optIdent   : Syntax
@@ -1149,26 +1077,10 @@ where
       let mut termAlts := #[]
       for alt in alts do
         let rhs ← toTerm alt.rhs
-        let termAlt := mkNode ``Parser.Term.matchAlt #[mkAtomFrom alt.ref "|", mkNullNode #[alt.patterns], mkAtomFrom alt.ref "=>", rhs]
+        let termAlt := mkNode `Lean.Parser.Term.matchAlt #[mkAtomFrom alt.ref "|", mkNullNode #[alt.patterns], mkAtomFrom alt.ref "=>", rhs]
         termAlts := termAlts.push termAlt
-      let termMatchAlts := mkNode ``Parser.Term.matchAlts #[mkNullNode termAlts]
-      return mkNode ``Parser.Term.«match» #[mkAtomFrom ref "match", genParam, optMotive, discrs, mkAtomFrom ref "with", termMatchAlts]
-    | .matchExpr ref meta d alts elseBranch => withFreshMacroScope do
-      let d' ← `(discr)
-      let mut termAlts := #[]
-      for alt in alts do
-        let rhs ← `(($(← toTerm alt.rhs) : $((← read).m) _))
-        let optVar := if let some var := alt.var? then mkNullNode #[var, mkAtomFrom var "@"] else mkNullNode #[]
-        let pat := mkNode ``Parser.Term.matchExprPat #[optVar, alt.funName, mkNullNode alt.pvars]
-        let termAlt := mkNode ``Parser.Term.matchExprAlt #[mkAtomFrom alt.ref "|", pat, mkAtomFrom alt.ref "=>", rhs]
-        termAlts := termAlts.push termAlt
-      let elseBranch := mkNode ``Parser.Term.matchExprElseAlt #[mkAtomFrom ref "|", mkHole ref, mkAtomFrom ref "=>", (← toTerm elseBranch)]
-      let termMatchExprAlts := mkNode ``Parser.Term.matchExprAlts #[mkNullNode termAlts, elseBranch]
-      let body := mkNode ``Parser.Term.matchExpr #[mkAtomFrom ref "match_expr", d', mkAtomFrom ref "with", termMatchExprAlts]
-      if meta then
-        `(Bind.bind (instantiateMVarsIfMVarApp $d) fun discr => $body)
-      else
-        `(let discr := $d; $body)
+      let termMatchAlts := mkNode `Lean.Parser.Term.matchAlts #[mkNullNode termAlts]
+      return mkNode `Lean.Parser.Term.«match» #[mkAtomFrom ref "match", genParam, optMotive, discrs, mkAtomFrom ref "with", termMatchAlts]
 
 def run (code : Code) (m : Syntax) (returnType : Syntax) (uvars : Array Var := #[]) (kind := Kind.regular) : MacroM Syntax :=
   toTerm code { m, returnType, kind, uvars }
@@ -1621,24 +1533,6 @@ mutual
     let matchCode ← mkMatch ref genParam discrs optMotive alts
     concatWith matchCode doElems
 
-  /-- Generate `CodeBlock` for `doMatchExpr; doElems` -/
-  partial def doMatchExprToCode (doMatchExpr : Syntax) (doElems: List Syntax) : M CodeBlock := do
-    let ref       := doMatchExpr
-    let meta      := doMatchExpr[1].isNone
-    let discr     := doMatchExpr[2]
-    let alts      := doMatchExpr[4][0].getArgs -- Array of `doMatchExprAlt`
-    let alts ← alts.mapM fun alt => do
-      let pat      := alt[1]
-      let var?     := if pat[0].isNone then none else some pat[0][0]
-      let funName  := pat[1]
-      let pvars    := pat[2].getArgs
-      let rhs      := alt[3]
-      let rhs ← doSeqToCode (getDoSeqElems rhs)
-      pure { ref, var?, funName, pvars, rhs }
-    let elseBranch ← doSeqToCode (getDoSeqElems doMatchExpr[4][1][3])
-    let matchCode ← mkMatchExpr ref meta discr alts elseBranch
-    concatWith matchCode doElems
-
   /--
     Generate `CodeBlock` for `doTry; doElems`
     ```
@@ -1708,9 +1602,6 @@ mutual
       | none =>
       match (← liftMacroM <| expandDoIf? doElem) with
       | some doElem => doSeqToCode (doElem::doElems)
-      | none =>
-      match (← liftMacroM <| expandDoLetExpr? doElem doElems) with
-      | some doElem => doSeqToCode [doElem]
       | none =>
         let (liftedDoElems, doElem) ← expandLiftMethod doElem
         if !liftedDoElems.isEmpty then
@@ -1749,8 +1640,6 @@ mutual
             doForToCode doElem doElems
           else if k == ``Parser.Term.doMatch then
             doMatchToCode doElem doElems
-          else if k == ``Parser.Term.doMatchExpr then
-            doMatchExprToCode doElem doElems
           else if k == ``Parser.Term.doTry then
             doTryToCode doElem doElems
           else if k == ``Parser.Term.doBreak then

src/Lean/Elab/GuardMsgs.lean

@@ -1,136 +0,0 @@
-/-
-Copyright (c) 2023 Kyle Miller. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kyle Miller
--/
-prelude
-import Lean.Server.CodeActions.Attr
-
-/-! `#guard_msgs` command for testing commands
-
-This module defines a command to test that another command produces the expected messages.
-See the docstring on the `#guard_msgs` command.
--/
-
-open Lean Parser.Tactic Elab Command
-
-namespace Lean.Elab.Tactic.GuardMsgs
-
-/-- Gives a string representation of a message without source position information.
-Ensures the message ends with a '\n'. -/
-private def messageToStringWithoutPos (msg : Message) : IO String := do
-  let mut str ← msg.data.toString
-  unless msg.caption == "" do
-    str := msg.caption ++ ":\n" ++ str
-  if !("\n".isPrefixOf str) then str := " " ++ str
-  match msg.severity with
-  | MessageSeverity.information => str := "info:" ++ str
-  | MessageSeverity.warning     => str := "warning:" ++ str
-  | MessageSeverity.error       => str := "error:" ++ str
-  if str.isEmpty || str.back != '\n' then
-    str := str ++ "\n"
-  return str
-
-/-- The decision made by a specification for a message. -/
-inductive SpecResult
-  /-- Capture the message and check it matches the docstring. -/
-  | check
-  /-- Drop the message and delete it. -/
-  | drop
-  /-- Do not capture the message. -/
-  | passthrough
-
-/-- Parses a `guardMsgsSpec`.
-- No specification: check everything.
-- With a specification: interpret the spec, and if nothing applies pass it through. -/
-def parseGuardMsgsSpec (spec? : Option (TSyntax ``guardMsgsSpec)) :
-    CommandElabM (Message → SpecResult) := do
-  if let some spec := spec? then
-    match spec with
-    | `(guardMsgsSpec| ($[$elts:guardMsgsSpecElt],*)) => do
-      let mut p : Message → SpecResult := fun _ => .passthrough
-      let pushP (s : MessageSeverity) (drop : Bool) (p : Message → SpecResult)
-          (msg : Message) : SpecResult :=
-        if msg.severity == s then if drop then .drop else .check
-        else p msg
-      for elt in elts.reverse do
-        match elt with
-        | `(guardMsgsSpecElt| $[drop%$drop?]? info)    => p := pushP .information drop?.isSome p
-        | `(guardMsgsSpecElt| $[drop%$drop?]? warning) => p := pushP .warning drop?.isSome p
-        | `(guardMsgsSpecElt| $[drop%$drop?]? error)   => p := pushP .error drop?.isSome p
-        | `(guardMsgsSpecElt| $[drop%$drop?]? all) =>
-          p := fun _ => if drop?.isSome then .drop else .check
-        | _ => throwErrorAt elt "Invalid #guard_msgs specification element"
-      return p
-    | _ => throwErrorAt spec "Invalid #guard_msgs specification"
-  else
-    return fun _ => .check
-
-/-- An info tree node corresponding to a failed `#guard_msgs` invocation,
-used for code action support. -/
-structure GuardMsgFailure where
-  /-- The result of the nested command -/
-  res : String
-deriving TypeName
-
-@[builtin_command_elab Lean.guardMsgsCmd] def elabGuardMsgs : CommandElab
-  | `(command| $[$dc?:docComment]? #guard_msgs%$tk $(spec?)? in $cmd) => do
-    let expected : String := (← dc?.mapM (getDocStringText ·)).getD "" |>.trim
-    let specFn ← parseGuardMsgsSpec spec?
-    let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
-    elabCommandTopLevel cmd
-    let msgs := (← get).messages
-    let mut toCheck : MessageLog := .empty
-    let mut toPassthrough : MessageLog := .empty
-    for msg in msgs.toList do
-      match specFn msg with
-      | .check       => toCheck := toCheck.add msg
-      | .drop        => pure ()
-      | .passthrough => toPassthrough := toPassthrough.add msg
-    let res := "---\n".intercalate (← toCheck.toList.mapM (messageToStringWithoutPos ·)) |>.trim
-    -- We do some whitespace normalization here to allow users to break long lines.
-    if expected.replace "\n" " " == res.replace "\n" " " then
-      -- Passed. Only put toPassthrough messages back on the message log
-      modify fun st => { st with messages := initMsgs ++ toPassthrough }
-    else
-      -- Failed. Put all the messages back on the message log and add an error
-      modify fun st => { st with messages := initMsgs ++ msgs }
-      logErrorAt tk m!"❌ Docstring on `#guard_msgs` does not match generated message:\n\n{res}"
-      pushInfoLeaf (.ofCustomInfo { stx := ← getRef, value := Dynamic.mk (GuardMsgFailure.mk res) })
-  | _ => throwUnsupportedSyntax
-
-open CodeAction Server RequestM in
-/-- A code action which will update the doc comment on a `#guard_msgs` invocation. -/
-@[builtin_command_code_action guardMsgsCmd]
-def guardMsgsCodeAction : CommandCodeAction := fun _ _ _ node => do
-  let .node _ ts := node | return #[]
-  let res := ts.findSome? fun
-    | .node (.ofCustomInfo { stx, value }) _ => return (stx, (← value.get? GuardMsgFailure).res)
-    | _ => none
-  let some (stx, res) := res | return #[]
-  let doc ← readDoc
-  let eager := {
-    title := "Update #guard_msgs with tactic output"
-    kind? := "quickfix"
-    isPreferred? := true
-  }
-  pure #[{
-    eager
-    lazy? := some do
-      let some start := stx.getPos? true | return eager
-      let some tail := stx.setArg 0 mkNullNode |>.getPos? true | return eager
-      let newText := if res.isEmpty then
-        ""
-      else if res.length ≤ 100-7 && !res.contains '\n' then -- TODO: configurable line length?
-        s!"/-- {res} -/\n"
-      else
-        s!"/--\n{res}\n-/\n"
-      pure { eager with
-        edit? := some <|.ofTextEdit doc.versionedIdentifier {
-          range := doc.meta.text.utf8RangeToLspRange ⟨start, tail⟩
-          newText
-        }
-      }
-  }]
-
-end Lean.Elab.Tactic.GuardMsgs

src/Lean/Elab/InfoTree/Main.lean

@@ -49,25 +49,14 @@ def PartialContextInfo.mergeIntoOuter?
     some { outer with parentDecl? := innerParentDecl }
 
 def CompletionInfo.stx : CompletionInfo → Syntax
-  | dot i ..          => i.stx
-  | id stx ..         => stx
-  | dotId stx ..      => stx
-  | fieldId stx ..    => stx
-  | namespaceId stx   => stx
-  | option stx        => stx
+  | dot i .. => i.stx
+  | id stx .. => stx
+  | dotId stx .. => stx
+  | fieldId stx .. => stx
+  | namespaceId stx => stx
+  | option stx => stx
   | endSection stx .. => stx
-  | tactic stx ..     => stx
-
-/--
-Obtains the `LocalContext` from this `CompletionInfo` if available and yields an empty context
-otherwise.
--/
-def CompletionInfo.lctx : CompletionInfo → LocalContext
-  | dot i ..            => i.lctx
-  | id _ _ _ lctx ..    => lctx
-  | dotId _ _ lctx ..   => lctx
-  | fieldId _ _ lctx .. => lctx
-  | _                   => .empty
+  | tactic stx .. => stx
 
 def CustomInfo.format : CustomInfo → Format
   | i => f!"CustomInfo({i.value.typeName})"

src/Lean/Elab/Match.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura, Mario Carneiro
 -/
 prelude
 import Lean.Util.ForEachExprWhere
-import Lean.Meta.CtorRecognizer
 import Lean.Meta.Match.Match
 import Lean.Meta.GeneralizeVars
 import Lean.Meta.ForEachExpr
@@ -443,7 +442,7 @@ private def applyRefMap (e : Expr) (map : ExprMap Expr) : Expr :=
 -/
 private def whnfPreservingPatternRef (e : Expr) : MetaM Expr := do
   let eNew ← whnf e
-  if (← isConstructorApp eNew) then
+  if eNew.isConstructorApp (← getEnv) then
     return eNew
   else
     return applyRefMap eNew (mkPatternRefMap e)
@@ -474,7 +473,7 @@ partial def normalize (e : Expr) : M Expr := do
         let p ← normalize p
         addVar h
         return mkApp4 e.getAppFn (e.getArg! 0) x p h
-      else if (← isMatchValue e) then
+      else if isMatchValue e then
         return e
       else if e.isFVar then
         if (← isExplicitPatternVar e) then
@@ -572,8 +571,8 @@ private partial def toPattern (e : Expr) : MetaM Pattern := do
         match e.getArg! 1, e.getArg! 3 with
         | Expr.fvar x, Expr.fvar h => return Pattern.as x p h
         | _,           _           => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
-      else if (← isMatchValue e) then
-        return Pattern.val (← normLitValue e)
+      else if isMatchValue e then
+        return Pattern.val e
       else if e.isFVar then
         return Pattern.var e.fvarId!
       else

src/Lean/Elab/MatchExpr.lean

@@ -1,217 +0,0 @@
-/-
-Copyright (c) 2024 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.Elab.Term
-
-namespace Lean.Elab.Term
-namespace MatchExpr
-/--
-`match_expr` alternative. Recall that it has the following structure.
-```
-| (ident "@")? ident bindeIdent* => rhs
-```
-
-Example:
-```
-| c@Eq _ a b => f c a b
-```
--/
-structure Alt where
-  /--
-  `some c` if there is a variable binding to the function symbol being matched.
-  `c` is the variable name.
-  -/
-  var?    : Option Ident
-  /-- Function being matched. -/
-  funName : Ident
-  /-- Pattern variables. The list uses `none` for representing `_`, and `some a` for pattern variable `a`. -/
-  pvars   : List (Option Ident)
-  /-- right-hand-side for the alternative. -/
-  rhs     : Syntax
-  /-- Store the auxliary continuation function for each right-hand-side. -/
-  k       : Ident := ⟨.missing⟩
-  /-- Actual value to be passed as an argument. -/
-  actuals : List Term := []
-
-/--
-`match_expr` else-alternative. Recall that it has the following structure.
-```
-| _ => rhs
-```
--/
-structure ElseAlt where
-  rhs : Syntax
-
-open Parser Term
-
-/--
-Converts syntax representing a `match_expr` else-alternative into an `ElseAlt`.
--/
-def toElseAlt? (stx : Syntax) : Option ElseAlt :=
-  if !stx.isOfKind ``matchExprElseAlt then none else
-  some { rhs := stx[3] }
-
-/--
-Converts syntax representing a `match_expr` alternative into an `Alt`.
--/
-def toAlt? (stx : Syntax) : Option Alt :=
-  if !stx.isOfKind ``matchExprAlt then none else
-  match stx[1] with
-  | `(matchExprPat| $[$var? @]? $funName:ident $pvars*) =>
-    let pvars := pvars.toList.reverse.map fun arg =>
-      match arg.raw with
-      | `(_) => none
-      | _ => some ⟨arg⟩
-    let rhs := stx[3]
-    some { var?, funName, pvars, rhs }
-  | _ => none
-
-/--
-Returns the function names of alternatives that do not have any pattern variable left.
--/
-def getFunNamesToMatch (alts : List Alt) : List Ident := Id.run do
-  let mut funNames := #[]
-  for alt in alts do
-    if alt.pvars.isEmpty then
-      if Option.isNone <| funNames.find? fun funName => funName.getId == alt.funName.getId then
-        funNames := funNames.push alt.funName
-  return funNames.toList
-
-/--
-Returns `true` if there is at least one alternative whose next pattern variable is not a `_`.
--/
-def shouldSaveActual (alts : List Alt) : Bool :=
-  alts.any fun alt => alt.pvars matches some _ :: _
-
-/--
-Returns the first alternative whose function name is `funName` **and**
-does not have pattern variables left to match.
--/
-def getAltFor? (alts : List Alt) (funName : Ident) : Option Alt :=
-  alts.find? fun alt => alt.funName.getId == funName.getId && alt.pvars.isEmpty
-
-/--
-Removes alternatives that do not have any pattern variable left to be matched.
-For the ones that still have pattern variables, remove the first one, and
-save `actual` if the removed pattern variable is not a `_`.
--/
-def next (alts : List Alt) (actual : Term) : List Alt :=
-  alts.filterMap fun alt =>
-    if let some _ :: pvars := alt.pvars then
-      some { alt with pvars, actuals := actual :: alt.actuals }
-    else if let none :: pvars := alt.pvars then
-      some { alt with pvars }
-    else
-      none
-
-/--
-Creates a fresh identifier for representing the continuation function used to
-execute the RHS of the given alternative, and stores it in the field `k`.
--/
-def initK (alt : Alt) : MacroM Alt := withFreshMacroScope do
-  -- Remark: the compiler frontend implemented in C++ currently detects jointpoints created by
-  -- the "do" notation by testing the name. See hack at method `visit_let` at `lcnf.cpp`
-  -- We will remove this hack when we re-implement the compiler frontend in Lean.
-  let k : Ident ← `(__do_jp)
-  return { alt with k }
-
-/--
-Generates parameters for the continuation function used to execute
-the RHS of the given alternative.
--/
-def getParams (alt : Alt) : MacroM (Array Term) := do
-  let mut params := #[]
-  if let some var := alt.var? then
-    params := params.push (← `(($var : Expr)))
-  params := params ++ (← alt.pvars.toArray.reverse.filterMapM fun
-    | none => return none
-    | some arg => return some (← `(($arg : Expr))))
-  if params.isEmpty then
-    return #[(← `(_))]
-  return params
-
-/--
-Generates the actual arguments for invoking the auxiliary continuation function
-associated with the given alternative. The arguments are the actuals stored in `alt`.
-`discr` is also an argument if `alt.var?` is not none.
--/
-def getActuals (discr : Term) (alt : Alt) : MacroM (Array Term) := do
-  let mut actuals := #[]
-  if alt.var?.isSome then
-    actuals := actuals.push discr
-  actuals := actuals ++ alt.actuals.toArray
-  if actuals.isEmpty then
-    return #[← `(())]
-  return actuals
-
-def toDoubleQuotedName (ident : Ident) : Term :=
-  ⟨mkNode ``Parser.Term.doubleQuotedName #[mkAtom "`", mkAtom "`", ident]⟩
-
-/--
-Generates an `if-then-else` tree for implementing a `match_expr` with discriminant `discr`,
-alternatives `alts`, and else-alternative `elseAlt`.
--/
-partial def generate (discr : Term) (alts : List Alt) (elseAlt : ElseAlt) : MacroM Syntax := do
-  let alts ← alts.mapM initK
-  let discr' ← `(__discr)
-  -- Remark: the compiler frontend implemented in C++ currently detects jointpoints created by
-  -- the "do" notation by testing the name. See hack at method `visit_let` at `lcnf.cpp`
-  -- We will remove this hack when we re-implement the compiler frontend in Lean.
-  let kElse ← `(__do_jp)
-  let rec loop (discr : Term) (alts : List Alt) : MacroM Term := withFreshMacroScope do
-    let funNamesToMatch := getFunNamesToMatch alts
-    let saveActual := shouldSaveActual alts
-    let actual ← if saveActual then `(a) else `(_)
-    let altsNext := next alts actual
-    let body ← if altsNext.isEmpty then
-      `($kElse ())
-    else
-      let discr' ← `(__discr)
-      let body ← loop discr' altsNext
-      if saveActual then
-        `(if h : ($discr).isApp then let a := Expr.appArg $discr h; let __discr := Expr.appFnCleanup $discr h; $body else $kElse ())
-      else
-        `(if h : ($discr).isApp then let __discr := Expr.appFnCleanup $discr h; $body else $kElse ())
-    let mut result := body
-    for funName in funNamesToMatch do
-      if let some alt := getAltFor? alts funName then
-        let actuals ← getActuals discr alt
-        result ← `(if ($discr).isConstOf $(toDoubleQuotedName funName) then $alt.k $actuals* else $result)
-    return result
-  let body ← loop discr' alts
-  let mut result ← `(let_delayed __do_jp := fun (_ : Unit) => $(⟨elseAlt.rhs⟩):term; let __discr := Expr.cleanupAnnotations $discr:term; $body:term)
-  for alt in alts do
-    let params ← getParams alt
-    result ← `(let_delayed $alt.k:ident := fun $params:term* => $(⟨alt.rhs⟩):term; $result:term)
-  return result
-
-def main (discr : Term) (alts : Array Syntax) (elseAlt : Syntax) : MacroM Syntax := do
-  let alts ← alts.toList.mapM fun alt =>
-    if let some alt := toAlt? alt then
-      pure alt
-    else
-      Macro.throwErrorAt alt "unexpected `match_expr` alternative"
-  let some elseAlt := toElseAlt? elseAlt
-    | Macro.throwErrorAt elseAlt "unexpected `match_expr` else-alternative"
-  generate discr alts elseAlt
-
-end MatchExpr
-
-@[builtin_macro Lean.Parser.Term.matchExpr] def expandMatchExpr : Macro := fun stx =>
-  match stx with
-  | `(match_expr $discr:term with $alts) =>
-    MatchExpr.main discr alts.raw[0].getArgs alts.raw[1]
-  | _ => Macro.throwUnsupported
-
-@[builtin_macro Lean.Parser.Term.letExpr] def expandLetExpr : Macro := fun stx =>
-  match stx with
-  | `(let_expr $pat:matchExprPat := $discr:term | $elseBranch:term; $body:term) =>
-    `(match_expr $discr with
-      | $pat:matchExprPat => $body
-      | _ => $elseBranch)
-  | _ => Macro.throwUnsupported
-
-end Lean.Elab.Term

src/Lean/Elab/Notation.lean

@@ -107,10 +107,22 @@ def mkUnexpander (attrKind : TSyntax ``attrKind) (pat qrhs : Term) : OptionT Mac
   -- The reference is attached to the syntactic representation of the called function itself, not the entire function application
   let lhs ← `($$f:ident)
   let lhs := Syntax.mkApp lhs (.mk args)
+  -- allow over-application, avoiding nested `app` nodes
+  let lhsWithMoreArgs := flattenApp (← `($lhs $$moreArgs*))
+  let patWithMoreArgs := flattenApp (← `($pat $$moreArgs*))
   `(@[$attrKind app_unexpander $(mkIdent c)]
     aux_def unexpand $(mkIdent c) : Lean.PrettyPrinter.Unexpander := fun
       | `($lhs)             => withRef f `($pat)
+      -- must be a separate case as the LHS and RHS above might not be `app` nodes
+      | `($lhsWithMoreArgs) => withRef f `($patWithMoreArgs)
       | _                   => throw ())
+where
+  -- NOTE: we consider only one nesting level here
+  flattenApp : Term → Term
+    | stx@`($f $xs*) => match f with
+      | `($f' $xs'*) => Syntax.mkApp f' (xs' ++ xs)
+      | _            => stx
+    | stx            => stx
 
 private def expandNotationAux (ref : Syntax) (currNamespace : Name)
     (doc? : Option (TSyntax ``docComment))

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Eqns
-import Lean.Meta.CtorRecognizer
 import Lean.Util.CollectFVars
 import Lean.Util.ForEachExprWhere
 import Lean.Meta.Tactic.Split
@@ -219,14 +218,13 @@ where
 -/
 private def shouldUseSimpMatch (e : Expr) : MetaM Bool := do
   let env ← getEnv
-  let find (root : Expr) : ExceptT Unit MetaM Unit :=
-    root.forEach fun e => do
-      if let some info := isMatcherAppCore? env e then
-        let args := e.getAppArgs
-        for discr in args[info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do
-          if (← Meta.isConstructorApp discr) then
-            throwThe Unit ()
-  return (← (find e).run) matches .error _
+  return Option.isSome <| e.find? fun e => Id.run do
+    if let some info := isMatcherAppCore? env e then
+      let args := e.getAppArgs
+      for discr in args[info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do
+        if discr.isConstructorApp env then
+          return true
+    return false
 
 partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
   let (_, eqnTypes) ← go mvarId |>.run { declNames } |>.run #[]

src/Lean/Elab/PreDefinition/Main.lean

@@ -121,7 +121,8 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
       preDefs.forM (·.termination.ensureNone "partial")
     else
       try
-        let hasHints := preDefs.any fun preDef => preDef.termination.isNotNone
+        let hasHints := preDefs.any  fun preDef =>
+          preDef.termination.decreasing_by?.isSome || preDef.termination.termination_by?.isSome
         if hasHints then
           wfRecursion preDefs
         else

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -8,7 +8,6 @@ import Lean.Util.HasConstCache
 import Lean.Meta.Match.MatcherApp.Transform
 import Lean.Meta.Tactic.Cleanup
 import Lean.Meta.Tactic.Refl
-import Lean.Meta.Tactic.TryThis
 import Lean.Elab.Quotation
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
@@ -703,19 +702,17 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
   -- Collect all recursive calls and extract their context
   let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities
   let recCalls := filterSubsumed recCalls
-  let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasingBy?)) ·)
+  let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasing_by?)) ·)
   let callMatrix := rcs.map (inspectCall ·)
 
   match ← liftMetaM <| solve measures callMatrix with
   | .some solution => do
     let wf ← buildTermWF originalVarNamess varNamess solution
 
-    let wf' := trimTermWF extraParamss wf
-    for preDef in preDefs, term in wf' do
-      if showInferredTerminationBy.get (← getOptions) then
-        logInfoAt preDef.ref m!"Inferred termination argument:\n{← term.unexpand}"
-      if let some ref := preDef.termination.terminationBy?? then
-        Tactic.TryThis.addSuggestion ref (← term.unexpand)
+    if showInferredTerminationBy.get (← getOptions) then
+      let wf' := trimTermWF extraParamss wf
+      for preDef in preDefs, term in wf' do
+        logInfoAt preDef.ref m!"Inferred termination argument: {← term.unexpand}"
 
     return wf
   | .none =>

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -94,12 +94,12 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
     return (← packMutual fixedPrefixSize preDefs unaryPreDefs, fixedPrefixSize)
 
   let wf ← do
-    let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.terminationBy?.isSome)
+    let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.termination_by?.isSome)
     if preDefsWith.isEmpty then
       -- No termination_by anywhere, so guess one
       guessLex preDefs unaryPreDef fixedPrefixSize
     else if preDefsWithout.isEmpty then
-      pure <| preDefsWith.map (·.termination.terminationBy?.get!)
+      pure <| preDefsWith.map (·.termination.termination_by?.get!)
     else
       -- Some have, some do not, so report errors
       preDefsWithout.forM fun preDef => do
@@ -114,7 +114,7 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
       trace[Elab.definition.wf] "wfRel: {wfRel}"
       let (value, envNew) ← withoutModifyingEnv' do
         addAsAxiom unaryPreDef
-        let value ← mkFix unaryPreDef prefixArgs wfRel (preDefs.map (·.termination.decreasingBy?))
+        let value ← mkFix unaryPreDef prefixArgs wfRel (preDefs.map (·.termination.decreasing_by?))
         eraseRecAppSyntaxExpr value
       /- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/
       let value ← unfoldDeclsFrom envNew value

src/Lean/Elab/PreDefinition/WF/TerminationHint.lean

@@ -27,7 +27,7 @@ structure TerminationBy where
   deriving Inhabited
 
 open Parser.Termination in
-def TerminationBy.unexpand (wf : TerminationBy) : MetaM (TSyntax ``terminationBy) := do
+def TerminationBy.unexpand (wf : TerminationBy) : MetaM Syntax := do
   -- TODO: Why can I not just use $wf.vars in the quotation below?
   let vars : TSyntaxArray `ident := wf.vars.map (⟨·.raw⟩)
   if vars.isEmpty then
@@ -50,9 +50,8 @@ is what `Term.runTactic` expects.
  -/
 structure TerminationHints where
   ref : Syntax
-  terminationBy?? : Option Syntax
-  terminationBy? : Option TerminationBy
-  decreasingBy?  : Option DecreasingBy
+  termination_by? : Option TerminationBy
+  decreasing_by?  : Option DecreasingBy
   /-- Here we record the number of parameters past the `:`. It is set by
   `TerminationHints.rememberExtraParams` and used as folows:
 
@@ -64,27 +63,19 @@ structure TerminationHints where
   extraParams : Nat
   deriving Inhabited
 
-def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, .none, 0⟩
+def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, 0⟩
 
 /-- Logs warnings when the `TerminationHints` are present.  -/
 def TerminationHints.ensureNone (hints : TerminationHints) (reason : String): CoreM Unit := do
-  match hints.terminationBy??, hints.terminationBy?, hints.decreasingBy? with
-  | .none, .none, .none => pure ()
-  | .none, .none, .some dec_by =>
+  match hints.termination_by?, hints.decreasing_by? with
+  | .none, .none => pure ()
+  | .none, .some dec_by =>
     logErrorAt dec_by.ref m!"unused `decreasing_by`, function is {reason}"
-  | .some term_by?, .none, .none =>
-    logErrorAt term_by? m!"unused `termination_by?`, function is {reason}"
-  | .none, .some term_by, .none =>
+  | .some term_by, .none =>
     logErrorAt term_by.ref m!"unused `termination_by`, function is {reason}"
-  | _, _, _ =>
+  | .some _, .some _ =>
     logErrorAt hints.ref m!"unused termination hints, function is {reason}"
 
-/-- True if any form of termination hint is present. -/
-def TerminationHints.isNotNone (hints : TerminationHints) : Bool :=
-  hints.terminationBy??.isSome ||
-  hints.terminationBy?.isSome ||
-  hints.decreasingBy?.isSome
-
 /--
 Remembers `extraParams` for later use. Needs to happen early enough where we still know
 how many parameters came from the function header (`headerParams`).
@@ -120,23 +111,19 @@ def elabTerminationHints {m} [Monad m] [MonadError m] (stx : TSyntax ``suffix) :
   if let .missing := stx.raw then
     return { TerminationHints.none with ref := stx }
   match stx with
-  | `(suffix| $[$t?]? $[$d?:decreasingBy]? ) => do
-    let terminationBy?? : Option Syntax ← if let some t := t? then match t with
-      | `(terminationBy?|termination_by?) => pure (some t)
-      | _ => pure none
-      else pure none
-    let terminationBy? : Option TerminationBy ← if let some t := t? then match t with
-      | `(terminationBy|termination_by => $_body) =>
-        throwErrorAt t "no extra parameters bounds, please omit the `=>`"
-      | `(terminationBy|termination_by $vars* => $body) => pure (some {ref := t, vars, body})
-      | `(terminationBy|termination_by $body:term) => pure (some {ref := t, vars := #[], body})
-      | `(terminationBy?|termination_by?) => pure none
+  | `(suffix| $[$t?:terminationBy]? $[$d?:decreasingBy]? ) => do
+    let termination_by? ← t?.mapM fun t => match t with
+      | `(terminationBy|termination_by $vars* => $body) =>
+        if vars.isEmpty then
+          throwErrorAt t "no extra parameters bounds, please omit the `=>`"
+        else
+          pure {ref := t, vars, body}
+      | `(terminationBy|termination_by $body:term) => pure {ref := t, vars := #[], body}
       | _ => throwErrorAt t "unexpected `termination_by` syntax"
-      else pure none
-    let decreasingBy? ← d?.mapM fun d => match d with
+    let decreasing_by? ← d?.mapM fun d => match d with
       | `(decreasingBy|decreasing_by $tactic) => pure {ref := d, tactic}
       | _ => throwErrorAt d "unexpected `decreasing_by` syntax"
-    return { ref := stx, terminationBy??, terminationBy?, decreasingBy?, extraParams := 0 }
+    return { ref := stx, termination_by?, decreasing_by?, extraParams := 0 }
   | _ => throwErrorAt stx s!"Unexpected Termination.suffix syntax: {stx} of kind {stx.raw.getKind}"
 
 end Lean.Elab.WF

src/Lean/Elab/StructInst.lean

@@ -802,8 +802,10 @@ partial def mkDefaultValueAux? (struct : Struct) : Expr → TermElabM (Option Ex
         let arg ← mkFreshExprMVar d
         mkDefaultValueAux? struct (b.instantiate1 arg)
   | e =>
-    let_expr id _ a := e | return some e
-    return some a
+    if e.isAppOfArity ``id 2 then
+      return some e.appArg!
+    else
+      return some e
 
 def mkDefaultValue? (struct : Struct) (cinfo : ConstantInfo) : TermElabM (Option Expr) :=
   withRef struct.ref do

src/Lean/Elab/Tactic.lean

@@ -37,4 +37,3 @@ import Lean.Elab.Tactic.NormCast
 import Lean.Elab.Tactic.Symm
 import Lean.Elab.Tactic.SolveByElim
 import Lean.Elab.Tactic.LibrarySearch
-import Lean.Elab.Tactic.ShowTerm

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -372,24 +372,10 @@ private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
     let expectedType ← preprocessPropToDecide expectedType
     let d ← mkDecide expectedType
     let d ← instantiateMVars d
-    -- Get instance from `d`
-    let s := d.appArg!
-    -- Reduce the instance rather than `d` itself, since that gives a nicer error message on failure.
-    let r ← withDefault <| whnf s
-    if r.isAppOf ``isFalse then
-      throwError "\
-        tactic 'decide' proved that the proposition\
-        {indentExpr expectedType}\n\
-        is false"
-    unless r.isAppOf ``isTrue do
-      throwError "\
-        tactic 'decide' failed for proposition\
-        {indentExpr expectedType}\n\
-        since its 'Decidable' instance reduced to\
-        {indentExpr r}\n\
-        rather than to the 'isTrue' constructor."
-    -- While we have a proof from reduction, we do not embed it in the proof term,
-    -- but rather we let the kernel recompute it during type checking from a more efficient term.
+    let r ← withDefault <| whnf d
+    unless r.isConstOf ``true do
+      throwError "failed to reduce to 'true'{indentExpr r}"
+    let s := d.appArg! -- get instance from `d`
     let rflPrf ← mkEqRefl (toExpr true)
     return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s rflPrf
 

src/Lean/Elab/Tactic/LibrarySearch.lean

@@ -67,7 +67,8 @@ def elabExact?Term : TermElab := fun stx expectedType? => do
     let goal ← mkFreshExprMVar expectedType
     let (_, introdGoal) ← goal.mvarId!.intros
     introdGoal.withContext do
-      if let some suggestions ← librarySearch introdGoal then
+      let tactic := fun exfalso g => solveByElim []  (maxDepth := 6) exfalso g
+      if let some suggestions ← librarySearch introdGoal tactic then
         reportOutOfHeartbeats `library_search stx
         for suggestion in suggestions do
           withMCtx suggestion.2 do

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -68,7 +68,7 @@ def mkEvalRflProof (e : Expr) (lc : LinearCombo) : OmegaM Expr := do
 `e = (coordinate n).eval atoms`. -/
 def mkCoordinateEvalAtomsEq (e : Expr) (n : Nat) : OmegaM Expr := do
   if n < 10 then
-    let atoms ← atoms
+    let atoms := (← getThe State).atoms
     let tail ← mkListLit (.const ``Int []) atoms[n+1:].toArray.toList
     let lem := .str ``LinearCombo s!"coordinate_eval_{n}"
     mkEqSymm (mkAppN (.const lem []) (atoms[:n+1].toArray.push tail))

src/Lean/Elab/Tactic/Omega/OmegaM.lean

@@ -51,7 +51,7 @@ structure Context where
 /-- The internal state for the `OmegaM` monad, recording previously encountered atoms. -/
 structure State where
   /-- The atoms up-to-defeq encountered so far. -/
-  atoms : HashMap Expr Nat := {}
+  atoms : Array Expr := #[]
 
 /-- An intermediate layer in the `OmegaM` monad. -/
 abbrev OmegaM' := StateRefT State (ReaderT Context MetaM)
@@ -76,11 +76,10 @@ def OmegaM.run (m : OmegaM α) (cfg : OmegaConfig) : MetaM α :=
 def cfg : OmegaM OmegaConfig := do pure (← read).cfg
 
 /-- Retrieve the list of atoms. -/
-def atoms : OmegaM (Array Expr) := do
-  return (← getThe State).atoms.toArray.qsort (·.2 < ·.2) |>.map (·.1)
+def atoms : OmegaM (List Expr) := return (← getThe State).atoms.toList
 
 /-- Return the `Expr` representing the list of atoms. -/
-def atomsList : OmegaM Expr := do mkListLit (.const ``Int []) (← atoms).toList
+def atomsList : OmegaM Expr := do mkListLit (.const ``Int []) (← atoms)
 
 /-- Return the `Expr` representing the list of atoms as a `Coeffs`. -/
 def atomsCoeffs : OmegaM Expr := do
@@ -244,16 +243,15 @@ Return its index, and, if it is new, a collection of interesting facts about the
 -/
 def lookup (e : Expr) : OmegaM (Nat × Option (HashSet Expr)) := do
   let c ← getThe State
-  match c.atoms.find? e with
-  | some i => return (i, none)
-  | none =>
+  for h : i in [:c.atoms.size] do
+    if ← isDefEq e c.atoms[i] then
+      return (i, none)
   trace[omega] "New atom: {e}"
   let facts ← analyzeAtom e
   if ← isTracingEnabledFor `omega then
     unless facts.isEmpty do
       trace[omega] "New facts: {← facts.toList.mapM fun e => inferType e}"
-  let i ← modifyGetThe State fun c =>
-    (c.atoms.size, { c with atoms := c.atoms.insert e c.atoms.size })
+  let i ← modifyGetThe State fun c => (c.atoms.size, { c with atoms := c.atoms.push e })
   return (i, some facts)
 
 end Omega

src/Lean/Elab/Tactic/ShowTerm.lean

@@ -1,28 +0,0 @@
-/-
-Copyright (c) 2021 Scott Morrison. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison, Mario Carneiro
--/
-prelude
-import Lean.Elab.ElabRules
-import Lean.Meta.Tactic.TryThis
-
-namespace Std.Tactic
-open Lean Elab Term Tactic Meta.Tactic.TryThis Parser.Tactic
-
-@[builtin_tactic showTerm] def evalShowTerm : Tactic := fun stx =>
-  match stx with
-  | `(tactic| show_term%$tk $t) => withMainContext do
-    let g ← getMainGoal
-    evalTactic t
-    addExactSuggestion tk (← instantiateMVars (mkMVar g)).headBeta (origSpan? := ← getRef)
-  | _ => throwUnsupportedSyntax
-
-/-- Implementation of `show_term` term elaborator. -/
-@[builtin_term_elab showTermElabImpl] def elabShowTerm : TermElab
-  | `(show_term_elab%$tk $t), ty => do
-    let e ← Term.elabTermEnsuringType t ty
-    Term.synthesizeSyntheticMVarsNoPostponing
-    addTermSuggestion tk (← instantiateMVars e).headBeta (origSpan? := ← getRef)
-    pure e
-  | _, _ => throwUnsupportedSyntax

src/Lean/Elab/Tactic/Simp.lean

@@ -353,13 +353,14 @@ def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax := do
           | true  => `(Parser.Tactic.simpLemma| $decl:term)
           | false => `(Parser.Tactic.simpLemma| ↓ $decl:term)
         args := args.push arg
-    | .fvar fvarId =>
-      -- local hypotheses in the context
+    | .fvar fvarId => -- local hypotheses in the context
+      -- `simp_all` always uses all propositional hypotheses (and it can't use
+      -- any others). So `simp_all only [h]`, where `h` is a hypothesis, would
+      -- be redundant. It would also be confusing since it suggests that only
+      -- `h` is used.
+      if isSimpAll then
+        continue
       if let some ldecl := lctx.find? fvarId then
-        -- `simp_all` always uses all propositional hypotheses.
-        -- So `simp_all only [x]`, only makes sense if `ldecl` is a let-variable.
-        if isSimpAll && !ldecl.hasValue then
-          continue
         localsOrStar := localsOrStar.bind fun locals =>
           if !ldecl.userName.isInaccessibleUserName && !ldecl.userName.hasMacroScopes &&
               (lctx.findFromUserName? ldecl.userName).get!.fvarId == ldecl.fvarId then

src/Lean/Elab/Tactic/SimpTrace.lean

@@ -25,12 +25,13 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
 @[builtin_tactic simpTrace] def evalSimpTrace : Tactic := fun stx =>
   match stx with
   | `(tactic|
-      simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do
+      simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => do
     let stx ← if bang.isSome then
       `(tactic| simp!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
     else
       `(tactic| simp%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
-    let { ctx, simprocs, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
+    let { ctx, simprocs, dischargeWrapper } ←
+      withMainContext <| mkSimpContext stx (eraseLocal := false)
     let usedSimps ← dischargeWrapper.with fun discharge? =>
       simpLocation ctx (simprocs := simprocs) discharge? <|
         (loc.map expandLocation).getD (.targets #[] true)

src/Lean/Exception.lean

@@ -69,7 +69,7 @@ protected def throwError [Monad m] [MonadError m] (msg : MessageData) : m α :=
   let (ref, msg) ← AddErrorMessageContext.add ref msg
   throw <| Exception.error ref msg
 
-/-- Throw an unknown constant error message. -/
+/-- Thrown an unknown constant error message. -/
 def throwUnknownConstant [Monad m] [MonadError m] (constName : Name) : m α :=
   Lean.throwError m!"unknown constant '{mkConst constName}'"
 

src/Lean/Expr.lean

@@ -801,7 +801,7 @@ def isType0 : Expr → Bool
 
 /-- Return `true` if the given expression is `.sort .zero` -/
 def isProp : Expr → Bool
-  | sort .zero => true
+  | sort (.zero ..) => true
   | _ => false
 
 /-- Return `true` if the given expression is a bound variable. -/
@@ -904,14 +904,6 @@ def appArg!' : Expr → Expr
   | app _ a   => a
   | _         => panic! "application expected"
 
-def appArg (e : Expr) (h : e.isApp) : Expr :=
-  match e, h with
-  | .app _ a, _ => a
-
-def appFn (e : Expr) (h : e.isApp) : Expr :=
-  match e, h with
-  | .app f _, _ => f
-
 def sortLevel! : Expr → Level
   | sort u => u
   | _      => panic! "sort expected"
@@ -1045,14 +1037,6 @@ def getAppFn : Expr → Expr
   | app f _ => getAppFn f
   | e         => e
 
-/--
-Similar to `getAppFn`, but skips `mdata`
--/
-def getAppFn' : Expr → Expr
-  | app f _   => getAppFn' f
-  | mdata _ a => getAppFn' a
-  | e         => e
-
 /-- Given `f a₀ a₁ ... aₙ`, returns true if `f` is a constant with name `n`. -/
 def isAppOf (e : Expr) (n : Name) : Bool :=
   match e.getAppFn with
@@ -1075,6 +1059,33 @@ def isAppOfArity' : Expr → Name → Nat → Bool
   | app f _,    n, a+1 => isAppOfArity' f n a
   | _,          _,  _   => false
 
+/--
+Checks if an expression is a "natural number numeral in normal form",
+i.e. of type `Nat`, and explicitly of the form `OfNat.ofNat n`
+where `n` matches `.lit (.natVal n)` for some literal natural number `n`.
+and if so returns `n`.
+-/
+-- Note that `Expr.lit (.natVal n)` is not considered in normal form!
+def nat? (e : Expr) : Option Nat := do
+  guard <| e.isAppOfArity ``OfNat.ofNat 3
+  let lit (.natVal n) := e.appFn!.appArg! | none
+  n
+
+/--
+Checks if an expression is an "integer numeral in normal form",
+i.e. of type `Nat` or `Int`, and either a natural number numeral in normal form (as specified by `nat?`),
+or the negation of a positive natural number numberal in normal form,
+and if so returns the integer.
+-/
+def int? (e : Expr) : Option Int :=
+  if e.isAppOfArity ``Neg.neg 3 then
+    match e.appArg!.nat? with
+    | none => none
+    | some 0 => none
+    | some n => some (-n)
+  else
+    e.nat?
+
 private def getAppNumArgsAux : Expr → Nat → Nat
   | app f _, n => getAppNumArgsAux f (n+1)
   | _,       n => n
@@ -1196,21 +1207,10 @@ def getRevArg! : Expr → Nat → Expr
   | app f _, i+1 => getRevArg! f i
   | _,       _   => panic! "invalid index"
 
-/-- Similar to `getRevArg!` but skips `mdata` -/
-def getRevArg!' : Expr → Nat → Expr
-  | mdata _ a, i => getRevArg!' a i
-  | app _ a, 0   => a
-  | app f _, i+1 => getRevArg!' f i
-  | _,       _   => panic! "invalid index"
-
 /-- Given `f a₀ a₁ ... aₙ`, returns the `i`th argument or panics if out of bounds. -/
 @[inline] def getArg! (e : Expr) (i : Nat) (n := e.getAppNumArgs) : Expr :=
   getRevArg! e (n - i - 1)
 
-/-- Similar to `getArg!`, but skips mdata -/
-@[inline] def getArg!' (e : Expr) (i : Nat) (n := e.getAppNumArgs) : Expr :=
-  getRevArg!' e (n - i - 1)
-
 /-- Given `f a₀ a₁ ... aₙ`, returns the `i`th argument or returns `v₀` if out of bounds. -/
 @[inline] def getArgD (e : Expr) (i : Nat) (v₀ : Expr) (n := e.getAppNumArgs) : Expr :=
   getRevArgD e (n - i - 1) v₀
@@ -1597,45 +1597,12 @@ partial def cleanupAnnotations (e : Expr) : Expr :=
   let e' := e.consumeMData.consumeTypeAnnotations
   if e' == e then e else cleanupAnnotations e'
 
-/--
-Similar to `appFn`, but also applies `cleanupAnnotations` to resulting function.
-This function is used compile the `match_expr` term.
--/
-def appFnCleanup (e : Expr) (h : e.isApp) : Expr :=
-  match e, h with
-  | .app f _, _ => f.cleanupAnnotations
-
 def isFalse (e : Expr) : Bool :=
   e.cleanupAnnotations.isConstOf ``False
 
 def isTrue (e : Expr) : Bool :=
   e.cleanupAnnotations.isConstOf ``True
 
-/--
-Checks if an expression is a "natural number numeral in normal form",
-i.e. of type `Nat`, and explicitly of the form `OfNat.ofNat n`
-where `n` matches `.lit (.natVal n)` for some literal natural number `n`.
-and if so returns `n`.
--/
--- Note that `Expr.lit (.natVal n)` is not considered in normal form!
-def nat? (e : Expr) : Option Nat := do
-  let_expr OfNat.ofNat _ n _ := e | failure
-  let lit (.natVal n) := n | failure
-  n
-
-/--
-Checks if an expression is an "integer numeral in normal form",
-i.e. of type `Nat` or `Int`, and either a natural number numeral in normal form (as specified by `nat?`),
-or the negation of a positive natural number numberal in normal form,
-and if so returns the integer.
--/
-def int? (e : Expr) : Option Int :=
-  let_expr Neg.neg _ _ a := e | e.nat?
-  match a.nat? with
-  | none => none
-  | some 0 => none
-  | some n => some (-n)
-
 /-- Return true iff `e` contains a free variable which satisfies `p`. -/
 @[inline] def hasAnyFVar (e : Expr) (p : FVarId → Bool) : Bool :=
   let rec @[specialize] visit (e : Expr) := if !e.hasFVar then false else

src/Lean/Meta.lean

@@ -46,4 +46,3 @@ import Lean.Meta.Eval
 import Lean.Meta.CoeAttr
 import Lean.Meta.Iterator
 import Lean.Meta.LazyDiscrTree
-import Lean.Meta.LitValues

src/Lean/Meta/Basic.lean

@@ -254,7 +254,7 @@ structure PostponedEntry where
   ref  : Syntax
   lhs  : Level
   rhs  : Level
-  /-- Context for the surrounding `isDefEq` call when the entry was created. -/
+  /-- Context for the surrounding `isDefEq` call when entry was created. -/
   ctx? : Option DefEqContext
   deriving Inhabited
 
@@ -264,7 +264,7 @@ structure PostponedEntry where
 structure State where
   mctx             : MetavarContext := {}
   cache            : Cache := {}
-  /-- When `trackZetaDelta == true`, then any let-decl free variable that is zetaDelta-expanded by `MetaM` is stored in `zetaDeltaFVarIds`. -/
+  /-- When `trackZetaDelta == true`, then any let-decl free variable that is zetaDelta expansion performed by `MetaM` is stored in `zetaDeltaFVarIds`. -/
   zetaDeltaFVarIds : FVarIdSet := {}
   /-- Array of postponed universe level constraints -/
   postponed        : PersistentArray PostponedEntry := {}
@@ -1737,15 +1737,6 @@ def isDefEqNoConstantApprox (t s : Expr) : MetaM Bool :=
 def etaExpand (e : Expr) : MetaM Expr :=
   withDefault do forallTelescopeReducing (← inferType e) fun xs _ => mkLambdaFVars xs (mkAppN e xs)
 
-/--
-If `e` is of the form `?m ...` instantiate metavars
--/
-def instantiateMVarsIfMVarApp (e : Expr) : MetaM Expr := do
-  if e.getAppFn.isMVar then
-    instantiateMVars e
-  else
-    return e
-
 end Meta
 
 builtin_initialize

src/Lean/Meta/CompletionName.lean

@@ -29,21 +29,11 @@ builtin_initialize completionBlackListExt : TagDeclarationExtension ← mkTagDec
 def addToCompletionBlackList (env : Environment) (declName : Name) : Environment :=
   completionBlackListExt.tag env declName
 
-/--
-Checks whether a given name is internal due to something other than `_private`.
-Correctly deals with names like `_private.<SomeNamespace>.0.<SomeType>._sizeOf_1` in a private type
-`SomeType`, which `n.isInternal && !isPrivateName n` does not.
--/
-private def isInternalNameModuloPrivate : Name → Bool
-  | n@(.str p s) => s.get 0 == '_' && n != privateHeader || isInternalNameModuloPrivate p
-  | .num p _ => isInternalNameModuloPrivate p
-  | _       => false
-
 /--
 Return true if name is blacklisted for completion purposes.
 -/
 private def isBlacklisted (env : Environment) (declName : Name) : Bool :=
-  isInternalNameModuloPrivate declName
+  declName.isInternal && !isPrivateName declName
   || isAuxRecursor env declName
   || isNoConfusion env declName
   || isRecCore env declName

src/Lean/Meta/CtorRecognizer.lean

@@ -1,74 +0,0 @@
-/-
-Copyright (c) 2024 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.LitValues
-
-namespace Lean.Meta
-
-private def getConstructorVal? (env : Environment) (ctorName : Name) : Option ConstructorVal :=
-  match env.find? ctorName with
-  | some (.ctorInfo v) => v
-  | _                  => none
-
-
-/--
-If `e` is a constructor application or a builtin literal defeq to a constructor application,
-then return the corresponding `ConstructorVal`.
--/
-def isConstructorApp? (e : Expr) : MetaM (Option ConstructorVal) := do
-  let e ← litToCtor e
-  let .const n _ := e.getAppFn | return none
-  let some v := getConstructorVal? (← getEnv) n | return none
-  if v.numParams + v.numFields == e.getAppNumArgs then
-    return some v
-  else
-    return none
-
-/--
-Similar to `isConstructorApp?`, but uses `whnf`.
--/
-def isConstructorApp'? (e : Expr) : MetaM (Option ConstructorVal) := do
-  if let some r ← isConstructorApp? e then
-    return r
-  isConstructorApp? (← whnf e)
-
-/--
-Returns `true`, if `e` is constructor application of builtin literal defeq to
-a constructor application.
--/
-def isConstructorApp (e : Expr) : MetaM Bool :=
-  return (← isConstructorApp? e).isSome
-
-/--
-Returns `true` if `isConstructorApp e` or `isConstructorApp (← whnf e)`
--/
-def isConstructorApp' (e : Expr) : MetaM Bool := do
-  if (← isConstructorApp e) then return true
-  return (← isConstructorApp (← whnf e))
-
-/--
-If `e` is a constructor application, return a pair containing the corresponding `ConstructorVal` and the constructor
-application arguments.
--/
-def constructorApp? (e : Expr) : MetaM (Option (ConstructorVal × Array Expr)) := do
-  let e ← litToCtor e
-  let .const declName _ := e.getAppFn | return none
-  let some v := getConstructorVal? (← getEnv) declName | return none
-  if v.numParams + v.numFields == e.getAppNumArgs then
-    return some (v, e.getAppArgs)
-  else
-    return none
-
-/--
-Similar to `constructorApp?`, but on failure it puts `e` in WHNF and tries again.
--/
-def constructorApp'? (e : Expr) : MetaM (Option (ConstructorVal × Array Expr)) := do
-  if let some r ← constructorApp? e then
-    return some r
-  else
-    constructorApp? (← whnf e)
-
-end Lean.Meta

src/Lean/Meta/Eqns.lean

@@ -51,8 +51,7 @@ private def shouldGenerateEqnThms (declName : Name) : MetaM Bool := do
     return false
 
 structure EqnsExtState where
-  map    : PHashMap Name (Array Name) := {}
-  mapInv : PHashMap Name Name := {}
+  map : PHashMap Name (Array Name) := {}
   deriving Inhabited
 
 /- We generate the equations on demand, and do not save them on .olean files. -/
@@ -78,22 +77,7 @@ private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
     return none
 
 /--
-Returns `some declName` if `thmName` is an equational theorem for `declName`.
--/
-def isEqnThm? (thmName : Name) : CoreM (Option Name) := do
-  return eqnsExt.getState (← getEnv) |>.mapInv.find? thmName
-
-/--
-Stores in the `eqnsExt` environment extension that `eqThms` are the equational theorems for `declName`
--/
-private def registerEqnThms (declName : Name) (eqThms : Array Name) : CoreM Unit := do
-  modifyEnv fun env => eqnsExt.modifyState env fun s => { s with
-    map := s.map.insert declName eqThms
-    mapInv := eqThms.foldl (init := s.mapInv) fun mapInv eqThm => mapInv.insert eqThm declName
-  }
-
-/--
-  Returns equation theorems for the given declaration.
+  Return equation theorems for the given declaration.
   By default, we do not create equation theorems for nonrecursive definitions.
   You can use `nonRec := true` to override this behavior, a dummy `rfl` proof is created on the fly.
 -/
@@ -103,12 +87,12 @@ def getEqnsFor? (declName : Name) (nonRec := false) : MetaM (Option (Array Name)
   else if (← shouldGenerateEqnThms declName) then
     for f in (← getEqnsFnsRef.get) do
       if let some r ← f declName then
-        registerEqnThms declName r
+        modifyEnv fun env => eqnsExt.modifyState env fun s => { s with map := s.map.insert declName r }
         return some r
     if nonRec then
       let some eqThm ← mkSimpleEqThm declName | return none
       let r := #[eqThm]
-      registerEqnThms declName r
+      modifyEnv fun env => eqnsExt.modifyState env fun s => { s with map := s.map.insert declName r }
       return some r
   return none
 
@@ -147,8 +131,8 @@ def registerGetUnfoldEqnFn (f : GetUnfoldEqnFn) : IO Unit := do
   getUnfoldEqnFnsRef.modify (f :: ·)
 
 /--
-  Return an "unfold" theorem for the given declaration.
-  By default, we do not create unfold theorems for nonrecursive definitions.
+  Return a "unfold" theorem for the given declaration.
+  By default, we not create unfold theorems for nonrecursive definitions.
   You can use `nonRec := true` to override this behavior.
 -/
 def getUnfoldEqnFor? (declName : Name) (nonRec := false) : MetaM (Option Name) := withLCtx {} {} do

src/Lean/Meta/ExprLens.lean

@@ -138,11 +138,11 @@ private def viewCoordRaw: Expr → Nat → M Expr
   | 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.
+/-- Given a valid SubExpr, will return the raw current expression without performing any instantiation.
+If the SubExpr has a type subexpression coordinate then will error.
 
 This is a cheaper version of `Lean.Meta.viewSubexpr` and can be used to quickly view the
-subexpression at a position. Note that because the resulting expression may contain
+subexpression at a position. Note that because the resulting expression will contain
 loose bound variables it can't be used in any `MetaM` methods. -/
 def viewSubexpr (p : Pos) (root : Expr) : M Expr :=
   p.foldlM viewCoordRaw root
@@ -172,3 +172,5 @@ def numBinders (p : Pos) (e : Expr) : M Nat :=
 end ViewRaw
 
 end Lean.Core
+
+

src/Lean/Meta/Injective.lean

@@ -26,8 +26,10 @@ private def mkAnd? (args : Array Expr) : Option Expr := Id.run do
 
 def elimOptParam (type : Expr) : CoreM Expr := do
   Core.transform type fun e =>
-    let_expr optParam _ a := e | return .continue
-    return TransformStep.visit a
+    if e.isAppOfArity  ``optParam 2 then
+      return TransformStep.visit (e.getArg! 0)
+    else
+      return .continue
 
 private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useEq : Bool) : MetaM (Option Expr) := do
   let us := ctorVal.levelParams.map mkLevelParam

src/Lean/Meta/LitValues.lean

@@ -1,148 +0,0 @@
-/-
-Copyright (c) 2024 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.Basic
-
-namespace Lean.Meta
-
-/-!
-Helper functions for recognizing builtin literal values.
-This module focus on recognizing the standard representation used in Lean for these literals.
-It also provides support for the following exceptional cases.
-- Raw natural numbers (i.e., natural numbers which are not encoded using `OfNat.ofNat`).
-- Bit-vectors encoded using `OfNat.ofNat` and `BitVec.ofNat`.
-- Negative integers encoded using raw natural numbers.
-- Characters encoded `Char.ofNat n` where `n` can be a raw natural number or an `OfNat.ofNat`.
-- Nested `Expr.mdata`.
--/
-
-/-- Returns `some n` if `e` is a raw natural number, i.e., it is of the form `.lit (.natVal n)`. -/
-def getRawNatValue? (e : Expr) : Option Nat :=
-  match e.consumeMData with
-  | .lit (.natVal n) => some n
-  | _ => none
-
-/-- Return `some (n, type)` if `e` is an `OfNat.ofNat`-application encoding `n` for a type with name `typeDeclName`. -/
-def getOfNatValue? (e : Expr) (typeDeclName : Name) : MetaM (Option (Nat × Expr)) := OptionT.run do
-  let_expr OfNat.ofNat type n _ ← e | failure
-  let type ← whnfD type
-  guard <| type.getAppFn.isConstOf typeDeclName
-  let .lit (.natVal n) := n.consumeMData | failure
-  return (n, type)
-
-/-- Return `some n` if `e` is a raw natural number or an `OfNat.ofNat`-application encoding `n`. -/
-def getNatValue? (e : Expr) : MetaM (Option Nat) := do
-  let e := e.consumeMData
-  if let some n := getRawNatValue? e then
-    return some n
-  let some (n, _) ← getOfNatValue? e ``Nat | return none
-  return some n
-
-/-- Return `some i` if `e` `OfNat.ofNat`-application encoding an integer, or `Neg.neg`-application of one. -/
-def getIntValue? (e : Expr) : MetaM (Option Int) := do
-  if let some (n, _) ← getOfNatValue? e ``Int then
-    return some n
-  let_expr Neg.neg _ _ a ← e | return none
-  let some (n, _) ← getOfNatValue? a ``Int | return none
-  return some (-↑n)
-
-/-- Return `some c` if `e` is a `Char.ofNat`-application encoding character `c`. -/
-def getCharValue? (e : Expr) : MetaM (Option Char) := do
-  let_expr Char.ofNat n ← e | return none
-  let some n ← getNatValue? n | return none
-  return some (Char.ofNat n)
-
-/-- Return `some s` if `e` is of the form `.lit (.strVal s)`. -/
-def getStringValue? (e : Expr) : (Option String) :=
-  match e with
-  | .lit (.strVal s) => some s
-  | _ => none
-
-/-- Return `some ⟨n, v⟩` if `e` is af `OfNat.ofNat` application encoding a `Fin n` with value `v` -/
-def getFinValue? (e : Expr) : MetaM (Option ((n : Nat) × Fin n)) := OptionT.run do
-  let (v, type) ← getOfNatValue? e ``Fin
-  let n ← getNatValue? (← whnfD type.appArg!)
-  match n with
-  | 0 => failure
-  | m+1 => return ⟨m+1, Fin.ofNat v⟩
-
-/-- Return `some ⟨n, v⟩` if `e` is af `OfNat.ofNat` application encoding a `BitVec n` with value `v` -/
-def getBitVecValue? (e : Expr) : MetaM (Option ((n : Nat) × BitVec n)) := OptionT.run do
-  if e.isAppOfArity' ``BitVec.ofNat 2 then
-    let n ← getNatValue? (e.getArg!' 0)
-    let v ← getNatValue? (e.getArg!' 1)
-    return ⟨n, BitVec.ofNat n v⟩
-  let (v, type) ← getOfNatValue? e ``BitVec
-  let n ← getNatValue? (← whnfD type.appArg!)
-  return ⟨n, BitVec.ofNat n v⟩
-
-/-- Return `some n` if `e` is an `OfNat.ofNat`-application encoding the `UInt8` with value `n`. -/
-def getUInt8Value? (e : Expr) : MetaM (Option UInt8) := OptionT.run do
-  let (n, _) ← getOfNatValue? e ``UInt8
-  return UInt8.ofNat n
-
-/-- Return `some n` if `e` is an `OfNat.ofNat`-application encoding the `UInt16` with value `n`. -/
-def getUInt16Value? (e : Expr) : MetaM (Option UInt16) := OptionT.run do
-  let (n, _) ← getOfNatValue? e ``UInt16
-  return UInt16.ofNat n
-
-/-- Return `some n` if `e` is an `OfNat.ofNat`-application encoding the `UInt32` with value `n`. -/
-def getUInt32Value? (e : Expr) : MetaM (Option UInt32) := OptionT.run do
-  let (n, _) ← getOfNatValue? e ``UInt32
-  return UInt32.ofNat n
-
-/-- Return `some n` if `e` is an `OfNat.ofNat`-application encoding the `UInt64` with value `n`. -/
-def getUInt64Value? (e : Expr) : MetaM (Option UInt64) := OptionT.run do
-  let (n, _) ← getOfNatValue? e ``UInt64
-  return UInt64.ofNat n
-
-/--
-If `e` is a literal value, ensure it is encoded using the standard representation.
-Otherwise, just return `e`.
--/
-def normLitValue (e : Expr) : MetaM Expr := do
-  let e ← instantiateMVars e
-  if let some n ← getNatValue? e then return toExpr n
-  if let some n ← getIntValue? e then return toExpr n
-  if let some ⟨_, n⟩ ← getFinValue? e then return toExpr n
-  if let some ⟨_, n⟩ ← getBitVecValue? e then return toExpr n
-  if let some s := getStringValue? e then return toExpr s
-  if let some c ← getCharValue? e then return toExpr c
-  if let some n ← getUInt8Value? e then return toExpr n
-  if let some n ← getUInt16Value? e then return toExpr n
-  if let some n ← getUInt32Value? e then return toExpr n
-  if let some n ← getUInt64Value? e then return toExpr n
-  return e
-
-/--
-If `e` is a `Nat`, `Int`, or `Fin` literal value, converts it into a constructor application.
-Otherwise, just return `e`.
--/
--- TODO: support other builtin literals if needed
-def litToCtor (e : Expr) : MetaM Expr := do
-  let e ← instantiateMVars e
-  if let some n ← getNatValue? e then
-    if n = 0 then
-      return mkConst ``Nat.zero
-    else
-      return .app (mkConst ``Nat.succ) (toExpr (n-1))
-  if let some n ← getIntValue? e then
-    if n < 0 then
-      return .app (mkConst ``Int.negSucc) (toExpr (- (n+1)).toNat)
-    else
-      return .app (mkConst ``Int.ofNat) (toExpr n.toNat)
-  if let some ⟨n, v⟩ ← getFinValue? e then
-    let i := toExpr v.val
-    let n := toExpr n
-    -- Remark: we construct the proof manually here to avoid a cyclic dependency.
-    let p := mkApp4 (mkConst ``LT.lt [0]) (mkConst ``Nat) (mkConst ``instLTNat) i n
-    let h := mkApp3 (mkConst ``of_decide_eq_true) p
-      (mkApp2 (mkConst ``Nat.decLt) i n)
-      (mkApp2 (mkConst ``Eq.refl [1]) (mkConst ``Bool) (mkConst ``true))
-    return mkApp3 (mkConst ``Fin.mk) n i h
-  return e
-
-end Lean.Meta

src/Lean/Meta/Match/Basic.lean

@@ -343,7 +343,7 @@ partial def toPattern (e : Expr) : MetaM Pattern := do
         match e.getArg! 1, e.getArg! 3 with
         | Expr.fvar x, Expr.fvar h => return Pattern.as x p h
         | _,           _   => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
-      else if (← isMatchValue e) then
+      else if isMatchValue e then
         return Pattern.val e
       else if e.isFVar then
         return Pattern.var e.fvarId!

src/Lean/Meta/Match/CaseValues.lean

@@ -30,7 +30,7 @@ private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hNa
     let tag ← mvarId.getTag
     mvarId.checkNotAssigned `caseValue
     let target ← mvarId.getType
-    let xEqValue ← mkEq (mkFVar fvarId) (← normLitValue value)
+    let xEqValue ← mkEq (mkFVar fvarId) (foldPatValue value)
     let xNeqValue := mkApp (mkConst `Not) xEqValue
     let thenTarget := Lean.mkForall hName BinderInfo.default xEqValue  target
     let elseTarget := Lean.mkForall hName BinderInfo.default xNeqValue target

src/Lean/Meta/Match/Match.lean

@@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.LitValues
 import Lean.Meta.Check
 import Lean.Meta.Closure
-import Lean.Meta.CtorRecognizer
 import Lean.Meta.Tactic.Cases
 import Lean.Meta.Tactic.Contradiction
 import Lean.Meta.GeneralizeTelescope
@@ -96,17 +94,10 @@ private def hasValPattern (p : Problem) : Bool :=
     | .val _ :: _ => true
     | _           => false
 
-private def hasNatValPattern (p : Problem) : MetaM Bool :=
-  p.alts.anyM fun alt => do
-    match alt.patterns with
-    | .val v :: _ => return (← getNatValue? v).isSome
-    | _           => return false
-
-private def hasIntValPattern (p : Problem) : MetaM Bool :=
-  p.alts.anyM fun alt => do
-    match alt.patterns with
-    | .val v :: _ => return (← getIntValue? v).isSome
-    | _           => return false
+private def hasNatValPattern (p : Problem) : Bool :=
+  p.alts.any fun alt => match alt.patterns with
+    | .val v :: _ => v.isRawNatLit -- TODO: support `OfNat.ofNat`?
+    | _           => false
 
 private def hasVarPattern (p : Problem) : Bool :=
   p.alts.any fun alt => match alt.patterns with
@@ -139,21 +130,6 @@ private def isValueTransition (p : Problem) : Bool :=
      | .var _ :: _ => true
      | _           => false
 
-private def isValueOnlyTransitionCore (p : Problem) (isValue : Expr → MetaM Bool) : MetaM Bool := do
-  if hasVarPattern p then return false
-  if !hasValPattern p then return false
-  p.alts.allM fun alt => do
-     match alt.patterns with
-     | .val v :: _   => isValue v
-     | .ctor .. :: _ => return true
-     | _             => return false
-
-private def isFinValueTransition (p : Problem) : MetaM Bool :=
-  isValueOnlyTransitionCore p fun e => return (← getFinValue? e).isSome
-
-private def isBitVecValueTransition (p : Problem) : MetaM Bool :=
-  isValueOnlyTransitionCore p fun e => return (← getBitVecValue? e).isSome
-
 private def isArrayLitTransition (p : Problem) : Bool :=
   hasArrayLitPattern p && hasVarPattern p
   && p.alts.all fun alt => match alt.patterns with
@@ -161,32 +137,13 @@ private def isArrayLitTransition (p : Problem) : Bool :=
      | .var _ :: _       => true
      | _                 => false
 
-private def hasCtorOrInaccessible (p : Problem) : Bool :=
-  !isNextVar p ||
-    p.alts.any fun alt => match alt.patterns with
-    | .ctor .. :: _        => true
-    | .inaccessible _ :: _ => true
-    | _                    => false
-
-private def isNatValueTransition (p : Problem) : MetaM Bool := do
-  unless (← hasNatValPattern p) do return false
-  return hasCtorOrInaccessible p
-
-/--
-Predicate for testing whether we need to expand `Int` value patterns into constructors.
-There are two cases:
-- We have constructor or inaccessible patterns. Example:
-```
-| 0, ...
-| Int.toVal p, ...
-...
-```
-- We don't have the `else`-case (i.e., variable pattern). This can happen
-when the non-value cases are unreachable.
--/
-private def isIntValueTransition (p : Problem) : MetaM Bool := do
-  unless (← hasIntValPattern p) do return false
-  return hasCtorOrInaccessible p || !hasVarPattern p
+private def isNatValueTransition (p : Problem) : Bool :=
+  hasNatValPattern p
+  && (!isNextVar p ||
+      p.alts.any fun alt => match alt.patterns with
+      | .ctor .. :: _        => true
+      | .inaccessible _ :: _ => true
+      | _                    => false)
 
 private def processSkipInaccessible (p : Problem) : Problem := Id.run do
   let x :: xs := p.vars | unreachable!
@@ -416,13 +373,14 @@ private def hasRecursiveType (x : Expr) : MetaM Bool := do
    update the next patterns with the fields of the constructor.
    Otherwise, return none. -/
 def processInaccessibleAsCtor (alt : Alt) (ctorName : Name) : MetaM (Option Alt) := do
+  let env ← getEnv
   match alt.patterns with
   | p@(.inaccessible e) :: ps =>
     trace[Meta.Match.match] "inaccessible in ctor step {e}"
     withExistingLocalDecls alt.fvarDecls do
       -- Try to push inaccessible annotations.
       let e ← whnfD e
-      match (← constructorApp? e) with
+      match e.constructorApp? env with
       | some (ctorVal, ctorArgs) =>
         if ctorVal.name == ctorName then
           let fields := ctorArgs.extract ctorVal.numParams ctorArgs.size
@@ -503,12 +461,12 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do
 private def altsAreCtorLike (p : Problem) : MetaM Bool := withGoalOf p do
   p.alts.allM fun alt => do match alt.patterns with
     | .ctor .. :: _ => return true
-    | .inaccessible e :: _ => isConstructorApp e
+    | .inaccessible e :: _ => return (← whnfD e).isConstructorApp (← getEnv)
     | _ => return false
 
 private def processNonVariable (p : Problem) : MetaM Problem := withGoalOf p do
   let x :: xs := p.vars | unreachable!
-  if let some (ctorVal, xArgs) ← withTransparency .default <| constructorApp'? x then
+  if let some (ctorVal, xArgs) := (← whnfD x).constructorApp? (← getEnv) then
     if (← altsAreCtorLike p) then
       let alts ← p.alts.filterMapM fun alt => do
         match alt.patterns with
@@ -626,46 +584,12 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
       let newAlts := p.alts.filter isFirstPatternVar
       return { p with mvarId := subgoal.mvarId, alts := newAlts, vars := x::xs }
 
-private def expandNatValuePattern (p : Problem) : MetaM Problem := do
-  let alts ← p.alts.mapM fun alt => do
-    match alt.patterns with
-    | .val n :: ps =>
-      match (← getNatValue? n) with
-      | some 0     => return { alt with patterns := .ctor ``Nat.zero [] [] [] :: ps }
-      | some (n+1) => return { alt with patterns := .ctor ``Nat.succ [] [] [.val (toExpr n)] :: ps }
-      | _ => return alt
-    | _ => return alt
-  return { p with alts := alts }
-
-private def expandIntValuePattern (p : Problem) : MetaM Problem := do
-  let alts ← p.alts.mapM fun alt => do
-    match alt.patterns with
-    | .val n :: ps =>
-      match (← getIntValue? n) with
-      | some i =>
-        if i >= 0 then
-        return { alt with patterns := .ctor ``Int.ofNat [] [] [.val (toExpr i.toNat)] :: ps }
-        else
-        return { alt with patterns := .ctor ``Int.negSucc [] [] [.val (toExpr (-(i + 1)).toNat)] :: ps }
-      | _ => return alt
-    | _ => return alt
-  return { p with alts := alts }
-
-private def expandFinValuePattern (p : Problem) : MetaM Problem := do
-  let alts ← p.alts.mapM fun alt => do
-    let .val n :: ps := alt.patterns | return alt
-    let some ⟨n, v⟩ ← getFinValue? n | return alt
-    let p ← mkLt (toExpr v.val) (toExpr n)
-    let h ← mkDecideProof p
-    return { alt with patterns := .ctor ``Fin.mk [] [toExpr n] [.val (toExpr v.val), .inaccessible h] :: ps }
-  return { p with alts := alts }
-
-private def expandBitVecValuePattern (p : Problem) : MetaM Problem := do
-  let alts ← p.alts.mapM fun alt => do
-    let .val n :: ps := alt.patterns | return alt
-    let some ⟨_, v⟩ ← getBitVecValue? n | return alt
-    return { alt with patterns := .ctor ``BitVec.ofFin [] [] [.val (toExpr v.toFin)] :: ps }
-  return { p with alts := alts }
+private def expandNatValuePattern (p : Problem) : Problem :=
+  let alts := p.alts.map fun alt => match alt.patterns with
+    | .val (.lit (.natVal 0)) :: ps     => { alt with patterns := .ctor ``Nat.zero [] [] [] :: ps }
+    | .val (.lit (.natVal (n+1))) :: ps => { alt with patterns := .ctor ``Nat.succ [] [] [.val (mkRawNatLit n)] :: ps }
+    | _                                 => alt
+  { p with alts := alts }
 
 private def traceStep (msg : String) : StateRefT State MetaM Unit := do
   trace[Meta.Match.match] "{msg} step"
@@ -710,18 +634,9 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := do
     traceStep ("as-pattern")
     let p ← processAsPattern p
     process p
-  else if (← isNatValueTransition p) then
+  else if isNatValueTransition p then
     traceStep ("nat value to constructor")
-    process (← expandNatValuePattern p)
-  else if (← isIntValueTransition p) then
-    traceStep ("int value to constructor")
-    process (← expandIntValuePattern p)
-  else if (← isFinValueTransition p) then
-    traceStep ("fin value to constructor")
-    process (← expandFinValuePattern p)
-  else if (← isBitVecValueTransition p) then
-    traceStep ("bitvec value to constructor")
-    process (← expandBitVecValuePattern p)
+    process (expandNatValuePattern p)
   else if !isNextVar p then
     traceStep ("non variable")
     let p ← processNonVariable p
@@ -739,11 +654,11 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := do
   else if isArrayLitTransition p then
     let ps ← processArrayLit p
     ps.forM process
-  else if (← hasNatValPattern p) then
+  else if hasNatValPattern p then
     -- This branch is reachable when `p`, for example, is just values without an else-alternative.
     -- We added it just to get better error messages.
     traceStep ("nat value to constructor")
-    process (← expandNatValuePattern p)
+    process (expandNatValuePattern p)
   else
     checkNextPatternTypes p
     throwNonSupported p

src/Lean/Meta/Match/MatchEqs.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.CtorRecognizer
 import Lean.Meta.Match.Match
 import Lean.Meta.Match.MatchEqsExt
 import Lean.Meta.Tactic.Apply
@@ -16,35 +15,6 @@ import Lean.Meta.Tactic.Contradiction
 
 namespace Lean.Meta
 
-/--
-A custom, approximated, and quick `contradiction` tactic.
-It only finds contradictions of the form `(h₁ : p)` and `(h₂ : ¬ p)` where
-`p`s are structurally equal. The procedure is not quadratic like `contradiction`.
-
-We use it to improve the performance of `proveSubgoalLoop` at `mkSplitterProof`.
-We will eventually have to write more efficient proof automation for this module.
-The new proof automation should exploit the structure of the generated goals and avoid general purpose tactics
-such as `contradiction`.
--/
-private def _root_.Lean.MVarId.contradictionQuick (mvarId : MVarId) : MetaM Bool := do
-  mvarId.withContext do
-    let mut posMap : HashMap Expr FVarId := {}
-    let mut negMap : HashMap Expr FVarId := {}
-    for localDecl in (← getLCtx) do
-      unless localDecl.isImplementationDetail do
-        if let some p ← matchNot? localDecl.type then
-          if let some pFVarId := posMap.find? p then
-            mvarId.assign (← mkAbsurd (← mvarId.getType) (mkFVar pFVarId) localDecl.toExpr)
-            return true
-          negMap := negMap.insert p localDecl.fvarId
-        if (← isProp localDecl.type) then
-          if let some nFVarId := negMap.find? localDecl.type then
-            mvarId.assign (← mkAbsurd (← mvarId.getType) localDecl.toExpr (mkFVar nFVarId))
-            return true
-          posMap := posMap.insert localDecl.type localDecl.fvarId
-      pure ()
-    return false
-
 /--
   Helper method for `proveCondEqThm`. Given a goal of the form `C.rec ... xMajor = rhs`,
   apply `cases xMajor`. -/
@@ -251,7 +221,7 @@ private def processNextEq : M Bool := do
           return true
         -- If it is not possible, we try to show the hypothesis is redundant by substituting even variables that are not at `s.xs`, and then use contradiction.
         else
-          match (← isConstructorApp? lhs), (← isConstructorApp? rhs) with
+          match lhs.isConstructorApp? (← getEnv), rhs.isConstructorApp? (← getEnv) with
           | some lhsCtor, some rhsCtor =>
             if lhsCtor.name != rhsCtor.name then
               return false -- If the constructors are different, we can discard the hypothesis even if it a heterogeneous equality
@@ -379,7 +349,7 @@ private def injectionAnyCandidate? (type : Expr) : MetaM (Option (Expr × Expr))
       return some (lhs, rhs)
   return none
 
-private def injectionAny (mvarId : MVarId) : MetaM InjectionAnyResult := do
+private def injectionAny (mvarId : MVarId) : MetaM InjectionAnyResult :=
   mvarId.withContext do
     for localDecl in (← getLCtx) do
       if let some (lhs, rhs) ← injectionAnyCandidate? localDecl.type then
@@ -597,8 +567,6 @@ where
 
   proveSubgoalLoop (mvarId : MVarId) : MetaM Unit := do
     trace[Meta.Match.matchEqs] "proveSubgoalLoop\n{mvarId}"
-    if (← mvarId.contradictionQuick) then
-      return ()
     match (← injectionAny mvarId) with
     | InjectionAnyResult.solved => return ()
     | InjectionAnyResult.failed =>

src/Lean/Meta/Match/Value.lean

@@ -4,24 +4,46 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.LitValues
 import Lean.Expr
 
 namespace Lean.Meta
+-- TODO: produce error for `USize` because `USize.decEq` depends on an opaque value: `System.Platform.numBits`.
+
+-- TODO: move?
+private def UIntTypeNames : Array Name :=
+  #[``UInt8, ``UInt16, ``UInt32, ``UInt64, ``USize]
+
+private def isUIntTypeName (n : Name) : Bool :=
+  UIntTypeNames.contains n
+
+def isFinPatLit (e : Expr) : Bool :=
+  e.isAppOfArity `Fin.ofNat 2 && e.appArg!.isRawNatLit
+
+/-- Return `some (typeName, numLit)` if `v` is of the form `UInt*.mk (Fin.ofNat _ numLit)` -/
+def isUIntPatLit? (v : Expr) : Option (Name × Expr) :=
+  match v with
+  | Expr.app (Expr.const (Name.str typeName "mk" ..) ..) val .. =>
+    if isUIntTypeName typeName && isFinPatLit val then
+      some (typeName, val.appArg!)
+    else
+      none
+  | _ => none
+
+def isUIntPatLit (v : Expr) : Bool :=
+  isUIntPatLit? v |>.isSome
+
+/--
+  The frontend expands uint numerals occurring in patterns into `UInt*.mk ..` constructor applications.
+  This method convert them back into `UInt*.ofNat ..` applications.
+-/
+def foldPatValue (v : Expr) : Expr :=
+  match isUIntPatLit? v with
+  | some (typeName, numLit) => mkApp (mkConst (Name.mkStr typeName "ofNat")) numLit
+  | _ => v
+
 
 /-- Return true is `e` is a term that should be processed by the `match`-compiler using `casesValues` -/
-def isMatchValue (e : Expr) : MetaM Bool := do
-  let e ← instantiateMVars e
-  if (← getNatValue? e).isSome then return true
-  if (← getIntValue? e).isSome then return true
-  if (← getFinValue? e).isSome then return true
-  if (← getBitVecValue? e).isSome then return true
-  if (getStringValue? e).isSome then return true
-  if (← getCharValue? e).isSome then return true
-  if (← getUInt8Value? e).isSome then return true
-  if (← getUInt16Value? e).isSome then return true
-  if (← getUInt32Value? e).isSome then return true
-  if (← getUInt64Value? e).isSome then return true
-  return false
+def isMatchValue (e : Expr) : Bool :=
+  e.isRawNatLit || e.isCharLit || e.isStringLit || isFinPatLit e || isUIntPatLit e
 
 end Lean.Meta

src/Lean/Meta/MatchUtil.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Util.Recognizers
 import Lean.Meta.Basic
-import Lean.Meta.CtorRecognizer
 
 namespace Lean.Meta
 
@@ -63,6 +62,8 @@ def matchNe? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) :=
       return none
 
 def matchConstructorApp? (e : Expr) : MetaM (Option ConstructorVal) := do
-  matchHelper? e isConstructorApp?
+  let env ← getEnv
+  matchHelper? e fun e =>
+    return e.isConstructorApp? env
 
 end Lean.Meta

src/Lean/Meta/Tactic/Acyclic.lean

@@ -14,7 +14,7 @@ private def isTarget (lhs rhs : Expr) : MetaM Bool := do
   if !lhs.isFVar || !lhs.occurs rhs then
     return false
   else
-    isConstructorApp' rhs
+    return (← whnf rhs).isConstructorApp (← getEnv)
 
 /--
   Close the given goal if `h` is a proof for an equality such as `as = a :: as`.

src/Lean/Meta/Tactic/ElimInfo.lean

@@ -37,15 +37,6 @@ structure ElimInfo where
   altsInfo   : Array ElimAltInfo := #[]
   deriving Repr, Inhabited
 
-
-/-- Given the type `t` of an alternative, determines the number of parameters
-(.forall and .let)-bound, and whether the conclusion is a `motive`-application.  -/
-def altArity (motive : Expr) (n : Nat) : Expr → Nat × Bool
-  | .forallE _ _ b _ => altArity motive (n+1) b
-  | .letE _ _ _ b _ => altArity motive (n+1) b
-  | conclusion => (n, conclusion.getAppFn == motive)
-
-
 def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : MetaM ElimInfo := do
   let elimType ← inferType elimExpr
   trace[Elab.induction] "eliminator {indentExpr elimExpr}\nhas type{indentExpr elimType}"
@@ -73,7 +64,8 @@ def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : Me
       if x != motive && !targets.contains x then
         let xDecl ← x.fvarId!.getDecl
         if xDecl.binderInfo.isExplicit then
-          let (numFields, provesMotive) := altArity motive 0 xDecl.type
+          let (numFields, provesMotive) ← forallTelescopeReducing xDecl.type fun args concl =>
+            pure (args.size, concl.getAppFn == motive)
           let name := xDecl.userName
           let declName? := do
             let base ← baseDeclName?

src/Lean/Meta/Tactic/Injection.lean

@@ -34,19 +34,19 @@ def injectionCore (mvarId : MVarId) (fvarId : FVarId) : MetaM InjectionResultCor
       match type.eq? with
       | none           => throwTacticEx `injection mvarId "equality expected"
       | some (_, a, b) =>
+        let a ← whnf a
+        let b ← whnf b
         let target ← mvarId.getType
-        match (← isConstructorApp'? a), (← isConstructorApp'? b) with
+        let env ← getEnv
+        match a.isConstructorApp? env, b.isConstructorApp? env with
         | some aCtor, some bCtor =>
-          -- We use the default transparency because `a` and `b` may be builtin literals.
-          let val ← withTransparency .default <| mkNoConfusion target prf
+          let val ← mkNoConfusion target prf
           if aCtor.name != bCtor.name then
             mvarId.assign val
             return InjectionResultCore.solved
           else
             let valType ← inferType val
-            -- We use the default transparency setting here because `a` and `b` may be builtin literals
-            -- that need to expanded into constructors.
-            let valType ← whnfD valType
+            let valType ← whnf valType
             match valType with
             | Expr.forallE _ newTarget _ _ =>
               let newTarget := newTarget.headBeta

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -57,6 +57,9 @@ inductive DeclMod
   | /-- the backward direction of an `iff` -/ mpr
 deriving DecidableEq, Inhabited, Ord
 
+instance : ToString DeclMod where
+  toString m := match m with | .none => "" | .mp => "mp" | .mpr => "mpr"
+
 /--
 LibrarySearch has an extension mechanism for replacing the function used
 to find candidate lemmas.
@@ -282,26 +285,6 @@ def mkLibrarySearchLemma (lem : Name) (mod : DeclMod) : MetaM Expr := do
   | .mp => mapForallTelescope (fun e => mkAppM ``Iff.mp #[e]) lem
   | .mpr => mapForallTelescope (fun e => mkAppM ``Iff.mpr #[e]) lem
 
-private def isVar (e : Expr) : Bool :=
-  match e with
-  | .bvar _ => true
-  | .fvar _ => true
-  | .mvar _ => true
-  | _ => false
-
-private def isNonspecific (type : Expr) : MetaM Bool := do
-  forallTelescope type fun _ tp =>
-    match tp.getAppFn with
-    | .bvar _ => pure true
-    | .fvar _ => pure true
-    | .mvar _ => pure true
-    | .const nm _ =>
-      if nm = ``Eq then
-        pure (tp.getAppArgsN 3 |>.all isVar)
-      else
-        pure false
-    | _ => pure false
-
 /--
 Tries to apply the given lemma (with symmetry modifier) to the goal,
 then tries to close subsequent goals using `solveByElim`.
@@ -311,14 +294,9 @@ otherwise the full list of subgoals is returned.
 private def librarySearchLemma (cfg : ApplyConfig) (act : List MVarId → MetaM (List MVarId))
     (allowFailure : MVarId → MetaM Bool) (cand : Candidate)  : MetaM (List MVarId) := do
   let ((goal, mctx), (name, mod)) := cand
-  let ppMod (mod : DeclMod) : MessageData :=
-        match mod with | .none => "" | .mp => " with mp" | .mpr => " with mpr"
-  withTraceNode `Tactic.librarySearch (return m!"{emoji ·} trying {name}{ppMod mod} ") do
+  withTraceNode `Tactic.librarySearch (return m!"{emoji ·} trying {name} with {mod} ") do
     setMCtx mctx
     let lem ← mkLibrarySearchLemma name mod
-    let lemType ← instantiateMVars (← inferType lem)
-    if ← isNonspecific lemType then
-      failure
     let newGoals ← goal.apply lem cfg
     try
       act newGoals
@@ -408,8 +386,7 @@ unless the goal was completely solved.)
 this is not currently tracked.)
 -/
 def librarySearch (goal : MVarId)
-    (tactic : Bool → List MVarId → MetaM (List MVarId) :=
-      fun initial g => solveByElim [] (maxDepth := 6) (exfalso := initial) g)
+    (tactic : Bool → List MVarId → MetaM (List MVarId))
     (allowFailure : MVarId → MetaM Bool := fun _ => pure true)
     (leavePercentHeartbeats : Nat := 10) :
     MetaM (Option (Array (List MVarId × MetavarContext))) := do

src/Lean/Meta/Tactic/NormCast.lean

@@ -5,7 +5,7 @@ Authors: Paul-Nicolas Madelaine, Robert Y. Lewis, Mario Carneiro, Gabriel Ebner
 -/
 prelude
 import Lean.Meta.CongrTheorems
-import Lean.Meta.Tactic.Simp.Attr
+import Lean.Meta.Tactic.Simp.SimpTheorems
 import Lean.Meta.CoeAttr
 
 namespace Lean.Meta.NormCast

src/Lean/Meta/Tactic/Rewrite.lean

@@ -8,7 +8,6 @@ import Lean.Meta.AppBuilder
 import Lean.Meta.MatchUtil
 import Lean.Meta.KAbstract
 import Lean.Meta.Check
-import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.Apply
 
 namespace Lean.Meta
@@ -54,7 +53,6 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           let u2 ← getLevel eType
           let eqPrf := mkApp6 (.const ``congrArg [u1, u2]) α eType lhs rhs motive heq
           postprocessAppMVars `rewrite mvarId newMVars binderInfos
-            (synthAssignedInstances := !tactic.skipAssignedInstances.get (← getOptions))
           let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM fun mvarId => not <$> mvarId.isAssigned
           let otherMVarIds ← getMVarsNoDelayed eqPrf
           let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·)

src/Lean/Meta/Tactic/Simp.lean

@@ -13,7 +13,6 @@ import Lean.Meta.Tactic.Simp.SimpAll
 import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs
 import Lean.Meta.Tactic.Simp.RegisterCommand
-import Lean.Meta.Tactic.Simp.Attr
 
 namespace Lean
 

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

@@ -1,74 +0,0 @@
-/-
-Copyright (c) 2024 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.Simp.Types
-import Lean.Meta.Tactic.Simp.SimpTheorems
-import Lean.Meta.Tactic.Simp.Simproc
-
-namespace Lean.Meta
-open Simp
-
-def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension)
-    (ref : Name := by exact decl_name%) : IO Unit :=
-  registerBuiltinAttribute {
-    ref   := ref
-    name  := attrName
-    descr := attrDescr
-    applicationTime := AttributeApplicationTime.afterCompilation
-    add   := fun declName stx attrKind => do
-      if (← isSimproc declName <||> isBuiltinSimproc declName) then
-        let simprocAttrName := simpAttrNameToSimprocAttrName attrName
-        Attribute.add declName simprocAttrName stx attrKind
-      else
-        let go : MetaM Unit := do
-          let info ← getConstInfo declName
-          let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
-          let prio ← getAttrParamOptPrio stx[2]
-          if (← isProp info.type) then
-            addSimpTheorem ext declName post (inv := false) attrKind prio
-          else if info.hasValue then
-            if let some eqns ← getEqnsFor? declName then
-              for eqn in eqns do
-                addSimpTheorem ext eqn post (inv := false) attrKind prio
-              ext.add (SimpEntry.toUnfoldThms declName eqns) attrKind
-              if hasSmartUnfoldingDecl (← getEnv) declName then
-                ext.add (SimpEntry.toUnfold declName) attrKind
-            else
-              ext.add (SimpEntry.toUnfold declName) attrKind
-          else
-            throwError "invalid 'simp', it is not a proposition nor a definition (to unfold)"
-        discard <| go.run {} {}
-    erase := fun declName => do
-      if (← isSimproc declName <||> isBuiltinSimproc declName) then
-        let simprocAttrName := simpAttrNameToSimprocAttrName attrName
-        Attribute.erase declName simprocAttrName
-      else
-        let s := ext.getState (← getEnv)
-        let s ← s.erase (.decl declName)
-        modifyEnv fun env => ext.modifyState env fun _ => s
-  }
-
-def registerSimpAttr (attrName : Name) (attrDescr : String)
-    (ref : Name := by exact decl_name%) : IO SimpExtension := do
-  let ext ← mkSimpExt ref
-  mkSimpAttr attrName attrDescr ext ref -- Remark: it will fail if it is not performed during initialization
-  simpExtensionMapRef.modify fun map => map.insert attrName ext
-  return ext
-
-builtin_initialize simpExtension : SimpExtension ← registerSimpAttr `simp "simplification theorem"
-
-builtin_initialize sevalSimpExtension : SimpExtension ← registerSimpAttr `seval "symbolic evaluator theorem"
-
-def getSimpTheorems : CoreM SimpTheorems :=
-  simpExtension.getTheorems
-
-def getSEvalTheorems : CoreM SimpTheorems :=
-  sevalSimpExtension.getTheorems
-
-def Simp.Context.mkDefault : MetaM Context :=
-  return { config := {}, simpTheorems := #[(← Meta.getSimpTheorems)], congrTheorems := (← Meta.getSimpCongrTheorems) }
-
-end Lean.Meta

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
 import Init.Data.BitVec.Basic
@@ -19,13 +18,39 @@ structure Literal where
   /-- Actual value. -/
   value : BitVec n
 
+/--
+Try to convert an `OfNat.ofNat`-application into a bitvector literal.
+-/
+private def fromOfNatExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
+  guard (e.isAppOfArity ``OfNat.ofNat 3)
+  let type ← whnf e.appFn!.appFn!.appArg!
+  guard (type.isAppOfArity ``BitVec 1)
+  let n ← Nat.fromExpr? type.appArg!
+  let v ← Nat.fromExpr? e.appFn!.appArg!
+  return { n, value := BitVec.ofNat n v }
+
+/--
+Try to convert an `BitVec.ofNat`-application into a bitvector literal.
+-/
+private def fromBitVecExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
+  guard (e.isAppOfArity ``BitVec.ofNat 2)
+  let n ← Nat.fromExpr? e.appFn!.appArg!
+  let v ← Nat.fromExpr? e.appArg!
+  return { n, value := BitVec.ofNat n v }
+
 /--
 Try to convert `OfNat.ofNat`/`BitVec.OfNat` application into a
 bitvector literal.
 -/
-def fromExpr? (e : Expr) : SimpM (Option Literal) := do
-  let some ⟨n, value⟩ ← getBitVecValue? e | return none
-  return some { n, value }
+def fromExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
+  fromBitVecExpr? e <|> fromOfNatExpr? e
+
+/--
+Convert a bitvector literal into an expression.
+-/
+-- Using `BitVec.ofNat` because it is being used in `simp` theorems
+def Literal.toExpr (lit : Literal) : Expr :=
+  mkApp2 (mkConst ``BitVec.ofNat) (mkNatLit lit.n) (mkNatLit lit.value.toNat)
 
 /--
 Helper function for reducing homogenous unary bitvector operators.
@@ -34,7 +59,8 @@ Helper function for reducing homogenous unary bitvector operators.
     (op : {n : Nat} → BitVec n → BitVec n) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some v ← fromExpr? e.appArg! | return .continue
-  return .done { expr := toExpr (op v.value) }
+  let v := { v with value := op v.value }
+  return .done { expr := v.toExpr }
 
 /--
 Helper function for reducing homogenous binary bitvector operators.
@@ -46,7 +72,8 @@ Helper function for reducing homogenous binary bitvector operators.
   let some v₂ ← fromExpr? e.appArg! | return .continue
   if h : v₁.n = v₂.n then
     trace[Meta.debug] "reduce [{declName}] {v₁.value}, {v₂.value}"
-    return .done { expr := toExpr (op v₁.value (h ▸ v₂.value)) }
+    let v := { v₁ with value := op v₁.value (h ▸ v₂.value) }
+    return .done { expr := v.toExpr }
   else
     return .continue
 
@@ -56,7 +83,8 @@ Helper function for reducing homogenous binary bitvector operators.
   unless e.isAppOfArity declName 3 do return .continue
   let some v ← fromExpr? e.appArg! | return .continue
   let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
-  return .done { expr := toExpr (op n v.value) }
+  let lit : Literal := { n, value := op n v.value }
+  return .done { expr := lit.toExpr }
 
 /--
 Helper function for reducing bitvector functions such as `getLsb` and `getMsb`.
@@ -77,7 +105,8 @@ Helper function for reducing bitvector functions such as `shiftLeft` and `rotate
   unless e.isAppOfArity declName arity do return .continue
   let some v ← fromExpr? e.appFn!.appArg! | return .continue
   let some i ← Nat.fromExpr? e.appArg! | return .continue
-  return .done { expr := toExpr (op v.value i) }
+  let v := { v with value := op v.value i }
+  return .done { expr := v.toExpr }
 
 /--
 Helper function for reducing bitvector predicates.
@@ -162,45 +191,48 @@ builtin_simproc [simp, seval] reduceRotateRight (BitVec.rotateRight _ _) :=
 
 /-- Simplification procedure for append on `BitVec`. -/
 builtin_simproc [simp, seval] reduceAppend ((_ ++ _ : BitVec _)) := fun e => do
-  let_expr HAppend.hAppend _ _ _ _ a b ← e | return .continue
-  let some v₁ ← fromExpr? a | return .continue
-  let some v₂ ← fromExpr? b | return .continue
-  return .done { expr := toExpr (v₁.value ++ v₂.value) }
+  unless e.isAppOfArity ``HAppend.hAppend 6 do return .continue
+  let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
+  let some v₂ ← fromExpr? e.appArg! | return .continue
+  let v : Literal := { n := v₁.n + v₂.n, value := v₁.value ++ v₂.value }
+  return .done { expr := v.toExpr }
 
 /-- Simplification procedure for casting `BitVec`s along an equality of the size. -/
 builtin_simproc [simp, seval] reduceCast (cast _ _) := fun e => do
-  let_expr cast _ m _ v ← e | return .continue
-  let some v ← fromExpr? v | return .continue
-  let some m ← Nat.fromExpr? m | return .continue
-  return .done { expr := toExpr (BitVec.ofNat m v.value.toNat) }
+  unless e.isAppOfArity ``cast 4 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let some m ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
+  let v : Literal := { n := m, value := BitVec.ofNat m v.value.toNat }
+  return .done { expr := v.toExpr }
 
 /-- Simplification procedure for `BitVec.toNat`. -/
 builtin_simproc [simp, seval] reduceToNat (BitVec.toNat _) := fun e => do
-  let_expr BitVec.toNat _ v ← e | return .continue
-  let some v ← fromExpr? v | return .continue
+  unless e.isAppOfArity ``BitVec.toNat 2 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
   return .done { expr := mkNatLit v.value.toNat }
 
 /-- Simplification procedure for `BitVec.toInt`. -/
 builtin_simproc [simp, seval] reduceToInt (BitVec.toInt _) := fun e => do
-  let_expr BitVec.toInt _ v ← e | return .continue
-  let some v ← fromExpr? v | return .continue
-  return .done { expr := toExpr v.value.toInt }
+  unless e.isAppOfArity ``BitVec.toInt 2 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  return .done { expr := Int.toExpr v.value.toInt }
 
 /-- Simplification procedure for `BitVec.ofInt`. -/
 builtin_simproc [simp, seval] reduceOfInt (BitVec.ofInt _ _) := fun e => do
-  let_expr BitVec.ofInt n i ← e | return .continue
-  let some n ← Nat.fromExpr? n | return .continue
-  let some i ← Int.fromExpr? i | return .continue
-  return .done { expr := toExpr (BitVec.ofInt n i) }
+  unless e.isAppOfArity ``BitVec.ofInt 2 do return .continue
+  let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let some i ← Int.fromExpr? e.appArg! | return .continue
+  let lit : Literal := { n, value := BitVec.ofInt n i }
+  return .done { expr := lit.toExpr }
 
 /-- Simplification procedure for ensuring `BitVec.ofNat` literals are normalized. -/
 builtin_simproc [simp, seval] reduceOfNat (BitVec.ofNat _ _) := fun e => do
-  let_expr BitVec.ofNat n v ← e | return .continue
-  let some n ← Nat.fromExpr? n | return .continue
-  let some v ← Nat.fromExpr? v | return .continue
+  unless e.isAppOfArity ``BitVec.ofNat 2 do return .continue
+  let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let some v ← Nat.fromExpr? e.appArg! | return .continue
   let bv := BitVec.ofNat n v
   if bv.toNat == v then return .continue -- already normalized
-  return .done { expr := toExpr (BitVec.ofNat n v) }
+  return .done { expr := { n, value := BitVec.ofNat n v : Literal }.toExpr }
 
 /-- Simplification procedure for `<` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceLT (( _ : BitVec _) < _)  := reduceBinPred ``LT.lt 4 (· < ·)
@@ -226,35 +258,39 @@ builtin_simproc [simp, seval] reduceSLE (BitVec.sle _ _) :=
 
 /-- Simplification procedure for `zeroExtend'` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceZeroExtend' (zeroExtend' _ _) := fun e => do
-  let_expr zeroExtend' _ w _ v ← e | return .continue
-  let some v ← fromExpr? v | return .continue
-  let some w ← Nat.fromExpr? w | return .continue
+  unless e.isAppOfArity ``zeroExtend' 4 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let some w ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
   if h : v.n ≤ w then
-    return .done { expr := toExpr (v.value.zeroExtend' h) }
+    let lit : Literal := { n := w, value := v.value.zeroExtend' h }
+    return .done { expr := lit.toExpr }
   else
     return .continue
 
 /-- Simplification procedure for `shiftLeftZeroExtend` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceShiftLeftZeroExtend (shiftLeftZeroExtend _ _) := fun e => do
-  let_expr shiftLeftZeroExtend _ v m ← e | return .continue
-  let some v ← fromExpr? v | return .continue
-  let some m ← Nat.fromExpr? m | return .continue
-  return .done { expr := toExpr (v.value.shiftLeftZeroExtend m) }
+  unless e.isAppOfArity ``shiftLeftZeroExtend 3 do return .continue
+  let some v ← fromExpr? e.appFn!.appArg! | return .continue
+  let some m ← Nat.fromExpr? e.appArg! | return .continue
+  let lit : Literal := { n := v.n + m, value := v.value.shiftLeftZeroExtend m }
+  return .done { expr := lit.toExpr }
 
 /-- Simplification procedure for `extractLsb'` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceExtracLsb' (extractLsb' _ _ _) := fun e => do
-  let_expr extractLsb' _ start len v ← e | return .continue
-  let some v ← fromExpr? v | return .continue
-  let some start ← Nat.fromExpr? start | return .continue
-  let some len ← Nat.fromExpr? len | return .continue
-  return .done { expr := toExpr (v.value.extractLsb' start len) }
+  unless e.isAppOfArity ``extractLsb' 4 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let some start ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
+  let some len ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let lit : Literal := { n := len, value := v.value.extractLsb' start len }
+  return .done { expr := lit.toExpr }
 
 /-- Simplification procedure for `replicate` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceReplicate (replicate _ _) := fun e => do
-  let_expr replicate _ i v ← e | return .continue
-  let some v ← fromExpr? v | return .continue
-  let some i ← Nat.fromExpr? i | return .continue
-  return .done { expr := toExpr (v.value.replicate i) }
+  unless e.isAppOfArity ``replicate 3 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let some w ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let lit : Literal := { n := v.n * w, value := v.value.replicate w }
+  return .done { expr := lit.toExpr }
 
 /-- Simplification procedure for `zeroExtend` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceZeroExtend (zeroExtend _ _) := reduceExtend ``zeroExtend zeroExtend
@@ -264,8 +300,9 @@ builtin_simproc [simp, seval] reduceSignExtend (signExtend _ _) := reduceExtend
 
 /-- Simplification procedure for `allOnes` -/
 builtin_simproc [simp, seval] reduceAllOnes (allOnes _) := fun e => do
-  let_expr allOnes n ← e | return .continue
-  let some n ← Nat.fromExpr? n | return .continue
-  return .done { expr := toExpr (allOnes n) }
+  unless e.isAppOfArity ``allOnes 1 do return .continue
+  let some n ← Nat.fromExpr? e.appArg! | return .continue
+  let lit : Literal := { n, value := allOnes n }
+  return .done { expr := lit.toExpr }
 
 end BitVec

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean

@@ -5,14 +5,15 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.ToExpr
-import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
 
 namespace Char
 open Lean Meta Simp
 
-def fromExpr? (e : Expr) : SimpM (Option Char) :=
-  getCharValue? e
+def fromExpr? (e : Expr) : SimpM (Option Char) := OptionT.run do
+  guard (e.isAppOfArity ``Char.ofNat 1)
+  let value ← Nat.fromExpr? e.appArg!
+  return Char.ofNat value
 
 @[inline] def reduceUnary [ToExpr α] (declName : Name) (op : Char → α) (arity : Nat := 1) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
@@ -42,9 +43,9 @@ builtin_simproc [simp, seval] reduceIsDigit (Char.isDigit _) := reduceUnary ``Ch
 builtin_simproc [simp, seval] reduceIsAlphaNum (Char.isAlphanum _) := reduceUnary ``Char.isAlphanum Char.isAlphanum
 builtin_simproc [simp, seval] reduceToString (toString (_ : Char)) := reduceUnary ``toString toString 3
 builtin_simproc [simp, seval] reduceVal (Char.val _) := fun e => do
-  let_expr Char.val arg ← e | return .continue
-  let some c ← fromExpr? arg | return .continue
-  return .done { expr := toExpr c.val }
+  unless e.isAppOfArity ``Char.val 1 do return .continue
+  let some c ← fromExpr? e.appArg! | return .continue
+  return .done { expr := UInt32.toExprCore c.val }
 builtin_simproc [simp, seval] reduceEq  (( _ : Char) = _)  := reduceBinPred ``Eq 3 (. = .)
 builtin_simproc [simp, seval] reduceNe  (( _ : Char) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
 builtin_simproc [simp, seval] reduceBEq  (( _ : Char) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
@@ -60,12 +61,12 @@ builtin_simproc ↓ [simp, seval] isValue (Char.ofNat _ ) := fun e => do
   return .done { expr := e }
 
 builtin_simproc [simp, seval] reduceOfNatAux (Char.ofNatAux _ _) := fun e => do
-  let_expr Char.ofNatAux n _ ← e | return .continue
-  let some n ← Nat.fromExpr? n | return .continue
+  unless e.isAppOfArity ``Char.ofNatAux 2 do return .continue
+  let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
   return .done { expr := toExpr (Char.ofNat n) }
 
 builtin_simproc [simp, seval] reduceDefault ((default : Char)) := fun e => do
-  let_expr default _ _ ← e | return .continue
+  unless e.isAppOfArity ``default 2 do return .continue
   return .done { expr := toExpr (default : Char) }
 
 end Char

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean

@@ -10,29 +10,33 @@ import Lean.Meta.Tactic.Simp.Simproc
 open Lean Meta Simp
 
 builtin_simproc ↓ [simp, seval] reduceIte (ite _ _ _) := fun e => do
-  let_expr f@ite α c i tb eb ← e | return .continue
+  unless e.isAppOfArity ``ite 5 do return .continue
+  let c := e.getArg! 1
   let r ← simp c
   if r.expr.isTrue then
-    let pr    := mkApp (mkApp5 (mkConst ``ite_cond_eq_true f.constLevels!) α c i tb eb) (← r.getProof)
-    return .visit { expr := tb, proof? := pr }
+    let eNew  := e.getArg! 3
+    let pr    := mkApp (mkAppN (mkConst ``ite_cond_eq_true e.getAppFn.constLevels!) e.getAppArgs) (← r.getProof)
+    return .visit { expr := eNew, proof? := pr }
   if r.expr.isFalse then
-    let pr    := mkApp (mkApp5 (mkConst ``ite_cond_eq_false f.constLevels!) α c i tb eb) (← r.getProof)
-    return .visit { expr := eb, proof? := pr }
+    let eNew  := e.getArg! 4
+    let pr    := mkApp (mkAppN (mkConst ``ite_cond_eq_false e.getAppFn.constLevels!) e.getAppArgs) (← r.getProof)
+    return .visit { expr := eNew, proof? := pr }
   return .continue
 
 builtin_simproc ↓ [simp, seval] reduceDite (dite _ _ _) := fun e => do
-  let_expr f@dite α c i tb eb ← e | return .continue
+  unless e.isAppOfArity ``dite 5 do return .continue
+  let c := e.getArg! 1
   let r ← simp c
   if r.expr.isTrue then
     let pr    ← r.getProof
     let h     := mkApp2 (mkConst ``of_eq_true) c pr
-    let eNew  := mkApp tb h |>.headBeta
-    let prNew := mkApp (mkApp5 (mkConst ``dite_cond_eq_true f.constLevels!) α c i tb eb) pr
+    let eNew  := mkApp (e.getArg! 3) h |>.headBeta
+    let prNew := mkApp (mkAppN (mkConst ``dite_cond_eq_true e.getAppFn.constLevels!) e.getAppArgs) pr
     return .visit { expr := eNew, proof? := prNew }
   if r.expr.isFalse then
     let pr    ← r.getProof
     let h     := mkApp2 (mkConst ``of_eq_false) c pr
-    let eNew  := mkApp eb h |>.headBeta
-    let prNew := mkApp (mkApp5 (mkConst ``dite_cond_eq_false f.constLevels!) α c i tb eb) pr
+    let eNew  := mkApp (e.getArg! 4) h |>.headBeta
+    let prNew := mkApp (mkAppN (mkConst ``dite_cond_eq_false e.getAppFn.constLevels!) e.getAppArgs) pr
     return .visit { expr := eNew, proof? := prNew }
   return .continue

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean

@@ -5,29 +5,37 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.ToExpr
-import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 
 namespace Fin
 open Lean Meta Simp
 
 structure Value where
-  n     : Nat
-  value : Fin n
+  ofNatFn   : Expr
+  size      : Nat
+  value     : Nat
 
-def fromExpr? (e : Expr) : SimpM (Option Value) := do
-  let some ⟨n, value⟩ ← getFinValue? e | return none
-  return some { n, value }
+def fromExpr? (e : Expr) : SimpM (Option Value) := OptionT.run do
+  guard (e.isAppOfArity ``OfNat.ofNat 3)
+  let type ← whnf e.appFn!.appFn!.appArg!
+  guard (type.isAppOfArity ``Fin 1)
+  let size ← Nat.fromExpr? type.appArg!
+  guard (size > 0)
+  let value ← Nat.fromExpr? e.appFn!.appArg!
+  let value := value % size
+  return { size, value, ofNatFn := e.appFn!.appFn! }
 
-@[inline] def reduceBin (declName : Name) (arity : Nat) (op : {n : Nat} → Fin n → Fin n → Fin n) (e : Expr) : SimpM Step := do
+def Value.toExpr (v : Value) : Expr :=
+  let vExpr := mkRawNatLit v.value
+  mkApp2 v.ofNatFn vExpr (mkApp2 (mkConst ``Fin.instOfNat) (Lean.toExpr (v.size - 1)) vExpr)
+
+@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
-  if h : v₁.n = v₂.n then
-    let v := op v₁.value (h ▸ v₂.value)
-    return .done { expr := toExpr v }
-  else
-    return .continue
+  unless v₁.size == v₂.size do return .continue
+  let v := { v₁ with value := op v₁.value v₂.value % v₁.size }
+  return .done { expr := v.toExpr }
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
@@ -63,12 +71,12 @@ builtin_simproc [simp, seval] reduceBNe  (( _ : Fin _) != _)  := reduceBoolPred
 
 /-- Simplification procedure for ensuring `Fin` literals are normalized. -/
 builtin_simproc [simp, seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do
-  let some ⟨n, v⟩ ← getFinValue? e | return .continue
-  let some m ← getNatValue? e.appFn!.appArg! | return .continue
-  if n == m then
+  let some v ← fromExpr? e | return .continue
+  let v' ← Nat.fromExpr? e.appFn!.appArg!
+  if v.value == v' then
     -- Design decision: should we return `.continue` instead of `.done` when simplifying.
     -- In the symbolic evaluator, we must return `.done`, otherwise it will unfold the `OfNat.ofNat`
     return .done { expr := e }
-  return .done { expr := toExpr v }
+  return .done { expr := v.toExpr }
 
 end Fin

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean

@@ -5,14 +5,33 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.ToExpr
-import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 
 namespace Int
 open Lean Meta Simp
 
-def fromExpr? (e : Expr) : SimpM (Option Int) :=
-  getIntValue? e
+def fromExpr? (e : Expr) : SimpM (Option Int) := OptionT.run do
+  let mut e := e
+  let mut isNeg := false
+  if e.isAppOfArity ``Neg.neg 3 then
+    e := e.appArg!
+    isNeg := true
+  guard (e.isAppOfArity ``OfNat.ofNat 3)
+  let type ← whnf e.appFn!.appFn!.appArg!
+  guard (type.isConstOf ``Int)
+  let value ← Nat.fromExpr? e.appFn!.appArg!
+  let mut value : Int := value
+  if isNeg then value := - value
+  return value
+
+def toExpr (v : Int) : Expr :=
+  let n := v.natAbs
+  let r := mkRawNatLit n
+  let e := mkApp3 (mkConst ``OfNat.ofNat [levelZero]) (mkConst ``Int) r (mkApp (mkConst ``instOfNat) r)
+  if v < 0 then
+    mkAppN (mkConst ``Neg.neg [levelZero]) #[mkConst ``Int, mkConst ``instNegInt, e]
+  else
+    e
 
 @[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Int → Int) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
@@ -57,7 +76,7 @@ builtin_simproc [simp, seval] reduceNeg ((- _ : Int)) := fun e => do
 
 /-- Return `.done` for positive Int values. We don't want to unfold in the symbolic evaluator. -/
 builtin_simproc [seval] isPosValue ((OfNat.ofNat _ : Int)) := fun e => do
-  let_expr OfNat.ofNat _ _ _ ← e | return .continue
+  unless e.isAppOfArity ``OfNat.ofNat 3 do return .continue
   return .done { expr := e }
 
 builtin_simproc [simp, seval] reduceAdd ((_ + _ : Int)) := reduceBin ``HAdd.hAdd 6 (· + ·)
@@ -67,9 +86,9 @@ builtin_simproc [simp, seval] reduceDiv ((_ / _ : Int)) := reduceBin ``HDiv.hDiv
 builtin_simproc [simp, seval] reduceMod ((_ % _ : Int)) := reduceBin ``HMod.hMod 6 (· % ·)
 
 builtin_simproc [simp, seval] reducePow ((_ : Int) ^ (_ : Nat)) := fun e => do
-  let_expr HPow.hPow _ _ _ _ a b ← e | return .continue
-  let some v₁ ← fromExpr? a | return .continue
-  let some v₂ ← Nat.fromExpr? b | return .continue
+  unless e.isAppOfArity ``HPow.hPow 6 do return .continue
+  let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
+  let some v₂ ← Nat.fromExpr? e.appArg! | return .continue
   return .done { expr := toExpr (v₁ ^ v₂) }
 
 builtin_simproc [simp, seval] reduceLT  (( _ : Int) < _)  := reduceBinPred ``LT.lt 4 (. < .)

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Simproc
-import Lean.Meta.LitValues
 import Lean.Meta.Offset
 import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Util
@@ -13,19 +12,20 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Util
 namespace Nat
 open Lean Meta Simp
 
-def fromExpr? (e : Expr) : SimpM (Option Nat) :=
-  getNatValue? e
+def fromExpr? (e : Expr) : SimpM (Option Nat) := do
+  let some n ← evalNat e |>.run | return none
+  return n
 
 @[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Nat → Nat) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appArg! | return .continue
-  return .done { expr := toExpr (op n) }
+  return .done { expr := mkNatLit (op n) }
 
 @[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue
   let some m ← fromExpr? e.appArg! | return .continue
-  return .done { expr := toExpr (op n m) }
+  return .done { expr := mkNatLit (op n m) }
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
@@ -65,7 +65,7 @@ builtin_simproc [simp, seval] reduceBNe  (( _ : Nat) != _)  := reduceBoolPred ``
 
 /-- Return `.done` for Nat values. We don't want to unfold in the symbolic evaluator. -/
 builtin_simproc [seval] isValue ((OfNat.ofNat _ : Nat)) := fun e => do
-  let_expr OfNat.ofNat _ _ _ ← e | return .continue
+  unless e.isAppOfArity ``OfNat.ofNat 3 do return .continue
   return .done { expr := e }
 
 end Nat

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean

@@ -10,8 +10,9 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
 namespace String
 open Lean Meta Simp
 
-def fromExpr? (e : Expr) : SimpM (Option String) := do
-  return getStringValue? e
+def fromExpr? (e : Expr) : SimpM (Option String) := OptionT.run do
+  let .lit (.strVal s) := e | failure
+  return s
 
 builtin_simproc [simp, seval] reduceAppend ((_ ++ _ : String)) := fun e => do
   unless e.isAppOfArity ``HAppend.hAppend 6 do return .continue

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 
 open Lean Meta Simp
@@ -14,30 +13,49 @@ let ofNat := typeName.getId ++ `ofNat
 let ofNatCore := mkIdent (typeName.getId ++ `ofNatCore)
 let toNat := mkIdent (typeName.getId ++ `toNat)
 let fromExpr := mkIdent `fromExpr
+let toExprCore := mkIdent `toExprCore
+let toExpr := mkIdent `toExpr
 `(
 namespace $typeName
 
-def $fromExpr (e : Expr) : SimpM (Option $typeName) := do
-  let some (n, _) ← getOfNatValue? e $(quote typeName.getId) | return none
-  return $(mkIdent ofNat) n
+structure Value where
+  ofNatFn : Expr
+  value   : $typeName
+
+def $fromExpr (e : Expr) : OptionT SimpM Value := do
+  guard (e.isAppOfArity ``OfNat.ofNat 3)
+  let type ← whnf e.appFn!.appFn!.appArg!
+  guard (type.isConstOf $(quote typeName.getId))
+  let value ← Nat.fromExpr? e.appFn!.appArg!
+  let value := $(mkIdent ofNat) value
+  return { value, ofNatFn := e.appFn!.appFn! }
+
+def $toExprCore (v : $typeName) : Expr :=
+  let vExpr := mkRawNatLit v.val
+  mkApp3 (mkConst ``OfNat.ofNat [levelZero]) (mkConst $(quote typeName.getId)) vExpr (mkApp (mkConst $(quote (typeName.getId ++ `instOfNat))) vExpr)
+
+def $toExpr (v : Value) : Expr :=
+  let vExpr := mkRawNatLit v.value.val
+  mkApp2 v.ofNatFn vExpr (mkApp (mkConst $(quote (typeName.getId ++ `instOfNat))) vExpr)
 
 @[inline] def reduceBin (declName : Name) (arity : Nat) (op : $typeName → $typeName → $typeName) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← ($fromExpr e.appFn!.appArg!) | return .continue
   let some m ← ($fromExpr e.appArg!) | return .continue
-  return .done { expr := toExpr (op n m) }
+  let r := { n with value := op n.value m.value }
+  return .done { expr := $toExpr r }
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : $typeName → $typeName → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← ($fromExpr e.appFn!.appArg!) | return .continue
   let some m ← ($fromExpr e.appArg!) | return .continue
-  evalPropStep e (op n m)
+  evalPropStep e (op n.value m.value)
 
 @[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : $typeName → $typeName → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← ($fromExpr e.appFn!.appArg!) | return .continue
   let some m ← ($fromExpr e.appArg!) | return .continue
-  return .done { expr := toExpr (op n m) }
+  return .done { expr := Lean.toExpr (op n.value m.value) }
 
 builtin_simproc [simp, seval] $(mkIdent `reduceAdd):ident ((_ + _ : $typeName)) := reduceBin ``HAdd.hAdd 6 (· + ·)
 builtin_simproc [simp, seval] $(mkIdent `reduceMul):ident ((_ * _ : $typeName)) := reduceBin ``HMul.hMul 6 (· * ·)
@@ -58,13 +76,14 @@ builtin_simproc [simp, seval] $(mkIdent `reduceOfNatCore):ident ($ofNatCore _ _)
   unless e.isAppOfArity $(quote ofNatCore.getId) 2 do return .continue
   let some value ← Nat.fromExpr? e.appFn!.appArg! | return .continue
   let value := $(mkIdent ofNat) value
-  return .done { expr := toExpr value }
+  let eNew := $toExprCore value
+  return .done { expr := eNew }
 
 builtin_simproc [simp, seval] $(mkIdent `reduceToNat):ident ($toNat _) := fun e => do
   unless e.isAppOfArity $(quote toNat.getId) 1 do return .continue
   let some v ← ($fromExpr e.appArg!) | return .continue
-  let n := $toNat v
-  return .done { expr := toExpr n }
+  let n := $toNat v.value
+  return .done { expr := mkNatLit n }
 
 /-- Return `.done` for UInt values. We don't want to unfold in the symbolic evaluator. -/
 builtin_simproc [seval] isValue ((OfNat.ofNat _ : $typeName)) := fun e => do

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

@@ -69,18 +69,16 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
           unless e.getAppNumArgs > projInfo.numParams do
             return none
           let major := e.getArg! projInfo.numParams
-          unless (← isConstructorApp major) do
+          unless major.isConstructorApp (← getEnv) do
             return none
           reduceProjCont? (← withDefault <| unfoldDefinition? e)
       else
         -- `structure` projections
         reduceProjCont? (← unfoldDefinition? e)
 
-private def reduceFVar (cfg : Config) (thms : SimpTheoremsArray) (e : Expr) : SimpM Expr := do
+private def reduceFVar (cfg : Config) (thms : SimpTheoremsArray) (e : Expr) : MetaM Expr := do
   let localDecl ← getFVarLocalDecl e
   if cfg.zetaDelta || thms.isLetDeclToUnfold e.fvarId! || localDecl.isImplementationDetail then
-    if !cfg.zetaDelta && thms.isLetDeclToUnfold e.fvarId! then
-      recordSimpTheorem (.fvar localDecl.fvarId)
     let some v := localDecl.value? | return e
     return v
   else
@@ -504,7 +502,7 @@ def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Resul
     unless modified do
       trace[Meta.Tactic.simp.congr] "{c.theoremName} not modified"
       return none
-    unless (← synthesizeArgs (.decl c.theoremName) bis xs) do
+    unless (← synthesizeArgs (.decl c.theoremName) xs bis) do
       trace[Meta.Tactic.simp.congr] "{c.theoremName} synthesizeArgs failed"
       return none
     let eNew ← instantiateMVars rhs

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

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Simp.SimpTheorems
 import Lean.Meta.Tactic.Simp.Simproc
-import Lean.Meta.Tactic.Simp.Attr
 
 namespace Lean.Meta.Simp
 

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

@@ -8,82 +8,24 @@ import Lean.Meta.ACLt
 import Lean.Meta.Match.MatchEqsExt
 import Lean.Meta.AppBuilder
 import Lean.Meta.SynthInstance
-import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.UnifyEq
 import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.LinearArith.Simp
 import Lean.Meta.Tactic.Simp.Simproc
-import Lean.Meta.Tactic.Simp.Attr
 
 namespace Lean.Meta.Simp
 
-/--
-Helper type for implementing `discharge?'`
--/
-inductive DischargeResult where
-  | proved
-  | notProved
-  | maxDepth
-  | failedAssign
-  deriving DecidableEq
-
-/--
-Wrapper for invoking `discharge?`. It checks for maximum discharge depth, create trace nodes, and ensure
-the generated proof was successfully assigned to `x`.
--/
-def discharge?' (thmId : Origin) (x : Expr) (type : Expr) : SimpM Bool := do
-  let r : DischargeResult ← withTraceNode `Meta.Tactic.simp.discharge (fun
-      | .ok .proved       => return m!"{← ppOrigin thmId} discharge {checkEmoji}{indentExpr type}"
-      | .ok .notProved    => return m!"{← ppOrigin thmId} discharge {crossEmoji}{indentExpr type}"
-      | .ok .maxDepth     => return m!"{← ppOrigin thmId} discharge {crossEmoji} max depth{indentExpr type}"
-      | .ok .failedAssign => return m!"{← ppOrigin thmId} discharge {crossEmoji} failed to assign proof{indentExpr type}"
-      | .error err        => return m!"{← ppOrigin thmId} discharge {crossEmoji}{indentExpr type}{indentD err.toMessageData}") do
-    let ctx ← getContext
-    if ctx.dischargeDepth >= ctx.maxDischargeDepth then
-      return .maxDepth
-    else withTheReader Context (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 }) do
-      -- We save the state, so that `UsedTheorems` does not accumulate
-      -- `simp` lemmas used during unsuccessful discharging.
-      let usedTheorems := (← get).usedTheorems
-      match (← discharge? type) with
-      | some proof =>
-        unless (← isDefEq x proof) do
-          modify fun s => { s with usedTheorems }
-          return .failedAssign
-        return .proved
-      | none =>
-        modify fun s => { s with usedTheorems }
-        return .notProved
-  return r = .proved
-
-def synthesizeArgs (thmId : Origin) (bis : Array BinderInfo) (xs : Array Expr) : SimpM Bool := do
-  let skipAssignedInstances := tactic.skipAssignedInstances.get (← getOptions)
+def synthesizeArgs (thmId : Origin) (xs : Array Expr) (bis : Array BinderInfo) : SimpM Bool := do
   for x in xs, bi in bis do
     let type ← inferType x
-    -- We use the flag `tactic.skipAssignedInstances` for backward compatibility.
-    -- See comment below.
-    if !skipAssignedInstances && bi.isInstImplicit then
+    -- Note that the binderInfo may be misleading here:
+    -- `simp [foo _]` uses `abstractMVars` to turn the elaborated term with
+    -- mvars into the lambda expression `fun α x inst => foo x`, and all
+    -- its bound variables have default binderInfo!
+    if bi.isInstImplicit then
       unless (← synthesizeInstance x type) do
         return false
-    /-
-    We used to invoke `synthesizeInstance` for every instance implicit argument,
-    to ensure the synthesized instance was definitionally equal to the one in
-    the term, but it turned out to be to inconvenient in practice. Here is an
-    example:
-    ```
-    theorem dec_and (p q : Prop) [Decidable (p ∧ q)] [Decidable p] [Decidable q] : decide (p ∧ q) = (p && q) := by
-      by_cases p <;> by_cases q <;> simp [*]
-
-    theorem dec_not (p : Prop) [Decidable (¬p)] [Decidable p] : decide (¬p) = !p := by
-      by_cases p <;> simp [*]
-
-    example [Decidable u] [Decidable v] : decide (u ∧ (v → False)) = (decide u && !decide v) := by
-      simp only [imp_false]
-      simp only [dec_and]
-      simp only [dec_not]
-    ```
-    -/
-    if (← instantiateMVars x).isMVar then
+    else if (← instantiateMVars x).isMVar then
       -- A hypothesis can be both a type class instance as well as a proposition,
       -- in that case we try both TC synthesis and the discharger
       -- (because we don't know whether the argument was originally explicit or instance-implicit).
@@ -91,7 +33,18 @@ def synthesizeArgs (thmId : Origin) (bis : Array BinderInfo) (xs : Array Expr) :
         if (← synthesizeInstance x type) then
           continue
       if (← isProp type) then
-        unless (← discharge?' thmId x type) do
+        -- We save the state, so that `UsedTheorems` does not accumulate
+        -- `simp` lemmas used during unsuccessful discharging.
+        let usedTheorems := (← get).usedTheorems
+        match (← discharge? type) with
+        | some proof =>
+          unless (← isDefEq x proof) do
+            trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to assign proof{indentExpr type}"
+            modify fun s => { s with usedTheorems }
+            return false
+        | none =>
+          trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to discharge hypotheses{indentExpr type}"
+          modify fun s => { s with usedTheorems }
           return false
   return true
 where
@@ -110,7 +63,7 @@ where
 private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
   let rec go (e : Expr) : SimpM (Option Result) := do
     if (← isDefEq lhs e) then
-      unless (← synthesizeArgs thm.origin bis xs) do
+      unless (← synthesizeArgs thm.origin xs bis) do
         return none
       let proof? ← if thm.rfl then
         pure none
@@ -203,11 +156,22 @@ where
   inErasedSet (thm : SimpTheorem) : Bool :=
     erased.contains thm.origin
 
+-- TODO: workaround for `Expr.constructorApp?` limitations. We should handle `OfNat.ofNat` there
+private def reduceOfNatNat (e : Expr) : MetaM Expr := do
+  unless e.isAppOfArity ``OfNat.ofNat 3 do
+    return e
+  unless (← whnfD (e.getArg! 0)).isConstOf ``Nat do
+    return e
+  return e.getArg! 1
+
 def simpCtorEq : Simproc := fun e => withReducibleAndInstances do
   match e.eq? with
   | none => return .continue
   | some (_, lhs, rhs) =>
-    match (← constructorApp'? lhs), (← constructorApp'? rhs) with
+    let lhs ← reduceOfNatNat (← whnf lhs)
+    let rhs ← reduceOfNatNat (← whnf rhs)
+    let env ← getEnv
+    match lhs.constructorApp? env, rhs.constructorApp? env with
     | some (c₁, _), some (c₂, _) =>
       if c₁.name != c₂.name then
         withLocalDeclD `h e fun h =>
@@ -323,6 +287,7 @@ def rewritePost (rflOnly := false) : Simproc := fun e => do
 Discharge procedure for the ground/symbolic evaluator.
 -/
 def dischargeGround (e : Expr) : SimpM (Option Expr) := do
+  trace[Meta.Tactic.simp.discharge] ">> discharge?: {e}"
   let r ← simp e
   if r.expr.isTrue then
     try
@@ -514,11 +479,21 @@ def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
       return some r
     if let some r ← dischargeEqnThmHypothesis? e then
       return some r
-  let r ← simp e
-  if r.expr.isTrue then
-    return some (← mkOfEqTrue (← r.getProof))
-  else
+  let ctx ← getContext
+  trace[Meta.Tactic.simp.discharge] ">> discharge?: {e}"
+  if ctx.dischargeDepth >= ctx.maxDischargeDepth then
+    trace[Meta.Tactic.simp.discharge] "maximum discharge depth has been reached"
     return none
+  else
+    withTheReader Context (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 }) do
+      let r ← simp e
+      if r.expr.isTrue then
+        try
+          return some (← mkOfEqTrue (← r.getProof))
+        catch _ =>
+          return none
+      else
+        return none
 
 abbrev Discharge := Expr → SimpM (Option Expr)
 

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

@@ -362,6 +362,37 @@ def addSimpTheorem (ext : SimpExtension) (declName : Name) (post : Bool) (inv :
   for simpThm in simpThms do
     ext.add (SimpEntry.thm simpThm) attrKind
 
+def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension)
+    (ref : Name := by exact decl_name%) : IO Unit :=
+  registerBuiltinAttribute {
+    ref   := ref
+    name  := attrName
+    descr := attrDescr
+    applicationTime := AttributeApplicationTime.afterCompilation
+    add   := fun declName stx attrKind =>
+      let go : MetaM Unit := do
+        let info ← getConstInfo declName
+        let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
+        let prio ← getAttrParamOptPrio stx[2]
+        if (← isProp info.type) then
+          addSimpTheorem ext declName post (inv := false) attrKind prio
+        else if info.hasValue then
+          if let some eqns ← getEqnsFor? declName then
+            for eqn in eqns do
+              addSimpTheorem ext eqn post (inv := false) attrKind prio
+            ext.add (SimpEntry.toUnfoldThms declName eqns) attrKind
+            if hasSmartUnfoldingDecl (← getEnv) declName then
+              ext.add (SimpEntry.toUnfold declName) attrKind
+          else
+            ext.add (SimpEntry.toUnfold declName) attrKind
+        else
+          throwError "invalid 'simp', it is not a proposition nor a definition (to unfold)"
+      discard <| go.run {} {}
+    erase := fun declName => do
+      let s := ext.getState (← getEnv)
+      let s ← s.erase (.decl declName)
+      modifyEnv fun env => ext.modifyState env fun _ => s
+  }
 
 def mkSimpExt (name : Name := by exact decl_name%) : IO SimpExtension :=
   registerSimpleScopedEnvExtension {
@@ -378,9 +409,26 @@ abbrev SimpExtensionMap := HashMap Name SimpExtension
 
 builtin_initialize simpExtensionMapRef : IO.Ref SimpExtensionMap ← IO.mkRef {}
 
+def registerSimpAttr (attrName : Name) (attrDescr : String)
+    (ref : Name := by exact decl_name%) : IO SimpExtension := do
+  let ext ← mkSimpExt ref
+  mkSimpAttr attrName attrDescr ext ref -- Remark: it will fail if it is not performed during initialization
+  simpExtensionMapRef.modify fun map => map.insert attrName ext
+  return ext
+
+builtin_initialize simpExtension : SimpExtension ← registerSimpAttr `simp "simplification theorem"
+
+builtin_initialize sevalSimpExtension : SimpExtension ← registerSimpAttr `seval "symbolic evaluator theorem"
+
 def getSimpExtension? (attrName : Name) : IO (Option SimpExtension) :=
   return (← simpExtensionMapRef.get).find? attrName
 
+def getSimpTheorems : CoreM SimpTheorems :=
+  simpExtension.getTheorems
+
+def getSEvalTheorems : CoreM SimpTheorems :=
+  sevalSimpExtension.getTheorems
+
 /-- Auxiliary method for adding a global declaration to a `SimpTheorems` datastructure. -/
 def SimpTheorems.addConst (s : SimpTheorems) (declName : Name) (post := true) (inv := false) (prio : Nat := eval_prio default) : MetaM SimpTheorems := do
   let s := { s with erased := s.erased.erase (.decl declName post inv) }

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

@@ -127,29 +127,25 @@ def toSimprocEntry (e : SimprocOLeanEntry) : ImportM SimprocEntry := do
 def eraseSimprocAttr (ext : SimprocExtension) (declName : Name) : AttrM Unit := do
   let s := ext.getState (← getEnv)
   unless s.simprocNames.contains declName do
-    throwError "'{declName}' does not have a simproc attribute"
+    throwError "'{declName}' does not have [simproc] attribute"
   modifyEnv fun env => ext.modifyState env fun s => s.erase declName
 
-def addSimprocAttrCore (ext : SimprocExtension) (declName : Name) (kind : AttributeKind) (post : Bool) : CoreM Unit := do
+def addSimprocAttr (ext : SimprocExtension) (declName : Name) (kind : AttributeKind) (post : Bool) : CoreM Unit := do
   let proc ← getSimprocFromDecl declName
   let some keys ← getSimprocDeclKeys? declName |
     throwError "invalid [simproc] attribute, '{declName}' is not a simproc"
   ext.add { declName, post, keys, proc } kind
 
-def Simprocs.addCore (s : Simprocs) (keys : Array SimpTheoremKey) (declName : Name) (post : Bool) (proc : Simproc) : Simprocs :=
-  let s := { s with simprocNames := s.simprocNames.insert declName, erased := s.erased.erase declName }
-  if post then
-    { s with post := s.post.insertCore keys { declName, keys, post, proc } }
-  else
-    { s with pre := s.pre.insertCore keys { declName, keys, post, proc } }
-
 /--
 Implements attributes `builtin_simproc` and `builtin_sevalproc`.
 -/
 def addSimprocBuiltinAttrCore (ref : IO.Ref Simprocs) (declName : Name) (post : Bool) (proc : Simproc) : IO Unit := do
   let some keys := (← builtinSimprocDeclsRef.get).keys.find? declName |
     throw (IO.userError "invalid [builtin_simproc] attribute, '{declName}' is not a builtin simproc")
-  ref.modify fun s => s.addCore keys declName post proc
+  if post then
+    ref.modify fun s => { s with post := s.post.insertCore keys { declName, keys, post, proc } }
+  else
+    ref.modify fun s => { s with pre := s.pre.insertCore keys { declName, keys, post, proc } }
 
 def addSimprocBuiltinAttr (declName : Name) (post : Bool) (proc : Simproc) : IO Unit :=
   addSimprocBuiltinAttrCore builtinSimprocsRef declName post proc
@@ -170,7 +166,10 @@ def Simprocs.add (s : Simprocs) (declName : Name) (post : Bool) : CoreM Simprocs
         throw e
   let some keys ← getSimprocDeclKeys? declName |
     throwError "invalid [simproc] attribute, '{declName}' is not a simproc"
-  return s.addCore keys declName post proc
+  if post then
+    return { s with post := s.post.insertCore keys { declName, keys, post, proc } }
+  else
+    return { s with pre := s.pre.insertCore keys { declName, keys, post, proc } }
 
 def SimprocEntry.try (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM Step := do
   let mut extraArgs := #[]
@@ -256,7 +255,6 @@ def simprocArrayCore (post : Bool) (ss : SimprocsArray) (e : Expr) : SimpM Step
 
 register_builtin_option simprocs : Bool := {
   defValue := true
-  group    := "backward compatibility"
   descr    := "Enable/disable `simproc`s (simplification procedures)."
 }
 
@@ -278,22 +276,24 @@ def mkSimprocExt (name : Name := by exact decl_name%) (ref? : Option (IO.Ref Sim
         return {}
     ofOLeanEntry  := fun _ => toSimprocEntry
     toOLeanEntry  := fun e => e.toSimprocOLeanEntry
-    addEntry      := fun s e => s.addCore e.keys e.declName e.post e.proc
+    addEntry      := fun s e =>
+      if e.post then
+        { s with post := s.post.insertCore e.keys e }
+      else
+        { s with pre := s.pre.insertCore e.keys e }
   }
 
-def addSimprocAttr (ext : SimprocExtension) (declName : Name) (stx : Syntax) (attrKind : AttributeKind) : AttrM Unit := do
-  let go : MetaM Unit := do
-    let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
-    addSimprocAttrCore ext declName attrKind post
-  discard <| go.run {} {}
-
 def mkSimprocAttr (attrName : Name) (attrDescr : String) (ext : SimprocExtension) (name : Name) : IO Unit := do
   registerBuiltinAttribute {
     ref   := name
     name  := attrName
     descr := attrDescr
     applicationTime := AttributeApplicationTime.afterCompilation
-    add   := addSimprocAttr ext
+    add   := fun declName stx attrKind =>
+      let go : MetaM Unit := do
+        let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
+        addSimprocAttr ext declName attrKind post
+      discard <| go.run {} {}
     erase := eraseSimprocAttr ext
   }
 

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

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.AppBuilder
 import Lean.Meta.CongrTheorems
-import Lean.Meta.Eqns
 import Lean.Meta.Tactic.Replace
 import Lean.Meta.Tactic.Simp.SimpTheorems
 import Lean.Meta.Tactic.Simp.SimpCongrTheorems
@@ -93,6 +92,9 @@ structure Context where
 def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
   ctx.simpTheorems.isDeclToUnfold declName
 
+def Context.mkDefault : MetaM Context :=
+  return { config := {}, simpTheorems := #[(← getSimpTheorems)], congrTheorems := (← getSimpCongrTheorems) }
+
 abbrev UsedSimps := HashMap Origin Nat
 
 structure State where
@@ -257,22 +259,7 @@ def getSimpCongrTheorems : SimpM SimpCongrTheorems :=
 @[inline] def withDischarger (discharge? : Expr → SimpM (Option Expr)) (x : SimpM α) : SimpM α :=
   savingCache <| withReader (fun r => { MethodsRef.toMethods r with discharge? }.toMethodsRef) x
 
-def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
-  /-
-  If `thmId` is an equational theorem (e.g., `foo._eq_1`), we should record `foo` instead.
-  See issue #3547.
-  -/
-  let thmId ← match thmId with
-    | .decl declName post false =>
-      /-
-      Remark: if `inv := true`, then the user has manually provided the theorem and wants to
-      use it in the reverse direction. So, we only performs the substitution when `inv := false`
-      -/
-      if let some declName ← isEqnThm? declName then
-        pure (Origin.decl declName post false)
-      else
-        pure thmId
-    | _ => pure thmId
+def recordSimpTheorem (thmId : Origin) : SimpM Unit :=
   modify fun s => if s.usedTheorems.contains thmId then s else
     let n := s.usedTheorems.size
     { s with usedTheorems := s.usedTheorems.insert thmId n }

src/Lean/Meta/Tactic/TryThis.lean

@@ -7,7 +7,11 @@ prelude
 import Lean.Server.CodeActions
 import Lean.Widget.UserWidget
 import Lean.Data.Json.Elab
-import Lean.Data.Lsp.Utf16
+
+/-- Gets the LSP range from a `String.Range`. -/
+def Lean.FileMap.utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
+  { start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
+
 
 /-!
 # "Try this" support

src/Lean/Meta/Tactic/UnifyEq.lean

@@ -70,7 +70,8 @@ def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {})
           else
             throwError "dependent elimination failed, failed to solve equation{indentExpr eqDecl.type}"
         let rec injection (a b : Expr) := do
-          if (← isConstructorApp a <&&> isConstructorApp b) then
+          let env ← getEnv
+          if a.isConstructorApp env && b.isConstructorApp env then
             /- ctor_i ... = ctor_j ... -/
             match (← injectionCore mvarId eqFVarId) with
             | InjectionResultCore.solved                   => return none -- this alternative has been solved

src/Lean/Meta/Tactic/Util.lean

@@ -178,10 +178,4 @@ def _root_.Lean.MVarId.isSubsingleton (g : MVarId) : MetaM Bool := do
   catch _ =>
     return false
 
-register_builtin_option tactic.skipAssignedInstances : Bool := {
-  defValue := true
-  group    := "backward compatibility"
-  descr    := "in the `rw` and `simp` tactics, if an instance implicit argument is assigned, do not try to synthesize instance."
-}
-
 end Lean.Meta

src/Lean/Meta/WHNF.lean

@@ -8,7 +8,6 @@ import Lean.Structure
 import Lean.Util.Recognizers
 import Lean.Meta.GetUnfoldableConst
 import Lean.Meta.FunInfo
-import Lean.Meta.CtorRecognizer
 import Lean.Meta.Match.MatcherInfo
 import Lean.Meta.Match.MatchPatternAttr
 
@@ -134,7 +133,7 @@ private def toCtorWhenStructure (inductName : Name) (major : Expr) : MetaM Expr
   let env ← getEnv
   if !isStructureLike env inductName then
     return major
-  else if let some _ ← isConstructorApp? major then
+  else if let some _ := major.isConstructorApp? env then
     return major
   else
     let majorType ← inferType major
@@ -755,7 +754,7 @@ mutual
                 let numArgs := e.getAppNumArgs
                 if recArgPos >= numArgs then return none
                 let recArg := e.getArg! recArgPos numArgs
-                if !(← isConstructorApp (← whnfMatcher recArg)) then return none
+                if !(← whnfMatcher recArg).isConstructorApp (← getEnv) then return none
                 return some r
             | _ =>
               if (← getMatcherInfo? fInfo.name).isSome then

src/Lean/Modifiers.lean

@@ -47,7 +47,7 @@ def isPrivateNameExport (n : Name) : Bool :=
 Return `true` if `n` is of the form `_private.<module_name>.0`
 See comment above.
 -/
-def isPrivatePrefix (n : Name) : Bool :=
+private def isPrivatePrefix (n : Name) : Bool :=
   match n with
   | .num p 0 => go p
   | _ => false

src/Lean/Parser/Do.lean

@@ -50,7 +50,7 @@ def notFollowedByRedefinedTermToken :=
   -- but we include them in the following list to fix the ambiguity where
   -- an "open" command follows the `do`-block.
   -- If we don't add `do`, then users would have to indent `do` blocks or use `{ ... }`.
-  notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "match_expr" <|> "let" <|> "let_expr" <|> "have" <|>
+  notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "let" <|> "have" <|>
       "do" <|> "dbg_trace" <|> "assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try")
     "token at 'do' element"
 
@@ -60,14 +60,6 @@ def notFollowedByRedefinedTermToken :=
   "let " >> optional "mut " >> termParser >> " := " >> termParser >>
   checkColGt >> " | " >> doSeq
 
-@[builtin_doElem_parser] def doLetExpr  := leading_parser
-  "let_expr " >> matchExprPat >> " := " >> termParser >>
-  checkColGt >> " | " >> doSeq
-
-@[builtin_doElem_parser] def doLetMetaExpr  := leading_parser
-  "let_expr " >> matchExprPat >> " ← " >> termParser >>
-  checkColGt >> " | " >> doSeq
-
 @[builtin_doElem_parser] def doLetRec   := leading_parser
   group ("let " >> nonReservedSymbol "rec ") >> letRecDecls
 def doIdDecl   := leading_parser
@@ -158,12 +150,6 @@ def doMatchAlts := ppDedent <| matchAlts (rhsParser := doSeq)
   "match " >> optional Term.generalizingParam >> optional Term.motive >>
   sepBy1 matchDiscr ", " >> " with" >> doMatchAlts
 
-def doMatchExprAlts := ppDedent <| matchExprAlts (rhsParser := doSeq)
-def optMetaFalse :=
-  optional ("(" >> nonReservedSymbol "meta" >>  " := " >> nonReservedSymbol "false" >> ") ")
-@[builtin_doElem_parser] def doMatchExpr := leading_parser:leadPrec
-  "match_expr " >> optMetaFalse >> termParser >> " with" >> doMatchExprAlts
-
 def doCatch      := leading_parser
   ppDedent ppLine >> atomic ("catch " >> binderIdent) >> optional (" : " >> termParser) >> darrow >> doSeq
 def doCatchMatch := leading_parser

src/Lean/Parser/Tactic.lean

@@ -66,60 +66,13 @@ doing a pattern match. This is equivalent to `fun` with match arms in term mode.
 @[builtin_tactic_parser] def introMatch := leading_parser
   nonReservedSymbol "intro" >> matchAlts
 
-/--
-`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`
-and then reducing that instance to evaluate the truth value of `p`.
-If it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.
-
-Limitations:
-- The target is not allowed to contain local variables or metavariables.
-  If there are local variables, you can try first using the `revert` tactic with these local variables
-  to move them into the target, which may allow `decide` to succeed.
-- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined
-  by well-founded recursion might not work, because evaluating them requires reducing proofs.
-  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.
-  These can appear for instances defined using tactics (such as `rw` and `simp`).
-  To avoid this, use definitions such as `decidable_of_iff` instead.
-
-## Examples
-
-Proving inequalities:
-```lean
+/-- `decide` will attempt to prove a goal of type `p` by synthesizing an instance
+of `Decidable p` and then evaluating it to `isTrue ..`. Because this uses kernel
+computation to evaluate the term, it may not work in the presence of definitions
+by well founded recursion, since this requires reducing proofs.
+```
 example : 2 + 2 ≠ 5 := by decide
 ```
-
-Trying to prove a false proposition:
-```lean
-example : 1 ≠ 1 := by decide
-/-
-tactic 'decide' proved that the proposition
-  1 ≠ 1
-is false
--/
-```
-
-Trying to prove a proposition whose `Decidable` instance fails to reduce
-```lean
-opaque unknownProp : Prop
-
-open scoped Classical in
-example : unknownProp := by decide
-/-
-tactic 'decide' failed for proposition
-  unknownProp
-since its 'Decidable' instance reduced to
-  Classical.choice ⋯
-rather than to the 'isTrue' constructor.
--/
-```
-
-## Properties and relations
-
-For equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.
-```lean
-example : 1 + 1 = 2 := by decide
-example : 1 + 1 = 2 := by rfl
-```
 -/
 @[builtin_tactic_parser] def decide := leading_parser
   nonReservedSymbol "decide"

src/Lean/Parser/Term.lean

@@ -118,18 +118,14 @@ def example (a : Nat) : Nat → Nat → Nat :=
 termination_by b c => a - b
 ```
 
-If omitted, a termination argument will be inferred. If written as `termination_by?`,
-the inferrred termination argument will be suggested.
+If omitted, a termination argument will be inferred.
 -/
 def terminationBy := leading_parser
+  ppDedent ppLine >>
   "termination_by " >>
   optional (atomic (many (ppSpace >> (ident <|> "_")) >> " => ")) >>
   termParser
 
-@[inherit_doc terminationBy]
-def terminationBy? := leading_parser
-  "termination_by?"
-
 /--
 Manually prove that the termination argument (as specified with `termination_by` or inferred)
 decreases at each recursive call.
@@ -143,7 +139,7 @@ def decreasingBy := leading_parser
 Termination hints are `termination_by` and `decreasing_by`, in that order.
 -/
 def suffix := leading_parser
-  optional (ppDedent ppLine >> (terminationBy? <|> terminationBy)) >> optional decreasingBy
+  optional terminationBy >> optional decreasingBy
 
 end Termination
 
@@ -195,13 +191,6 @@ def optSemicolon (p : Parser) : Parser :=
 This syntax is used to construct named metavariables. -/
 @[builtin_term_parser] def syntheticHole := leading_parser
   "?" >> (ident <|> hole)
-/--
-Denotes a term that was omitted by the pretty printer.
-This is only meant to be used for pretty printing, however for copy/paste friendliness it elaborates like `_` while logging a warning.
-The presence of `⋯` in pretty printer output is controlled by the `pp.deepTerms` and `pp.proofs` options.
--/
-@[builtin_term_parser] def omission := leading_parser
-  "⋯"
 def binderIdent : Parser  := ident <|> hole
 /-- A temporary placeholder for a missing proof or value. -/
 @[builtin_term_parser] def «sorry» := leading_parser
@@ -802,6 +791,7 @@ interpolated string literal) to stderr. It should only be used for debugging.
 @[builtin_term_parser] def assert := leading_parser:leadPrec
   withPosition ("assert! " >> termParser) >> optSemicolon termParser
 
+
 def macroArg       := termParser maxPrec
 def macroDollarArg := leading_parser "$" >> termParser 10
 def macroLastArg   := macroDollarArg <|> macroArg
@@ -816,29 +806,6 @@ def macroLastArg   := macroDollarArg <|> macroArg
 @[builtin_term_parser] def dotIdent := leading_parser
   "." >> checkNoWsBefore >> rawIdent
 
-/--
-Implementation of the `show_term` term elaborator.
--/
-@[builtin_term_parser] def showTermElabImpl :=
-  leading_parser:leadPrec "show_term_elab " >> termParser
-
-/-!
-`match_expr` support.
--/
-
-def matchExprPat := leading_parser optional (atomic (ident >> "@")) >> ident >> many binderIdent
-def matchExprAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (matchExprPat >> " => " >> rhsParser)
-def matchExprElseAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (hole >> " => " >> rhsParser)
-def matchExprAlts (rhsParser : Parser) :=
-  leading_parser withPosition $
-    many (ppLine >> checkColGe "irrelevant" >> notFollowedBy (symbol "| " >> " _ ") "irrelevant" >> matchExprAlt rhsParser)
-    >> (ppLine >> checkColGe "irrelevant" >> matchExprElseAlt rhsParser)
-@[builtin_term_parser] def matchExpr := leading_parser:leadPrec
-  "match_expr " >> termParser >> " with" >> ppDedent (matchExprAlts termParser)
-
-@[builtin_term_parser] def letExpr := leading_parser:leadPrec
-  withPosition ("let_expr " >> matchExprPat >> " := " >> termParser >> checkColGt >> " | " >> termParser) >> optSemicolon termParser
-
 end Term
 
 @[builtin_term_parser default+1] def Tactic.quot : Parser := leading_parser
@@ -857,7 +824,6 @@ builtin_initialize
   register_parser_alias matchDiscr
   register_parser_alias bracketedBinder
   register_parser_alias attrKind
-  register_parser_alias optSemicolon
 
 end Parser
 end Lean

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -16,22 +16,12 @@ open Lean.Parser.Term
 open SubExpr
 open TSyntax.Compat
 
-/--
-If `cond` is true, wraps the syntax produced by `d` in a type ascription.
--/
-def withTypeAscription (d : Delab) (cond : Bool := true) : DelabM Term := do
-  let stx ← d
-  if cond then
-    let typeStx ← withType delab
-    `(($stx : $typeStx))
-  else
-    return stx
+def maybeAddBlockImplicit (ident : Syntax) : DelabM Syntax := do
+  if ← getPPOption getPPAnalysisBlockImplicit then `(@$ident:ident) else pure ident
 
-/--
-Wraps the identifier (or identifier with explicit universe levels) with `@` if `pp.analysis.blockImplicit` is set to true.
--/
-def maybeAddBlockImplicit (identLike : Syntax) : DelabM Syntax := do
-  if ← getPPOption getPPAnalysisBlockImplicit then `(@$identLike) else pure identLike
+def unfoldMDatas : Expr → Expr
+  | Expr.mdata _ e => unfoldMDatas e
+  | e              => e
 
 @[builtin_delab fvar]
 def delabFVar : Delab := do
@@ -69,12 +59,8 @@ def delabSort : Delab := do
     | some l' => `(Type $(Level.quote l' max_prec))
     | none    => `(Sort $(Level.quote l max_prec))
 
-/--
-Delaborator for `const` expressions.
-This is not registered as a delaborator, as `const` is not an expression kind
-(see [delab] description and `Lean.PrettyPrinter.Delaborator.getExprKind`).
-Rather, it is called through the `app` delaborator.
--/
+
+-- NOTE: not a registered delaborator, as `const` is never called (see [delab] description)
 def delabConst : Delab := do
   let Expr.const c₀ ls ← getExpr | unreachable!
   let c₀ := if (← getPPOption getPPPrivateNames) then c₀ else (privateToUserName? c₀).getD c₀
@@ -92,11 +78,11 @@ def delabConst : Delab := do
   else
     `($(mkIdent c).{$[$(ls.toArray.map quote)],*})
 
-  let stx ← maybeAddBlockImplicit stx
+  let mut stx ← maybeAddBlockImplicit stx
   if (← getPPOption getPPTagAppFns) then
-    annotateTermInfo stx
-  else
-    return stx
+    stx ← annotateCurPos stx
+    addTermInfo (← getPos) stx (← getExpr)
+  return stx
 
 def withMDataOptions [Inhabited α] (x : DelabM α) : DelabM α := do
   match ← getExpr with
@@ -113,6 +99,12 @@ def withMDataOptions [Inhabited α] (x : DelabM α) : DelabM α := do
 partial def withMDatasOptions [Inhabited α] (x : DelabM α) : DelabM α := do
   if (← getExpr).isMData then withMDataOptions (withMDatasOptions x) else x
 
+def delabAppFn : Delab := do
+  if (← getExpr).consumeMData.isConst then
+    withMDatasOptions delabConst
+  else
+    delab
+
 /--
 A structure that records details of a function parameter.
 -/
@@ -125,7 +117,6 @@ structure ParamKind where
   defVal      : Option Expr := none
   /-- Whether the parameter is an autoparam (i.e., whether it uses a tactic for the default value). -/
   isAutoParam : Bool := false
-  deriving Inhabited
 
 /--
 Returns true if the parameter is an explicit parameter that has neither a default value nor a tactic.
@@ -137,7 +128,7 @@ def ParamKind.isRegularExplicit (param : ParamKind) : Bool :=
 Given a function `f` supplied with arguments `args`, returns an array whose n-th element
 is set to the kind of the n-th argument's associated parameter.
 We do not assume the expression `mkAppN f args` is sensical,
-and this function captures errors (except for panics) and returns the empty array in that case.
+and this function captures errors (except for panics) and returns the empty array.
 
 The returned array might be longer than the number of arguments.
 It gives parameter kinds for the fully-applied function.
@@ -150,24 +141,25 @@ argument when its arguments are specialized to function types, like in `id id 2`
 -/
 def getParamKinds (f : Expr) (args : Array Expr) : MetaM (Array ParamKind) := do
   try
-    let mut result : Array ParamKind := Array.mkEmpty args.size
-    let mut fnType ← inferType f
-    let mut j := 0
-    for i in [0:args.size] do
-      unless fnType.isForall do
-        fnType ← withTransparency .all <| whnf (fnType.instantiateRevRange j i args)
-        j := i
-      let .forallE n t b bi := fnType | failure
-      let defVal := t.getOptParamDefault? |>.map (·.instantiateRevRange j i args)
-      result := result.push { name := n, bInfo := bi, defVal, isAutoParam := t.isAutoParam }
-      fnType := b
-    fnType := fnType.instantiateRevRange j args.size args
-    -- We still want to consider parameters past the ones for the supplied arguments for analysis.
-    forallTelescopeReducing fnType fun xs _ => do
-      xs.foldlM (init := result) fun result x => do
-        let l ← x.fvarId!.getDecl
-        -- Warning: the defVal might refer to fvars that are only valid in this context
-        pure <| result.push { name := l.userName, bInfo := l.binderInfo, defVal := l.type.getOptParamDefault?, isAutoParam := l.type.isAutoParam }
+    withTransparency TransparencyMode.all do
+      let mut result : Array ParamKind := Array.mkEmpty args.size
+      let mut fnType ← inferType f
+      let mut j := 0
+      for i in [0:args.size] do
+        unless fnType.isForall do
+          fnType ← whnf (fnType.instantiateRevRange j i args)
+          j := i
+        let .forallE n t b bi := fnType | failure
+        let defVal := t.getOptParamDefault? |>.map (·.instantiateRevRange j i args)
+        result := result.push { name := n, bInfo := bi, defVal, isAutoParam := t.isAutoParam }
+        fnType := b
+      fnType := fnType.instantiateRevRange j args.size args
+      -- We still want to consider parameters past the ones for the supplied arguments.
+      forallTelescopeReducing fnType fun xs _ => do
+        xs.foldlM (init := result) fun result x => do
+          let l ← x.fvarId!.getDecl
+          -- Warning: the defVal might refer to fvars that are only valid in this context
+          pure <| result.push { name := l.userName, bInfo := l.binderInfo, defVal := l.type.getOptParamDefault?, isAutoParam := l.type.isAutoParam }
   catch _ => pure #[] -- recall that expr may be nonsensical
 
 def shouldShowMotive (motive : Expr) (opts : Options) : MetaM Bool := do
@@ -175,10 +167,46 @@ def shouldShowMotive (motive : Expr) (opts : Options) : MetaM Bool := do
   <||> (pure (getPPMotivesPi opts) <&&> returnsPi motive)
   <||> (pure (getPPMotivesNonConst opts) <&&> isNonConstFun motive)
 
+/--
+Returns true if an application should use explicit mode when delaborating.
+-/
+def useAppExplicit (paramKinds : Array ParamKind) : DelabM Bool := do
+  if ← getPPOption getPPExplicit then
+    if paramKinds.any (fun param => !param.isRegularExplicit) then return true
+
+  -- If the expression has an implicit function type, fall back to delabAppExplicit.
+  -- This is e.g. necessary for `@Eq`.
+  let isImplicitApp ← try
+      let ty ← whnf (← inferType (← getExpr))
+      pure <| ty.isForall && (ty.binderInfo matches .implicit | .instImplicit)
+    catch _ => pure false
+  if isImplicitApp then return true
+
+  return false
+
+/--
+Returns true if the application is a candidate for unexpanders.
+-/
+def isRegularApp (maxArgs : Nat) : DelabM Bool := do
+  let e ← getExpr
+  if not (unfoldMDatas (e.getBoundedAppFn maxArgs)).isConst then return false
+  withBoundedAppFnArgs maxArgs
+    (not <$> withMDatasOptions (getPPOption getPPUniverses <||> getPPOption getPPAnalysisBlockImplicit))
+    (fun b => pure b <&&> not <$> getPPOption getPPAnalysisNamedArg)
+
+def unexpandRegularApp (stx : Syntax) : Delab := do
+  let Expr.const c .. := (unfoldMDatas (← getExpr).getAppFn) | unreachable!
+  let fs := appUnexpanderAttribute.getValues (← getEnv) c
+  let ref ← getRef
+  fs.firstM fun f =>
+    match f stx |>.run ref |>.run () with
+    | EStateM.Result.ok stx _ => pure stx
+    | _ => failure
+
 def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStructureInstances do
   let env ← getEnv
   let e ← getExpr
-  let some s ← isConstructorApp? e | failure
+  let some s ← pure $ e.isConstructorApp? env | failure
   guard $ isStructure env s.induct;
   /- If implicit arguments should be shown, and the structure has parameters, we should not
      pretty print using { ... }, because we will not be able to see the parameters. -/
@@ -199,204 +227,97 @@ def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStruct
     if (← getPPOption getPPStructureInstanceType) then delab >>= pure ∘ some else pure none
   `({ $fields,* $[: $tyStx]? })
 
-/--
-Given an application of `numArgs` arguments with the calculated `ParamKind`s,
-returns `true` if we should wrap the applied function with `@` when we are in explicit mode.
--/
-def needsExplicit (f : Expr) (numArgs : Nat) (paramKinds : Array ParamKind) : Bool :=
-  if paramKinds.size == 0 && 0 < numArgs && f matches .const _ [] then
-    -- Error calculating ParamKinds,
-    -- but we presume that the universe list has been intentionally erased, for example by LCNF.
-    -- The arguments in this case are *only* the explicit arguments, so we don't want to prefix with `@`.
-    false
-  else
-    -- Error calculating ParamKinds, so return `true` to be safe
-    paramKinds.size < numArgs
-    -- One of the supplied parameters isn't explicit
-    || paramKinds[:numArgs].any (fun param => !param.bInfo.isExplicit)
-    -- The next parameter is implicit or inst implicit
-    || (numArgs < paramKinds.size && paramKinds[numArgs]!.bInfo matches .implicit | .instImplicit)
-    -- One of the parameters after the supplied parameters is explicit but not regular explicit.
-    || paramKinds[numArgs:].any (fun param => param.bInfo.isExplicit && !param.isRegularExplicit)
-
 /--
 Delaborates a function application in explicit mode, and ensures the resulting
-head syntax is wrapped with `@` if needed.
+head syntax is wrapped with `@`.
 -/
-def delabAppExplicitCore (numArgs : Nat) (delabHead : Delab) (paramKinds : Array ParamKind) : Delab := do
-  let (fnStx, _, argStxs) ← withBoundedAppFnArgs numArgs
+def delabAppExplicitCore (maxArgs : Nat) (delabHead : Delab) (paramKinds : Array ParamKind) (tagAppFn : Bool) : Delab := do
+  let (fnStx, _, argStxs) ← withBoundedAppFnArgs maxArgs
     (do
-      let stx ← delabHead
-      let insertExplicit := !stx.raw.isOfKind ``Lean.Parser.Term.explicit && needsExplicit (← getExpr) numArgs paramKinds
-      let stx ← if insertExplicit then `(@$stx) else pure stx
+      let stx ← withOptionAtCurrPos `pp.tagAppFns tagAppFn delabHead
+      let needsExplicit := stx.raw.getKind != ``Lean.Parser.Term.explicit
+      let stx ← if needsExplicit then `(@$stx) else pure stx
       pure (stx, paramKinds.toList, #[]))
     (fun ⟨fnStx, paramKinds, argStxs⟩ => do
-      let isInstImplicit := paramKinds.head? |>.map (·.bInfo == .instImplicit) |>.getD false
+      let isInstImplicit := match paramKinds with
+                            | [] => false
+                            | param :: _ => param.bInfo == BinderInfo.instImplicit
       let argStx ← if ← getPPOption getPPAnalysisHole then `(_)
                    else if isInstImplicit == true then
-                     withTypeAscription (cond := ← getPPOption getPPInstanceTypes) do
-                       if ← getPPOption getPPInstances then delab else `(_)
+                     let stx ← if ← getPPOption getPPInstances then delab else `(_)
+                     if ← getPPOption getPPInstanceTypes then
+                       let typeStx ← withType delab
+                       `(($stx : $typeStx))
+                     else pure stx
                    else delab
       pure (fnStx, paramKinds.tailD [], argStxs.push argStx))
   return Syntax.mkApp fnStx argStxs
 
 /--
 Delaborates a function application in the standard mode, where implicit arguments are generally not
-included, unless `pp.analysis.namedArg` is set at that argument.
-
-This delaborator is where `app_unexpander`s and the structure instance unexpander are applied.
-
-Assumes `numArgs ≤ paramKinds.size`.
+included.
 -/
-def delabAppImplicitCore (unexpand : Bool) (numArgs : Nat) (delabHead : Delab) (paramKinds : Array ParamKind) : Delab := do
-  let (shouldUnexpand, fnStx, _, _, argStxs, argData) ←
-    withBoundedAppFnArgs numArgs
-      (do
-        let head ← getExpr
-        let shouldUnexpand ← pure (unexpand && head.consumeMData.isConst)
-          <&&> not <$> withMDatasOptions (getPPOption getPPUniverses <||> getPPOption getPPAnalysisBlockImplicit)
-        return (shouldUnexpand, ← delabHead, numArgs, paramKinds.toList, Array.mkEmpty numArgs, (Array.mkEmpty numArgs).push (shouldUnexpand, 0)))
-      (fun (shouldUnexpand, fnStx, remainingArgs, paramKinds, argStxs, argData) => do
-        /-
-        - `argStxs` is the accumulated array of arguments that should be pretty printed
-        - `argData` is a list of `Bool × Nat` used to figure out:
-          1. whether an unexpander could be used for the prefix up to this argument and
-          2. how many arguments we need to include after this one when annotating the result of unexpansion.
-          Argument `argStxs[i]` corresponds to `argData[i+1]`, with `argData[0]` being for the head itself.
-        -/
-        let (argUnexpandable, stx?) ← mkArgStx (remainingArgs - 1) paramKinds
-        let shouldUnexpand := shouldUnexpand && argUnexpandable
-        let (argStxs, argData) :=
-          match stx?, argData.back with
-          -- By default, a pretty-printed argument accounts for just itself.
-          | some stx, _ => (argStxs.push stx, argData.push (shouldUnexpand, 1))
-          -- A non-pretty-printed argument is accounted for by the previous pretty printed one.
-          | none, (_, argCount) => (argStxs, argData.pop.push (shouldUnexpand, argCount + 1))
-        return (shouldUnexpand, fnStx, remainingArgs - 1, paramKinds.tailD [], argStxs, argData))
-  if ← pure (argData.any Prod.fst) <&&> getPPOption getPPNotation then
-    -- Try using an app unexpander for a prefix of the arguments.
-    if let some stx ← (some <$> tryAppUnexpanders fnStx argStxs argData) <|> pure none then
-      return stx
-  let stx := Syntax.mkApp fnStx argStxs
-  if ← pure shouldUnexpand <&&> getPPOption getPPStructureInstances then
-    -- Try using the structure instance unexpander.
-    -- It only makes sense applying this to the entire application, since structure instances cannot themselves be applied.
-    if let some stx ← (some <$> unexpandStructureInstance stx) <|> pure none then
-      return stx
-  return stx
-where
-  mkNamedArg (name : Name) (argStx : Syntax) : DelabM (Bool × Option Syntax) :=
-    return (false, ← `(Parser.Term.namedArgument| ($(mkIdent name) := $argStx)))
-  /--
-  If the argument should be pretty printed then it returns the syntax for that argument.
-  The boolean is `false` if an unexpander should not be used for the application due to this argument.
-  The argumnet `remainingArgs` is the number of arguments in the application after this one.
-  -/
-  mkArgStx (remainingArgs : Nat) (paramKinds : List ParamKind) : DelabM (Bool × Option Syntax) := do
-    if ← getPPOption getPPAnalysisSkip then return (true, none)
-    else if ← getPPOption getPPAnalysisHole then return (true, ← `(_))
-    else
+def delabAppImplicitCore (maxArgs : Nat) (delabHead : Delab) (paramKinds : Array ParamKind) (tagAppFn : Bool) : Delab := do
+  -- TODO: always call the unexpanders, make them guard on the right # args?
+  let (fnStx, _, argStxs) ← withBoundedAppFnArgs maxArgs
+    (do
+      let stx ← withOptionAtCurrPos `pp.tagAppFns tagAppFn delabHead
+      return (stx, paramKinds.toList, #[]))
+    (fun (fnStx, paramKinds, argStxs) => do
       let arg ← getExpr
-      let param :: _ := paramKinds | unreachable!
-      if ← getPPOption getPPAnalysisNamedArg then
-        mkNamedArg param.name (← delab)
-      else if param.defVal.isSome && remainingArgs == 0 && param.defVal.get! == arg then
-        -- Assumption: `useAppExplicit` has already detected whether it is ok to omit this argument
-        return (true, none)
-      else if param.bInfo.isExplicit then
-        return (true, ← delab)
-      else if ← pure (param.name == `motive) <&&> shouldShowMotive arg (← getOptions) then
-        mkNamedArg param.name (← delab)
-      else
-        return (true, none)
-  /--
-  Runs the given unexpanders, returning the resulting syntax if any are applicable, and otherwise fails.
-  -/
-  tryUnexpand (fs : List Unexpander) (stx : Syntax) : DelabM Syntax := do
-    let ref ← getRef
-    fs.firstM fun f =>
-      match f stx |>.run ref |>.run () with
-      | EStateM.Result.ok stx _ => return stx
-      | _ => failure
-  /--
-  If the expression is a candidate for app unexpanders,
-  try applying an app unexpander using some prefix of the arguments, longest prefix first.
-  This function makes sure that the unexpanded syntax is annotated and given TermInfo so that it is hoverable in the InfoView.
-  -/
-  tryAppUnexpanders (fnStx : Term) (argStxs : Array Syntax) (argData : Array (Bool × Nat)) : Delab := do
-    let .const c _ := (← getExpr).getAppFn.consumeMData | unreachable!
-    let fs := appUnexpanderAttribute.getValues (← getEnv) c
-    if fs.isEmpty then failure
-    let rec go (prefixArgs : Nat) : DelabM Term := do
-      let (unexpand, argCount) := argData[prefixArgs]!
-      match prefixArgs with
-      | 0 =>
-        guard unexpand
-        let stx ← tryUnexpand fs fnStx
-        return Syntax.mkApp (← annotateTermInfo stx) argStxs
-      | prefixArgs' + 1 =>
-        (do guard unexpand
-            let stx ← tryUnexpand fs <| Syntax.mkApp fnStx (argStxs.extract 0 prefixArgs)
-            return Syntax.mkApp (← annotateTermInfo stx) (argStxs.extract prefixArgs argStxs.size))
-        <|> withBoundedAppFn argCount (go prefixArgs')
-    go argStxs.size
+      let opts ← getOptions
+      let mkNamedArg (name : Name) (argStx : Syntax) : DelabM Syntax := do
+        `(Parser.Term.namedArgument| ($(mkIdent name) := $argStx))
+      let argStx? : Option Syntax ←
+        if ← getPPOption getPPAnalysisSkip then pure none
+        else if ← getPPOption getPPAnalysisHole then `(_)
+        else
+          match paramKinds with
+          | [] => delab
+          | param :: rest =>
+            if param.defVal.isSome && rest.isEmpty then
+              let v := param.defVal.get!
+              if !v.hasLooseBVars && v == arg then pure none else delab
+            else if !param.isRegularExplicit && param.defVal.isNone then
+              if ← getPPOption getPPAnalysisNamedArg <||> (pure (param.name == `motive) <&&> shouldShowMotive arg opts) then some <$> mkNamedArg param.name (← delab) else pure none
+            else delab
+      let argStxs := match argStx? with
+        | none => argStxs
+        | some stx => argStxs.push stx
+      pure (fnStx, paramKinds.tailD [], argStxs))
+  let stx := Syntax.mkApp fnStx argStxs
 
-/--
-Returns true if an application should use explicit mode when delaborating.
--/
-def useAppExplicit (numArgs : Nat) (paramKinds : Array ParamKind) : DelabM Bool := do
-  -- If `pp.explicit` is set, then use explicit mode.
-  -- (Note that explicit mode can decide to omit `@` if the application has no implicit arguments.)
-  if ← getPPOption getPPExplicit then return true
-
-  -- If there was an error collecting ParamKinds, fall back to explicit mode.
-  if paramKinds.size < numArgs then return true
-
-  if numArgs < paramKinds.size then
-    let nextParam := paramKinds[numArgs]!
-
-    -- If the next parameter is implicit or inst implicit, fall back to explicit mode.
-    -- This is necessary for `@Eq` for example.
-    if nextParam.bInfo matches .implicit | .instImplicit then return true
-
-  -- If any of the next parameters is explicit but has an optional value or is an autoparam, fall back to explicit mode.
-  -- This is necessary since these are eagerly processed when elaborating.
-  if paramKinds[numArgs:].any fun param => param.bInfo.isExplicit && !param.isRegularExplicit then return true
-
-  return false
+  if ← isRegularApp maxArgs then
+    (guard (← getPPOption getPPNotation) *> unexpandRegularApp stx)
+    <|> (guard (← getPPOption getPPStructureInstances) *> unexpandStructureInstance stx)
+    <|> pure stx
+  else pure stx
 
 /--
 Delaborates applications. Removes up to `maxArgs` arguments to form
 the "head" of the application and delaborates the head using `delabHead`.
-Then the application is then processed in explicit mode or implicit mode depending on which should be used.
+The remaining arguments are processed depending on whether heuristics indicate that the application
+should be delaborated using `@`.
 -/
-def delabAppCore (unexpand : Bool) (maxArgs : Nat) (delabHead : Delab) : Delab := do
+def delabAppCore (maxArgs : Nat) (delabHead : Delab) : Delab := do
+  let tagAppFn ← getPPOption getPPTagAppFns
   let e ← getExpr
-  let args := e.getBoundedAppArgs maxArgs
-  let paramKinds ← getParamKinds (e.getBoundedAppFn maxArgs) args
+  let paramKinds ← getParamKinds (e.getBoundedAppFn maxArgs) (e.getBoundedAppArgs maxArgs)
 
-  let useExplicit ← useAppExplicit args.size paramKinds
+  let useExplicit ← useAppExplicit paramKinds
 
   if useExplicit then
-    delabAppExplicitCore args.size delabHead paramKinds
+    delabAppExplicitCore maxArgs delabHead paramKinds tagAppFn
   else
-    delabAppImplicitCore unexpand args.size delabHead paramKinds
+    delabAppImplicitCore maxArgs delabHead paramKinds tagAppFn
 
 /--
 Default delaborator for applications.
 -/
 @[builtin_delab app]
 def delabApp : Delab := do
-  let tagAppFn ← getPPOption getPPTagAppFns
   let e ← getExpr
-  delabAppCore true e.getAppNumArgs (delabAppFn tagAppFn)
-where
-  delabAppFn (tagAppFn : Bool) : Delab :=
-    withOptionAtCurrPos `pp.tagAppFns tagAppFn do
-      if (← getExpr).consumeMData.isConst then
-        withMDatasOptions delabConst
-      else
-        delab
+  delabAppCore e.getAppNumArgs delabAppFn
 
 /--
 The `withOverApp` combinator allows delaborators to handle "over-application" by using the core
@@ -423,7 +344,7 @@ def withOverApp (arity : Nat) (x : Delab) : Delab := do
   if n == arity then
     x
   else
-    delabAppCore false (n - arity) (withAnnotateTermInfo x)
+    delabAppCore (n - arity) (withAnnotateTermInfo x)
 
 /-- State for `delabAppMatch` and helpers. -/
 structure AppMatchState where

src/Lean/PrettyPrinter/Delaborator/SubExpr.lean

@@ -65,16 +65,6 @@ def withBoundedAppFnArgs (maxArgs : Nat) (xf : m α) (xa : α → m α) : m α :
     withAppArg (xa acc)
   | _, _ => xf
 
-/--
-Runs `xf` in the context of `Lean.Expr.getBoundedAppFn maxArgs`.
-This is equivalent to `withBoundedAppFnArgs maxArgs xf pure`.
--/
-def withBoundedAppFn (maxArgs : Nat) (xf : m α) : m α := do
-  let e ← getExpr
-  let numArgs := min maxArgs e.getAppNumArgs
-  let newPos := (← getPos).pushNaryFn numArgs
-  withTheReader SubExpr (fun cfg => { cfg with expr := e.getBoundedAppFn numArgs, pos := newPos }) xf
-
 def withBindingDomain (x : m α) : m α := do descend (← getExpr).bindingDomain! 0 x
 
 def withBindingBody (n : Name) (x : m α) : m α := do