chore: update stage0

RELEASES.md

@@ -8,15 +8,9 @@ This file contains work-in-progress notes for the upcoming release, as well as p
 Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
 of each version.
 
-v4.7.0
+v4.7.0 (development in progress)
 ---------
 
-* `simp` and `rw` now use instance arguments found by unification,
-  rather than always resynthesizing. For backwards compatibility, the original behaviour is
-  available via `set_option tactic.skipAssignedInstances false`.
-  [#3507](https://github.com/leanprover/lean4/pull/3507) and
-  [#3509](https://github.com/leanprover/lean4/pull/3509).
-
 * When the `pp.proofs` is false, now omitted proofs use `⋯` rather than `_`,
   which gives a more helpful error message when copied from the Infoview.
   The `pp.proofs.threshold` option lets small proofs always be pretty printed.
@@ -100,48 +94,7 @@ v4.7.0
 * 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)
-
-* You can now write `termination_by?` after a declaration to see the automatically inferred
-  termination argument, and turn it into a `termination_by …` clause using the “Try this” widget or a code action. [#3514](https://github.com/leanprover/lean4/pull/3514)
-
-* A large fraction of `Std` has been moved into the Lean repository.
-  This was motivated by:
-  1. Making universally useful tactics such as `ext`, `by_cases`, `change at`,
-    `norm_cast`, `rcases`, `simpa`, `simp?`, `omega`, and `exact?`
-    available to all users of Lean, without imports.
-  2. Minimizing the syntactic changes between plain Lean and Lean with `import Std`.
-  3. Simplifying the development process for the basic data types
-     `Nat`, `Int`, `Fin` (and variants such as `UInt64`), `List`, `Array`,
-     and `BitVec` as we begin making the APIs and simp normal forms for these types
-     more complete and consistent.
-  4. Laying the groundwork for the Std roadmap, as a library focused on
-     essential datatypes not provided by the core langauge (e.g. `RBMap`)
-     and utilities such as basic IO.
-  While we have achieved most of our initial aims in `v4.7.0-rc1`,
-  some upstreaming will continue over the coming months.
-
-* The `/` and `%` notations in `Int` now use `Int.ediv` and `Int.emod`
-  (i.e. the rounding conventions have changed).
-  Previously `Std` overrode these notations, so this is no change for users of `Std`.
-  There is now kernel support for these functions.
-  [#3376](https://github.com/leanprover/lean4/pull/3376).
-
-* `omega`, our integer linear arithmetic tactic, is now available in the core langauge.
-  * It is supplemented by a preprocessing tactic `bv_omega` which can solve goals about `BitVec`
-    which naturally translate into linear arithmetic problems.
-    [#3435](https://github.com/leanprover/lean4/pull/3435).
-  * `omega` now has support for `Fin` [#3427](https://github.com/leanprover/lean4/pull/3427),
-    the `<<<` operator [#3433](https://github.com/leanprover/lean4/pull/3433).
-  * During the port `omega` was modified to no longer identify atoms up to definitional equality
-    (so in particular it can no longer prove `id x ≤ x`). [#3525](https://github.com/leanprover/lean4/pull/3525).
-    This may cause some regressions.
-    We plan to provide a general purpose preprocessing tactic later, or an `omega!` mode.
-  * `omega` is now invoked in Lean's automation for termination proofs
-    [#3503](https://github.com/leanprover/lean4/pull/3503) as well as in
-    array indexing proofs [#3515](https://github.com/leanprover/lean4/pull/3515).
-    This automation will be substantially revised in the medium term,
-    and while `omega` does help automate some proofs, we plan to make this much more robust.
-
+* 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
@@ -156,44 +109,10 @@ v4.7.0
   useful for checking tactics (particularly `simp`) behave as expected in test
   suites.
 
-* Previously, app unexpanders would only be applied to entire applications. However, some notations produce
-  functions, and these functions can be given additional arguments. The solution so far has been to write app unexpanders so that they can take an arbitrary number of additional arguments. However this leads to misleading hover information in the Infoview. For example, while `HAdd.hAdd f g 1` pretty prints as `(f + g) 1`, hovering over `f + g` shows `f`. There is no way to fix the situation from within an app unexpander; the expression position for `HAdd.hAdd f g` is absent, and app unexpanders cannot register TermInfo.
-
-  This commit changes the app delaborator to try running app unexpanders on every prefix of an application, from longest to shortest prefix. For efficiency, it is careful to only try this when app delaborators do in fact exist for the head constant, and it also ensures arguments are only delaborated once. Then, in `(f + g) 1`, the `f + g` gets TermInfo registered for that subexpression, making it properly hoverable.
-
-  [#3375](https://github.com/leanprover/lean4/pull/3375)
-
 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
   monads built on `EIO Exception` should be synthesized automatically.
-* The `match ... with.` and `fun.` notations previously in Std have been replaced by
-  `nomatch ...` and `nofun`. [#3279](https://github.com/leanprover/lean4/pull/3279) and [#3286](https://github.com/leanprover/lean4/pull/3286)
-
-
-Other improvements:
-* Several bug fixes for `simp`:
-  * we should not crash when `simp` loops [#3269](https://github.com/leanprover/lean4/pull/3269)
-  * `simp` gets stuck on `autoParam` [#3315](https://github.com/leanprover/lean4/pull/3315)
-  * `simp` fails when custom discharger makes no progress [#3317](https://github.com/leanprover/lean4/pull/3317)
-  * `simp` fails to discharge `autoParam` premises even when it can reduce them to `True` [#3314](https://github.com/leanprover/lean4/pull/3314)
-  * `simp?` suggests generated equations lemma names, fixes [#3547](https://github.com/leanprover/lean4/pull/3547) [#3573](https://github.com/leanprover/lean4/pull/3573)
-* Fixes for `match` expressions:
-  * fix regression with builtin literals [#3521](https://github.com/leanprover/lean4/pull/3521)
-  * accept `match` when patterns cover all cases of a `BitVec` finite type [#3538](https://github.com/leanprover/lean4/pull/3538)
-  * fix matching `Int` literals [#3504](https://github.com/leanprover/lean4/pull/3504)
-  * patterns containing int values and constructors [#3496](https://github.com/leanprover/lean4/pull/3496)
-* Improve `termination_by` error messages [#3255](https://github.com/leanprover/lean4/pull/3255)
-* Fix `rename_i` in macros, fixes [#3553](https://github.com/leanprover/lean4/pull/3553) [#3581](https://github.com/leanprover/lean4/pull/3581)
-* Fix excessive resource usage in `generalize`, fixes [#3524](https://github.com/leanprover/lean4/pull/3524) [#3575](https://github.com/leanprover/lean4/pull/3575)
-* An equation lemma with autoParam arguments fails to rewrite, fixing [#2243](https://github.com/leanprover/lean4/pull/2243) [#3316](https://github.com/leanprover/lean4/pull/3316)
-* `add_decl_doc` should check that declarations are local [#3311](https://github.com/leanprover/lean4/pull/3311)
-* Instantiate the types of inductives with the right parameters, closing [#3242](https://github.com/leanprover/lean4/pull/3242) [#3246](https://github.com/leanprover/lean4/pull/3246)
-* New simprocs for many basic types. [#3407](https://github.com/leanprover/lean4/pull/3407)
-
-Lake fixes:
-* Warn on fetch cloud release failure [#3401](https://github.com/leanprover/lean4/pull/3401)
-* Cloud release trace & `lake build :release` errors [#3248](https://github.com/leanprover/lean4/pull/3248)
 
 v4.6.0
 ---------

src/CMakeLists.txt

@@ -11,7 +11,7 @@ project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
 set(LEAN_VERSION_MINOR 7)
 set(LEAN_VERSION_PATCH 0)
-set(LEAN_VERSION_IS_RELEASE 1)  # This number is 1 in the release revision, and 0 otherwise.
+set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
 set(LEAN_VERSION_STRING "${LEAN_VERSION_MAJOR}.${LEAN_VERSION_MINOR}.${LEAN_VERSION_PATCH}")
 if (LEAN_SPECIAL_VERSION_DESC)

src/Init/Data/List/Basic.lean

@@ -727,9 +727,9 @@ inductive lt [LT α] : List α → List α → Prop where
 instance [LT α] : LT (List α) := ⟨List.lt⟩
 
 instance hasDecidableLt [LT α] [h : DecidableRel (α:=α) (·<·)] : (l₁ l₂ : List α) → Decidable (l₁ < l₂)
-  | [],    []    => isFalse nofun
+  | [],    []    => isFalse (fun h => nomatch h)
   | [],    _::_  => isTrue (List.lt.nil _ _)
-  | _::_, []     => isFalse nofun
+  | _::_, []     => isFalse (fun h => nomatch h)
   | a::as, b::bs =>
     match h a b with
     | isTrue h₁  => isTrue (List.lt.head _ _ h₁)

src/Init/Data/Nat.lean

@@ -16,4 +16,3 @@ import Init.Data.Nat.Power2
 import Init.Data.Nat.Linear
 import Init.Data.Nat.SOM
 import Init.Data.Nat.Lemmas
-import Init.Data.Nat.Mod

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

@@ -23,13 +23,26 @@ namespace Nat
 private theorem one_div_two : 1/2 = 0 := by trivial
 
 private theorem two_pow_succ_sub_succ_div_two : (2 ^ (n+1) - (x + 1)) / 2 = 2^n - (x/2 + 1) := by
-  omega
+  if h : x + 1 ≤ 2 ^ (n + 1) then
+    apply fun x => (Nat.sub_eq_of_eq_add x).symm
+    apply Eq.trans _
+    apply Nat.add_mul_div_left _ _ Nat.zero_lt_two
+    rw [← Nat.sub_add_comm h]
+    rw [Nat.add_sub_assoc (by omega)]
+    rw [Nat.pow_succ']
+    rw [Nat.mul_add_div Nat.zero_lt_two]
+    simp [show (2 * (x / 2 + 1) - (x + 1)) / 2 = 0 by omega]
+  else
+    rw [Nat.pow_succ'] at *
+    omega
 
 private theorem two_pow_succ_sub_one_div_two : (2 ^ (n+1) - 1) / 2 = 2^n - 1 :=
   two_pow_succ_sub_succ_div_two
 
 private theorem two_mul_sub_one {n : Nat} (n_pos : n > 0) : (2*n - 1) % 2 = 1 := by
-  omega
+  match n with
+  | 0 => contradiction
+  | n + 1 => simp [Nat.mul_succ, Nat.mul_add_mod, mod_eq_of_lt]
 
 /-! ### Preliminaries -/
 
@@ -267,7 +280,8 @@ theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
     | n+1 =>
       -- just logic + omega:
       simp only [zero_lt_succ, decide_True, Bool.true_and]
-      rw [← decide_not, decide_eq_decide]
+      rw [Nat.pow_succ', ← decide_not, decide_eq_decide]
+      rw [Nat.pow_succ'] at h₂
       omega
   | succ i ih =>
     simp only [testBit_succ]
@@ -278,7 +292,8 @@ theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
     | n+1 =>
       rw [Nat.two_pow_succ_sub_succ_div_two, ih]
       · simp [Nat.succ_lt_succ_iff]
-      · omega
+      · rw [Nat.pow_succ'] at h₂
+        omega
 
 @[simp] theorem testBit_two_pow_sub_one (n i : Nat) : testBit (2^n-1) i = decide (i < n) := by
   rw [testBit_two_pow_sub_succ]
@@ -432,8 +447,12 @@ theorem testBit_mul_pow_two_add (a : Nat) {b i : Nat} (b_lt : b < 2^i) (j : Nat)
   cases Nat.lt_or_ge j i with
   | inl j_lt =>
     simp only [j_lt]
-    have i_def : i = j + succ (pred (i-j)) := by
-      rw [succ_pred_eq_of_pos] <;> omega
+    have i_ge := Nat.le_of_lt j_lt
+    have i_sub_j_nez : i-j ≠ 0 := Nat.sub_ne_zero_of_lt j_lt
+    have i_def : i = j + succ (pred (i-j)) :=
+          calc i = j + (i-j) := (Nat.add_sub_cancel' i_ge).symm
+               _ = j + succ (pred (i-j)) := by
+                 rw [← congrArg (j+·) (Nat.succ_pred i_sub_j_nez)]
     rw [i_def]
     simp only [testBit_to_div_mod, Nat.pow_add, Nat.mul_assoc]
     simp only [Nat.mul_add_div (Nat.two_pow_pos _), Nat.mul_add_mod]

src/Init/Data/Nat/Mod.lean

@@ -1,76 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
--/
-prelude
-import Init.Omega
-
-/-!
-# Further results about `mod`.
-
-This file proves some results about `mod` that are useful for bitblasting,
-in particular
-`Nat.mod_mul : x % (a * b) = x % a + a * (x / a % b)`
-and its corollary
-`Nat.mod_pow_succ : x % b ^ (k + 1) = x % b ^ k + b ^ k * ((x / b ^ k) % b)`.
-
-It contains the necesssary preliminary results relating order and `*` and `/`,
-which should probably be moved to their own file.
--/
-
-namespace Nat
-
-@[simp] protected theorem mul_lt_mul_left (a0 : 0 < a) : a * b < a * c ↔ b < c := by
-  induction a with
-  | zero => simp_all
-  | succ a ih =>
-    cases a
-    · simp
-    · simp_all [succ_eq_add_one, Nat.right_distrib]
-      omega
-
-@[simp] protected theorem mul_lt_mul_right (a0 : 0 < a) : b * a < c * a ↔ b < c := by
-  rw [Nat.mul_comm b a, Nat.mul_comm c a, Nat.mul_lt_mul_left a0]
-
-protected theorem lt_of_mul_lt_mul_left {a b c : Nat} (h : a * b < a * c) : b < c := by
-  cases a <;> simp_all
-
-protected theorem lt_of_mul_lt_mul_right {a b c : Nat} (h : b * a < c * a) : b < c := by
-  rw [Nat.mul_comm b a, Nat.mul_comm c a] at h
-  exact Nat.lt_of_mul_lt_mul_left h
-
-protected theorem div_lt_of_lt_mul {m n k : Nat} (h : m < n * k) : m / n < k :=
-  Nat.lt_of_mul_lt_mul_left <|
-    calc
-      n * (m / n) ≤ m % n + n * (m / n) := Nat.le_add_left _ _
-      _ = m := mod_add_div _ _
-      _ < n * k := h
-
-theorem mod_mul_right_div_self (m n k : Nat) : m % (n * k) / n = m / n % k := by
-  rcases Nat.eq_zero_or_pos n with (rfl | hn); simp [mod_zero]
-  rcases Nat.eq_zero_or_pos k with (rfl | hk); simp [mod_zero]
-  conv => rhs; rw [← mod_add_div m (n * k)]
-  rw [Nat.mul_assoc, add_mul_div_left _ _ hn, add_mul_mod_self_left,
-    mod_eq_of_lt (Nat.div_lt_of_lt_mul (mod_lt _ (Nat.mul_pos hn hk)))]
-
-theorem mod_mul_left_div_self (m n k : Nat) : m % (k * n) / n = m / n % k := by
-  rw [Nat.mul_comm k n, mod_mul_right_div_self]
-
-@[simp 1100]
-theorem mod_mul_right_mod (a b c : Nat) : a % (b * c) % b = a % b :=
-  Nat.mod_mod_of_dvd a (Nat.dvd_mul_right b c)
-
-@[simp 1100]
-theorem mod_mul_left_mod (a b c : Nat) : a % (b * c) % c = a % c :=
-  Nat.mod_mod_of_dvd a (Nat.mul_comm _ _ ▸ Nat.dvd_mul_left c b)
-
-theorem mod_mul {a b x : Nat} : x % (a * b) = x % a + a * (x / a % b) := by
-  rw [Nat.add_comm, ← Nat.div_add_mod (x % (a*b)) a, Nat.mod_mul_right_mod,
-    Nat.mod_mul_right_div_self]
-
-theorem mod_pow_succ {x b k : Nat} :
-    x % b ^ (k + 1) = x % b ^ k + b ^ k * ((x / b ^ k) % b) := by
-  rw [Nat.pow_succ, Nat.mod_mul]
-
-end Nat

src/Init/Prelude.lean

@@ -1635,8 +1635,8 @@ instance : LT Nat where
   lt := Nat.lt
 
 theorem Nat.not_succ_le_zero : ∀ (n : Nat), LE.le (succ n) 0 → False
-  | 0      => nofun
-  | succ _ => nofun
+  | 0,      h => nomatch h
+  | succ _, h => nomatch h
 
 theorem Nat.not_lt_zero (n : Nat) : Not (LT.lt n 0) :=
   not_succ_le_zero n

src/Init/Tactics.lean

@@ -673,13 +673,12 @@ It makes sure the "continuation" `?_` is the main goal after refining.
 macro "refine_lift " e:term : tactic => `(tactic| focus (refine no_implicit_lambda% $e; rotate_right))
 
 /--
-The `have` tactic is for adding hypotheses to the local context of the main goal.
-* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
-* `have h := e` uses the type of `e` for `t`.
-* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
-* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
-  where `_` stands for the tactics that follow this one.
-  It is convenient for types that have only one applicable constructor.
+`have h : t := e` adds the hypothesis `h : t` to the current goal if `e` a term
+of type `t`.
+* If `t` is omitted, it will be inferred.
+* If `h` is omitted, the name `this` is used.
+* The variant `have pattern := e` is equivalent to `match e with | pattern => _`,
+  and it is convenient for types that have only one applicable constructor.
   For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
   hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
 -/
@@ -694,15 +693,12 @@ If `h :` is omitted, the name `this` is used.
  -/
 macro "suffices " d:sufficesDecl : tactic => `(tactic| refine_lift suffices $d; ?_)
 /--
-The `let` tactic is for adding definitions to the local context of the main goal.
-* `let x : t := e` adds the definition `x : t := e` if `e` is a term of type `t`.
-* `let x := e` uses the type of `e` for `t`.
-* `let : t := e` and `let := e` use `this` for the name of the hypothesis.
-* `let pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
-  where `_` stands for the tactics that follow this one.
-  It is convenient for types that let only one applicable constructor.
-  For example, given `p : α × β × γ`, `let ⟨x, y, z⟩ := p` produces the
-  local variables `x : α`, `y : β`, and `z : γ`.
+`let h : t := e` adds the hypothesis `h : t := e` to the current goal if `e` a term of type `t`.
+If `t` is omitted, it will be inferred.
+The variant `let pattern := e` is equivalent to `match e with | pattern => _`,
+and it is convenient for types that have only applicable constructor.
+Example: given `h : p ∧ q ∧ r`, `let ⟨h₁, h₂, h₃⟩ := h` produces the hypotheses
+`h₁ : p`, `h₂ : q`, and `h₃ : r`.
 -/
 macro "let " d:letDecl : tactic => `(tactic| refine_lift let $d:letDecl; ?_)
 /--

src/Lean/Data/PersistentHashMap.lean

@@ -84,14 +84,14 @@ partial def insertAtCollisionNodeAux [BEq α] : CollisionNode α β → Nat →
       else insertAtCollisionNodeAux n (i+1) k v
     else
       ⟨Node.collision (keys.push k) (vals.push v) (size_push heq k v), IsCollisionNode.mk _ _ _⟩
-  | ⟨Node.entries _, h⟩, _, _, _ => nomatch h
+  | ⟨Node.entries _, h⟩, _, _, _ => False.elim (nomatch h)
 
 def insertAtCollisionNode [BEq α] : CollisionNode α β → α → β → CollisionNode α β :=
   fun n k v => insertAtCollisionNodeAux n 0 k v
 
 def getCollisionNodeSize : CollisionNode α β → Nat
   | ⟨Node.collision keys _ _, _⟩ => keys.size
-  | ⟨Node.entries _, h⟩          => nomatch h
+  | ⟨Node.entries _, h⟩          => False.elim (nomatch h)
 
 def mkCollisionNode (k₁ : α) (v₁ : β) (k₂ : α) (v₂ : β) : Node α β :=
   let ks : Array α := Array.mkEmpty maxCollisions
@@ -105,7 +105,7 @@ partial def insertAux [BEq α] [Hashable α] : Node α β → USize → USize
     let newNode := insertAtCollisionNode ⟨Node.collision keys vals heq, IsCollisionNode.mk _ _ _⟩ k v
     if depth >= maxDepth || getCollisionNodeSize newNode < maxCollisions then newNode.val
     else match newNode with
-      | ⟨Node.entries _, h⟩ => nomatch h
+      | ⟨Node.entries _, h⟩ => False.elim (nomatch h)
       | ⟨Node.collision keys vals heq, _⟩ =>
         let rec traverse (i : Nat) (entries : Node α β) : Node α β :=
           if h : i < keys.size then

src/Lean/Elab/Do.lean

@@ -765,19 +765,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
@@ -1157,10 +1144,9 @@ where
       let d' ← `(discr)
       let mut termAlts := #[]
       for alt in alts do
-        let rhs ← `(($(← toTerm alt.rhs) : $((← read).m) _))
+        let rhs ← toTerm alt.rhs
         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]
+        let termAlt := mkNode ``Parser.Term.matchExprAlt #[mkAtomFrom alt.ref "|", optVar, alt.funName, mkNullNode alt.pvars, 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]
@@ -1628,11 +1614,10 @@ mutual
     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 var? := if alt[1].isNone then none else some alt[1][0]
+      let funName  := alt[2]
+      let pvars    := alt[3].getArgs
+      let rhs      := alt[5]
       let rhs ← doSeqToCode (getDoSeqElems rhs)
       pure { ref, var?, funName, pvars, rhs }
     let elseBranch ← doSeqToCode (getDoSeqElems doMatchExpr[4][1][3])
@@ -1708,9 +1693,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

src/Lean/Elab/Extra.lean

@@ -488,10 +488,8 @@ def elabBinRelCore (noProp : Bool) (stx : Syntax) (expectedType? : Option Expr)
     ```
     We can improve this failure in the future by applying default instances before reporting a type mismatch.
     -/
-    let lhsStx := stx[2]
-    let rhsStx := stx[3]
-    let lhs ← withRef lhsStx <| toTree lhsStx
-    let rhs ← withRef rhsStx <| toTree rhsStx
+    let lhs ← withRef stx[2] <| toTree stx[2]
+    let rhs ← withRef stx[3] <| toTree stx[3]
     let tree := .binop stx .regular f lhs rhs
     let r ← analyze tree none
     trace[Elab.binrel] "hasUncomparable: {r.hasUncomparable}, maxType: {r.max?}"
@@ -499,10 +497,10 @@ def elabBinRelCore (noProp : Bool) (stx : Syntax) (expectedType? : Option Expr)
       -- Use default elaboration strategy + `toBoolIfNecessary`
       let lhs ← toExprCore lhs
       let rhs ← toExprCore rhs
-      let lhs ← withRef lhsStx <| toBoolIfNecessary lhs
-      let rhs ← withRef rhsStx <| toBoolIfNecessary rhs
+      let lhs ← toBoolIfNecessary lhs
+      let rhs ← toBoolIfNecessary rhs
       let lhsType ← inferType lhs
-      let rhs ← withRef rhsStx <| ensureHasType lhsType rhs
+      let rhs ← ensureHasType lhsType rhs
       elabAppArgs f #[] #[Arg.expr lhs, Arg.expr rhs] expectedType? (explicit := false) (ellipsis := false) (resultIsOutParamSupport := false)
     else
       let mut maxType := r.max?.get!

src/Lean/Elab/MatchExpr.lean

@@ -52,22 +52,23 @@ 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] }
+  some { rhs := stx.getArg 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
+  let var? : Option Ident :=
+    let optVar := stx.getArg 1
+    if optVar.isNone then none else some ⟨optVar.getArg 0⟩
+  let funName := ⟨stx.getArg 2⟩
+  let pvars := stx.getArg 3 |>.getArgs.toList.reverse.map fun arg =>
+    match arg with
+    | `(_) => none
+    | _ => some ⟨arg⟩
+  let rhs := stx.getArg 5
+  some { var?, funName, pvars, rhs }
 
 /--
 Returns the function names of alternatives that do not have any pattern variable left.
@@ -112,25 +113,22 @@ 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)
+  let k : Ident ← `(k)
   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 (TSyntax ``bracketedBinder)) := do
+def getParams (alt : Alt) : MacroM (Array Term) := do
   let mut params := #[]
   if let some var := alt.var? then
-    params := params.push (← `(bracketedBinderF| ($var : Expr)))
+    params := params.push (← `(($var : Expr)))
   params := params ++ (← alt.pvars.toArray.reverse.filterMapM fun
     | none => return none
-    | some arg => return some (← `(bracketedBinderF| ($arg : Expr))))
+    | some arg => return some (← `(($arg : Expr))))
   if params.isEmpty then
-    return #[(← `(bracketedBinderF| (_ : Unit)))]
+    return #[(← `(_))]
   return params
 
 /--
@@ -156,11 +154,8 @@ 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 discr' ← `(discr)
+  let kElse ← `(ke)
   let rec loop (discr : Term) (alts : List Alt) : MacroM Term := withFreshMacroScope do
     let funNamesToMatch := getFunNamesToMatch alts
     let saveActual := shouldSaveActual alts
@@ -169,12 +164,12 @@ partial def generate (discr : Term) (alts : List Alt) (elseAlt : ElseAlt) : Macr
     let body ← if altsNext.isEmpty then
       `($kElse ())
     else
-      let discr' ← `(__discr)
+      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 ())
+        `(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 ())
+        `(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
@@ -182,10 +177,10 @@ partial def generate (discr : Term) (alts : List Alt) (elseAlt : ElseAlt) : Macr
         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 (_ : Unit) := $(⟨elseAlt.rhs⟩):term; let __discr := Expr.cleanupAnnotations $discr:term; $body:term)
+  let mut result ← `(let_delayed ke := 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 $params:bracketedBinder* := $(⟨alt.rhs⟩):term; $result:term)
+    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
@@ -203,15 +198,7 @@ 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)
+    MatchExpr.main discr (alts.raw.getArg 0).getArgs (alts.raw.getArg 1)
   | _ => Macro.throwUnsupported
 
 end Lean.Elab.Term

src/Lean/Elab/Print.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Util.FoldConsts
-import Lean.Meta.Eqns
 import Lean.Elab.Command
 
 namespace Lean.Elab.Command
@@ -129,18 +128,4 @@ private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
     cs.forM printAxiomsOf
   | _ => throwUnsupportedSyntax
 
-private def printEqnsOf (constName : Name) : CommandElabM Unit := do
-  let some eqns ← liftTermElabM <| Meta.getEqnsFor? constName (nonRec := true) |
-    logInfo m!"'{constName}' does not have equations"
-  let mut m := m!"equations:"
-  for eq in eqns do
-    let cinfo ← getConstInfo eq
-    m := m ++ Format.line ++ (← mkHeader "theorem" eq cinfo.levelParams cinfo.type .safe)
-  logInfo m
-
-@[builtin_command_elab «printEqns»] def elabPrintEqns : CommandElab := fun stx => do
-  let id := stx[2]
-  let cs ← resolveGlobalConstWithInfos id
-  cs.forM printEqnsOf
-
 end Lean.Elab.Command

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/BuiltinTactic.lean

@@ -352,21 +352,12 @@ def renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray ``binderIdent) : Ta
     let mut info  := #[]
     let mut found : NameSet := {}
     let n := lctx.numIndices
-    -- hypotheses are inaccessible if their scopes are different from the caller's (we assume that
-    -- the scopes are the same for all the hypotheses in `hs`, which is reasonable to expect in
-    -- practice and otherwise the expected semantics of `rename_i` really are not clear)
-    let some callerScopes := hs.findSome? (fun
-        | `(binderIdent| $h:ident) => some <| extractMacroScopes h.getId
-        | _ => none)
-      | return mvarId
     for i in [:n] do
       let j := n - i - 1
       match lctx.getAt? j with
       | none => pure ()
       | some localDecl =>
-        let inaccessible := !(extractMacroScopes localDecl.userName |>.equalScope callerScopes)
-        let shadowed := found.contains localDecl.userName
-        if inaccessible || shadowed then
+        if localDecl.userName.hasMacroScopes || found.contains localDecl.userName then
           if let `(binderIdent| $h:ident) := hs.back then
             let newName := h.getId
             lctx := lctx.setUserName localDecl.fvarId newName

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

@@ -358,7 +358,6 @@ def addIntInequality (p : MetaProblem) (h y : Expr) : OmegaM MetaProblem := do
 /-- Given a fact `h` with type `¬ P`, return a more useful fact obtained by pushing the negation. -/
 def pushNot (h P : Expr) : MetaM (Option Expr) := do
   let P ← whnfR P
-  trace[omega] "pushing negation: {P}"
   match P with
   | .forallE _ t b _ =>
     if (← isProp t) && (← isProp b) then
@@ -367,42 +366,43 @@ def pushNot (h P : Expr) : MetaM (Option Expr) := do
     else
       return none
   | .app _ _ =>
-    match_expr P with
-    | LT.lt α _ x y => match_expr α with
-      | Nat => return some (mkApp3 (.const ``Nat.le_of_not_lt []) x y h)
-      | Int => return some (mkApp3 (.const ``Int.le_of_not_lt []) x y h)
-      | Fin n => return some (mkApp4 (.const ``Fin.le_of_not_lt []) n x y h)
-      | _ => return none
-    | LE.le α _ x y => match_expr α with
-      | Nat => return some (mkApp3 (.const ``Nat.lt_of_not_le []) x y h)
-      | Int => return some (mkApp3 (.const ``Int.lt_of_not_le []) x y h)
-      | Fin n => return some (mkApp4 (.const ``Fin.lt_of_not_le []) n x y h)
-      | _ => return none
-    | Eq α x y => match_expr α with
-      | Nat => return some (mkApp3 (.const ``Nat.lt_or_gt_of_ne []) x y h)
-      | Int => return some (mkApp3 (.const ``Int.lt_or_gt_of_ne []) x y h)
-      | Fin n => return some (mkApp4 (.const ``Fin.lt_or_gt_of_ne []) n x y h)
-      | _ => return none
-    | Dvd.dvd α _ k x => match_expr α with
-      | Nat => return some (mkApp3 (.const ``Nat.emod_pos_of_not_dvd []) k x h)
-      | Int =>
-        -- This introduces a disjunction that could be avoided by checking `k ≠ 0`.
-        return some (mkApp3 (.const ``Int.emod_pos_of_not_dvd []) k x h)
-      | _ => return none
-    | Prod.Lex _ _ _ _ _ _ => return some (← mkAppM ``Prod.of_not_lex #[h])
-    | Not P =>
-      return some (mkApp3 (.const ``Decidable.of_not_not []) P
-        (.app (.const ``Classical.propDecidable []) P) h)
-    | And P Q =>
-      return some (mkApp5 (.const ``Decidable.or_not_not_of_not_and []) P Q
-        (.app (.const ``Classical.propDecidable []) P)
-        (.app (.const ``Classical.propDecidable []) Q) h)
-    | Or P Q =>
-      return some (mkApp3 (.const ``and_not_not_of_not_or []) P Q h)
-    | Iff P Q =>
-      return some (mkApp5 (.const ``Decidable.and_not_or_not_and_of_not_iff []) P Q
-        (.app (.const ``Classical.propDecidable []) P)
-        (.app (.const ``Classical.propDecidable []) Q) h)
+    match P.getAppFnArgs with
+    | (``LT.lt, #[.const ``Int [], _, x, y]) =>
+      return some (mkApp3 (.const ``Int.le_of_not_lt []) x y h)
+    | (``LE.le, #[.const ``Int [], _, x, y]) =>
+      return some (mkApp3 (.const ``Int.lt_of_not_le []) x y h)
+    | (``LT.lt, #[.const ``Nat [], _, x, y]) =>
+      return some (mkApp3 (.const ``Nat.le_of_not_lt []) x y h)
+    | (``LE.le, #[.const ``Nat [], _, x, y]) =>
+      return some (mkApp3 (.const ``Nat.lt_of_not_le []) x y h)
+    | (``LT.lt, #[.app (.const ``Fin []) n, _, x, y]) =>
+      return some (mkApp4 (.const ``Fin.le_of_not_lt []) n x y h)
+    | (``LE.le, #[.app (.const ``Fin []) n, _, x, y]) =>
+      return some (mkApp4 (.const ``Fin.lt_of_not_le []) n x y h)
+    | (``Eq, #[.const ``Nat [], x, y]) =>
+      return some (mkApp3 (.const ``Nat.lt_or_gt_of_ne []) x y h)
+    | (``Eq, #[.const ``Int [], x, y]) =>
+      return some (mkApp3 (.const ``Int.lt_or_gt_of_ne []) x y h)
+    | (``Prod.Lex, _) => return some (← mkAppM ``Prod.of_not_lex #[h])
+    | (``Eq, #[.app (.const ``Fin []) n, x, y]) =>
+      return some (mkApp4 (.const ``Fin.lt_or_gt_of_ne []) n x y h)
+    | (``Dvd.dvd, #[.const ``Nat [], _, k, x]) =>
+      return some (mkApp3 (.const ``Nat.emod_pos_of_not_dvd []) k x h)
+    | (``Dvd.dvd, #[.const ``Int [], _, k, x]) =>
+      -- This introduces a disjunction that could be avoided by checking `k ≠ 0`.
+      return some (mkApp3 (.const ``Int.emod_pos_of_not_dvd []) k x h)
+    | (``Or, #[P₁, P₂]) => return some (mkApp3 (.const ``and_not_not_of_not_or []) P₁ P₂ h)
+    | (``And, #[P₁, P₂]) =>
+      return some (mkApp5 (.const ``Decidable.or_not_not_of_not_and []) P₁ P₂
+        (.app (.const ``Classical.propDecidable []) P₁)
+        (.app (.const ``Classical.propDecidable []) P₂) h)
+    | (``Not, #[P']) =>
+      return some (mkApp3 (.const ``Decidable.of_not_not []) P'
+        (.app (.const ``Classical.propDecidable []) P') h)
+    | (``Iff, #[P₁, P₂]) =>
+      return some (mkApp5 (.const ``Decidable.and_not_or_not_and_of_not_iff []) P₁ P₂
+        (.app (.const ``Classical.propDecidable []) P₁)
+        (.app (.const ``Classical.propDecidable []) P₂) h)
     | _ => return none
   | _ => return none
 

src/Lean/Elab/Util.lean

@@ -24,13 +24,6 @@ def MacroScopesView.format (view : MacroScopesView) (mainModule : Name) : Format
     else
       view.scopes.foldl Name.mkNum (view.name ++ view.imported ++ view.mainModule)
 
-/--
-Two names are from the same lexical scope if their scoping information modulo `MacroScopesView.name`
-is equal.
--/
-def MacroScopesView.equalScope (a b : MacroScopesView) : Bool :=
-  a.scopes == b.scopes && a.mainModule == b.mainModule && a.imported == b.imported
-
 namespace Elab
 
 def expandOptNamedPrio (stx : Syntax) : MacroM Nat :=

src/Lean/Expr.lean

@@ -1075,6 +1075,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
@@ -1611,31 +1638,6 @@ def isFalse (e : Expr) : Bool :=
 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/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
 

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/LazyDiscrTree.lean

@@ -698,14 +698,15 @@ private structure ImportFailure where
   /-- Exception that triggers error. -/
   exception : Exception
 
-#print Lean.Meta.Cache
 /-- Information generation from imported modules. -/
 private structure ImportData where
+  cache : IO.Ref (Lean.Meta.Cache)
   errors : IO.Ref (Array ImportFailure)
 
 private def ImportData.new : BaseIO ImportData := do
+  let cache ← IO.mkRef {}
   let errors ← IO.mkRef #[]
-  pure { errors }
+  pure { cache, errors }
 
 private def addConstImportData
     (env : Environment)
@@ -716,7 +717,8 @@ private def addConstImportData
     (name : Name) (constInfo : ConstantInfo) : BaseIO (PreDiscrTree α) := do
   if constInfo.isUnsafe then return tree
   if !allowCompletion env name then return tree
-  let mstate : Meta.State := { cache := {} }
+  let mstate : Meta.State := { cache := ←d.cache.get }
+  d.cache.set {}
   let ctx : Meta.Context := { config := { transparency := .reducible } }
   let cm := (act name constInfo).run ctx mstate
   let cctx : Core.Context := {
@@ -725,7 +727,8 @@ private def addConstImportData
   }
   let cstate : Core.State := {env}
   match ←(cm.run cctx cstate).toBaseIO with
-  | .ok ((a, _), _) =>
+  | .ok ((a, ms), _) =>
+    d.cache.set ms.cache
     pure <| a.foldl (fun t e => t.push e.key e.entry) tree
   | .error e =>
     let i : ImportFailure := {

src/Lean/Meta/LitValues.lean

@@ -27,10 +27,11 @@ def getRawNatValue? (e : Expr) : Option Nat :=
 
 /-- 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
+  let e := e.consumeMData
+  guard <| e.isAppOfArity' ``OfNat.ofNat 3
+  let type ← whnfD (e.getArg!' 0)
   guard <| type.getAppFn.isConstOf typeDeclName
-  let .lit (.natVal n) := n.consumeMData | failure
+  let .lit (.natVal n) := (e.getArg!' 1).consumeMData | failure
   return (n, type)
 
 /-- Return `some n` if `e` is a raw natural number or an `OfNat.ofNat`-application encoding `n`. -/
@@ -45,15 +46,16 @@ def getNatValue? (e : Expr) : MetaM (Option Nat) := do
 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)
+  if e.isAppOfArity' ``Neg.neg 3 then
+    let some (n, _) ← getOfNatValue? (e.getArg!' 2) ``Int | return none
+    return some (-n)
+  return none
 
 /-- 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)
+def getCharValue? (e : Expr) : MetaM (Option Char) := OptionT.run do
+  guard <| e.isAppOfArity' ``Char.ofNat 1
+  let n ← getNatValue? (e.getArg!' 0)
+  return Char.ofNat n
 
 /-- Return `some s` if `e` is of the form `.lit (.strVal s)`. -/
 def getStringValue? (e : Expr) : (Option String) :=

src/Lean/Meta/Match/CaseArraySizes.lean

@@ -19,7 +19,7 @@ structure CaseArraySizesSubgoal where
 def getArrayArgType (a : Expr) : MetaM Expr := do
   let aType ← inferType a
   let aType ← whnfD aType
-  unless aType.isAppOfArity ``Array 1 do
+  unless aType.isAppOfArity `Array 1 do
     throwError "array expected{indentExpr a}"
   pure aType.appArg!
 

src/Lean/Meta/Offset.lean

@@ -18,10 +18,9 @@ private abbrev withInstantiatedMVars (e : Expr) (k : Expr → OptionT MetaM α)
     k eNew
 
 def isNatProjInst (declName : Name) (numArgs : Nat) : Bool :=
-    (numArgs == 4 && (declName == ``Add.add || declName == ``Sub.sub || declName == ``Mul.mul || declName == ``Div.div || declName == ``Mod.mod || declName == ``NatPow.pow))
- || (numArgs == 5 && (declName == ``Pow.pow))
- || (numArgs == 6 && (declName == ``HAdd.hAdd || declName == ``HSub.hSub || declName == ``HMul.hMul || declName == ``HDiv.hDiv || declName == ``HMod.hMod || declName == ``HPow.hPow))
- || (numArgs == 3 && declName == ``OfNat.ofNat)
+      (numArgs == 4 && (declName == ``Add.add || declName == ``Sub.sub || declName == ``Mul.mul))
+   || (numArgs == 6 && (declName == ``HAdd.hAdd || declName == ``HSub.hSub || declName == ``HMul.hMul))
+   || (numArgs == 3 && declName == ``OfNat.ofNat)
 
 /--
   Evaluate simple `Nat` expressions.
@@ -36,21 +35,31 @@ partial def evalNat (e : Expr) : OptionT MetaM Nat := do
   | _                    => failure
 where
   visit e := do
-    match_expr e with
-    | Nat.succ a => return (← evalNat a) + 1
-    | Nat.add a b => return (← evalNat a) + (← evalNat b)
-    | Nat.sub a b => return (← evalNat a) - (← evalNat b)
-    | Nat.mul a b => return (← evalNat a) * (← evalNat b)
-    | Nat.div a b => return (← evalNat a) / (← evalNat b)
-    | Nat.mod a b => return (← evalNat a) % (← evalNat b)
-    | Nat.pow a b => return (← evalNat a) ^ (← evalNat b)
-    | _ =>
-      let e ← instantiateMVarsIfMVarApp e
-      let f := e.getAppFn
-      if f.isConst && isNatProjInst f.constName! e.getAppNumArgs then
+    let f := e.getAppFn
+    match f with
+    | .mvar .. => withInstantiatedMVars e evalNat
+    | .const c _ =>
+      let nargs := e.getAppNumArgs
+      if c == ``Nat.succ && nargs == 1 then
+        let v ← evalNat (e.getArg! 0)
+        return v+1
+      else if c == ``Nat.add && nargs == 2 then
+        let v₁ ← evalNat (e.getArg! 0)
+        let v₂ ← evalNat (e.getArg! 1)
+        return v₁ + v₂
+      else if c == ``Nat.sub && nargs == 2 then
+        let v₁ ← evalNat (e.getArg! 0)
+        let v₂ ← evalNat (e.getArg! 1)
+        return v₁ - v₂
+      else if c == ``Nat.mul && nargs == 2 then
+        let v₁ ← evalNat (e.getArg! 0)
+        let v₂ ← evalNat (e.getArg! 1)
+        return v₁ * v₂
+      else if isNatProjInst c nargs then
         evalNat (← unfoldProjInst? e)
       else
         failure
+    | _ => failure
 
 mutual
 

src/Lean/Meta/Tactic/Generalize.lean

@@ -23,8 +23,7 @@ structure GeneralizeArg where
 Telescopic `generalize` tactic. It can simultaneously generalize many terms.
 It uses `kabstract` to occurrences of the terms that need to be generalized.
 -/
-private partial def generalizeCore (mvarId : MVarId) (args : Array GeneralizeArg)
-    (transparency : TransparencyMode) : MetaM (Array FVarId × MVarId) :=
+private partial def generalizeCore (mvarId : MVarId) (args : Array GeneralizeArg) : MetaM (Array FVarId × MVarId) :=
   mvarId.withContext do
     mvarId.checkNotAssigned `generalize
     let tag ← mvarId.getTag
@@ -36,8 +35,7 @@ private partial def generalizeCore (mvarId : MVarId) (args : Array GeneralizeArg
         let eType ← instantiateMVars (← inferType e)
         let type ← go (i+1)
         let xName ← if let some xName := arg.xName? then pure xName else mkFreshUserName `x
-        return Lean.mkForall xName BinderInfo.default eType
-          (← withTransparency transparency <| kabstract type e)
+        return Lean.mkForall xName BinderInfo.default eType (← kabstract type e)
       else
         return target
     let targetNew ← go 0
@@ -73,62 +71,13 @@ private partial def generalizeCore (mvarId : MVarId) (args : Array GeneralizeArg
       mvarId.assign (mkAppN (mkAppN mvarNew es) rfls.toArray)
       mvarNew.mvarId!.introNP (args.size + rfls.length)
 
-/-
-Remark: we use `TransparencyMode.instances` as the default setting at `generalize`
-and `generalizeHyp` to avoid excessive resource usage.
-
-**Motivation:**
-The `kabstract e p` operation is widely used, for instance, in the `generalize` tactic.
-It operates by taking an expression `e` and a pattern (i.e., an expression containing metavariables)
-and employs keyed-matching to identify and abstract instances of `p` within `e`.
-For example, if `e` is `a + (2 * (b + c))` and `p` is `2 * ?m`, the resultant expression
-would be `a + #0`, where `#0` represents a loose bound variable.
-
-This matching process is not merely syntactic; it also considers reduction. It's impractical
-to attempt matching each sub-term with `p`; therefore, only sub-terms sharing the same "root"
-symbol are evaluated. For instance, with the pattern `2 * ?m`, only sub-terms with the
-root `*` are considered. Matching is executed using the definitionally equality test
-(i.e., `isDefEq`).
-
-The `generalize` tactic employs `kabstract` and defaults to standard reducibility.
-Hence, the `isDefEq` operations invoked by `kabstract` can become highly resource-intensive
-and potentially trigger "max recursion depth reached" errors, as observed in issue #3524.
-This issue was isolated by @**Scott Morrison** with the following example:
-```
-example (a : Nat) : ((2 ^ 7) + a) - 2 ^ 7 = 0 := by
-  generalize 0 - 0 = x
-```
-In this scenario, `kabstract` triggers a "max recursion depth reached" error while
-testing whether `((2 ^ 7) + a) - 2 ^ 7` is definitionally equal to `0 - 0`.
-Note that the term `((2 ^ 7) + a) - 2 ^ 7` is not ground.
-We believe most users find the error message to be uninformative and unexpected.
-To fix this issue, we decided to use `TransparencyMode.instances` as the default setting.
-
-Kyle Miller has performed the following analysis on the potential impact of the
-changes on Mathlib (2024-03-02).
-
-There seem to be just 130 cases of generalize in Mathlib, and after looking through a
-good number of them, they seem to come in just two types:
-
-- Ones where it looks like reducible+instance transparency should work, where in
-  particular there is nothing obvious being reduced, and
-- Ones that don't make use of the `kabstract` feature at all (it's being used like a
-  `have` that introduces an equality for rewriting).
-
-That wasn't a systematic review of generalize though. It's possible changing the
-transparency settings would break things, but in my opinion it would be better
-if generalize weren't used for unfolding things.
--/
-
 @[inherit_doc generalizeCore]
-def _root_.Lean.MVarId.generalize (mvarId : MVarId) (args : Array GeneralizeArg)
-    (transparency := TransparencyMode.instances) : MetaM (Array FVarId × MVarId) :=
-  generalizeCore mvarId args transparency
+def _root_.Lean.MVarId.generalize (mvarId : MVarId) (args : Array GeneralizeArg) : MetaM (Array FVarId × MVarId) :=
+  generalizeCore mvarId args
 
 @[inherit_doc generalizeCore, deprecated MVarId.generalize]
-def generalize (mvarId : MVarId) (args : Array GeneralizeArg)
-    (transparency := TransparencyMode.instances) : MetaM (Array FVarId × MVarId) :=
-  generalizeCore mvarId args transparency
+def generalize (mvarId : MVarId) (args : Array GeneralizeArg) : MetaM (Array FVarId × MVarId) :=
+  generalizeCore mvarId args
 
 /--
 Extension of `generalize` to support generalizing within specified hypotheses.
@@ -136,16 +85,16 @@ The `hyps` array contains the list of hypotheses within which to look for occurr
 of the generalizing expressions.
 -/
 def _root_.Lean.MVarId.generalizeHyp (mvarId : MVarId) (args : Array GeneralizeArg) (hyps : Array FVarId := #[])
-    (fvarSubst : FVarSubst := {}) (transparency := TransparencyMode.instances) : MetaM (FVarSubst × Array FVarId × MVarId) := do
+    (fvarSubst : FVarSubst := {}) : MetaM (FVarSubst × Array FVarId × MVarId) := do
   if hyps.isEmpty then
     -- trivial case
-    return (fvarSubst, ← mvarId.generalize args transparency)
+    return (fvarSubst, ← mvarId.generalize args)
   let args ← args.mapM fun arg => return { arg with expr := ← instantiateMVars arg.expr }
   let hyps ← hyps.filterM fun h => do
     let type ← instantiateMVars (← h.getType)
-    args.anyM fun arg => return (← withTransparency transparency <| kabstract type arg.expr).hasLooseBVars
+    args.anyM fun arg => return (← kabstract type arg.expr).hasLooseBVars
   let (reverted, mvarId) ← mvarId.revert hyps true
-  let (newVars, mvarId) ← mvarId.generalize args transparency
+  let (newVars, mvarId) ← mvarId.generalize args
   let (reintros, mvarId) ← mvarId.introNP reverted.size
   let fvarSubst := Id.run do
     let mut subst : FVarSubst := fvarSubst

src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean

@@ -74,31 +74,42 @@ def addAsVar (e : Expr) : M LinearExpr := do
 
 partial def toLinearExpr (e : Expr) : M LinearExpr := do
   match e with
-  | .lit (.natVal n)      => return num n
-  | .mdata _ e            => toLinearExpr e
-  | .const ``Nat.zero ..  => return num 0
-  | .app ..               => visit e
-  | .mvar ..              => visit e
-  | _                     => addAsVar e
+  | Expr.lit (Literal.natVal n) => return num n
+  | Expr.mdata _ e              => toLinearExpr e
+  | Expr.const ``Nat.zero ..    => return num 0
+  | Expr.app ..                 => visit e
+  | Expr.mvar ..                => visit e
+  | _                           => addAsVar e
 where
   visit (e : Expr) : M LinearExpr := do
-    match_expr e with
-    | Nat.succ a => return inc (← toLinearExpr a)
-    | Nat.add a b => return add (← toLinearExpr a) (← toLinearExpr b)
-    | Nat.mul a b =>
-      match (← evalNat a |>.run) with
-      | some k => return mulL k (← toLinearExpr b)
-      | none => match (← evalNat b |>.run) with
-        | some k => return mulR (← toLinearExpr a) k
-        | none => addAsVar e
-    | _ =>
-      let e ← instantiateMVarsIfMVarApp e
-      let f := e.getAppFn
-      if f.isConst && isNatProjInst f.constName! e.getAppNumArgs then
-        let some e ← unfoldProjInst? e | addAsVar e
-        toLinearExpr e
+    let f := e.getAppFn
+    match f with
+    | Expr.mvar .. =>
+      let eNew ← instantiateMVars e
+      if eNew != e then
+        toLinearExpr eNew
       else
         addAsVar e
+    | Expr.const declName .. =>
+      let numArgs := e.getAppNumArgs
+      if declName == ``Nat.succ && numArgs == 1 then
+        return inc (← toLinearExpr e.appArg!)
+      else if declName == ``Nat.add && numArgs == 2 then
+        return add (← toLinearExpr (e.getArg! 0)) (← toLinearExpr (e.getArg! 1))
+      else if declName == ``Nat.mul && numArgs == 2 then
+        match (← evalNat (e.getArg! 0) |>.run) with
+        | some k => return mulL k (← toLinearExpr (e.getArg! 1))
+        | none => match (← evalNat (e.getArg! 1) |>.run) with
+          | some k => return mulR (← toLinearExpr (e.getArg! 0)) k
+          | none => addAsVar e
+      else if isNatProjInst declName numArgs then
+        if let some e ← unfoldProjInst? e then
+          toLinearExpr e
+        else
+          addAsVar e
+      else
+        addAsVar e
+    | _ => addAsVar e
 
 partial def toLinearCnstr? (e : Expr) : M (Option LinearCnstr) := do
   let f := e.getAppFn

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

@@ -162,42 +162,42 @@ 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
+  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
   return .done { expr := toExpr (v₁.value ++ v₂.value) }
 
 /-- 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
+  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
   return .done { expr := toExpr (BitVec.ofNat m v.value.toNat) }
 
 /-- 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
+  unless e.isAppOfArity ``BitVec.toInt 2 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
   return .done { expr := 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
+  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
   return .done { expr := toExpr (BitVec.ofInt n i) }
 
 /-- 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) }
@@ -226,9 +226,9 @@ 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) }
   else
@@ -236,25 +236,25 @@ builtin_simproc [simp, seval] reduceZeroExtend' (zeroExtend' _ _) := fun e => do
 
 /-- 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
+  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
   return .done { expr := toExpr (v.value.shiftLeftZeroExtend m) }
 
 /-- 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
+  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
   return .done { expr := toExpr (v.value.extractLsb' start len) }
 
 /-- 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
+  return .done { expr := toExpr (v.value.replicate w) }
 
 /-- Simplification procedure for `zeroExtend` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceZeroExtend (zeroExtend _ _) := reduceExtend ``zeroExtend zeroExtend
@@ -264,19 +264,8 @@ 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
+  unless e.isAppOfArity ``allOnes 1 do return .continue
+  let some n ← Nat.fromExpr? e.appArg! | return .continue
   return .done { expr := toExpr (allOnes n) }
 
-builtin_simproc [simp, seval] reduceBitVecOfFin (BitVec.ofFin _)  := fun e => do
-  let_expr BitVec.ofFin w v ← e | return .continue
-  let some w ← evalNat w |>.run | return .continue
-  let some ⟨_, v⟩ ← getFinValue? v | return .continue
-  return .done { expr := toExpr (BitVec.ofNat w v.val) }
-
-builtin_simproc [simp, seval] reduceBitVecToFin (BitVec.toFin _)  := fun e => do
-  let_expr BitVec.toFin _ v ← e | return .continue
-  let some ⟨_, v⟩ ← getBitVecValue? v | return .continue
-  return .done { expr := toExpr v.toFin }
-
 end BitVec

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

@@ -42,8 +42,8 @@ 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
+  unless e.isAppOfArity ``Char.val 1 do return .continue
+  let some c ← fromExpr? e.appArg! | return .continue
   return .done { expr := toExpr c.val }
 builtin_simproc [simp, seval] reduceEq  (( _ : Char) = _)  := reduceBinPred ``Eq 3 (. = .)
 builtin_simproc [simp, seval] reduceNe  (( _ : Char) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
@@ -60,12 +60,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

@@ -71,13 +71,4 @@ builtin_simproc [simp, seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do
     return .done { expr := e }
   return .done { expr := toExpr v }
 
-builtin_simproc [simp, seval] reduceFinMk (Fin.mk _ _)  := fun e => do
-  let_expr Fin.mk n v _ ← e | return .continue
-  let some n ← evalNat n |>.run | return .continue
-  let some v ← getNatValue? v | return .continue
-  if h : n > 0 then
-    return .done { expr := toExpr (Fin.ofNat' v h) }
-  else
-    return .continue
-
 end Fin

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

@@ -57,7 +57,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 +67,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 (. < .)
@@ -89,14 +89,4 @@ builtin_simproc [simp, seval] reduceBNe  (( _ : Int) != _)  := reduceBoolPred ``
 builtin_simproc [simp, seval] reduceAbs (natAbs _) := reduceNatCore ``natAbs natAbs
 builtin_simproc [simp, seval] reduceToNat (Int.toNat _) := reduceNatCore ``Int.toNat Int.toNat
 
-builtin_simproc [simp, seval] reduceNegSucc (Int.negSucc _) := fun e => do
-  let_expr Int.negSucc a ← e | return .continue
-  let some a ← getNatValue? a | return .continue
-  return .done { expr := toExpr (-(Int.ofNat a + 1)) }
-
-builtin_simproc [simp, seval] reduceOfNat (Int.ofNat _) := fun e => do
-  let_expr Int.ofNat a ← e | return .continue
-  let some a ← getNatValue? a | return .continue
-  return .done { expr := toExpr (Int.ofNat a) }
-
 end Int

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

@@ -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/UInt.lean

@@ -60,12 +60,6 @@ builtin_simproc [simp, seval] $(mkIdent `reduceOfNatCore):ident ($ofNatCore _ _)
   let value := $(mkIdent ofNat) value
   return .done { expr := toExpr value }
 
-builtin_simproc [simp, seval] $(mkIdent `reduceOfNat):ident ($(mkIdent ofNat) _) := fun e => do
-  unless e.isAppOfArity $(quote ofNat) 1 do return .continue
-  let some value ← Nat.fromExpr? e.appArg! | return .continue
-  let value := $(mkIdent ofNat) value
-  return .done { expr := toExpr value }
-
 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

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
@@ -257,22 +256,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/Parser/Command.lean

@@ -230,8 +230,6 @@ def «structure»          := leading_parser
   "#print " >> (ident <|> strLit)
 @[builtin_command_parser] def printAxioms    := leading_parser
   "#print " >> nonReservedSymbol "axioms " >> ident
-@[builtin_command_parser] def printEqns      := leading_parser
-  "#print " >> (nonReservedSymbol "equations " <|> nonReservedSymbol "eqns ") >> ident
 @[builtin_command_parser] def «init_quot»    := leading_parser
   "init_quot"
 def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit

src/Lean/Parser/Do.lean

@@ -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
@@ -159,10 +151,8 @@ def doMatchAlts := ppDedent <| matchAlts (rhsParser := doSeq)
   sepBy1 matchDiscr ", " >> " with" >> doMatchAlts
 
 def doMatchExprAlts := ppDedent <| matchExprAlts (rhsParser := doSeq)
-def optMetaFalse :=
-  optional (atomic ("(" >> nonReservedSymbol "meta" >>  " := " >> nonReservedSymbol "false" >> ") "))
 @[builtin_doElem_parser] def doMatchExpr := leading_parser:leadPrec
-  "match_expr " >> optMetaFalse >> termParser >> " with" >> doMatchExprAlts
+  "match_expr " >> optional ("(" >> nonReservedSymbol "meta" >>  " := " >> nonReservedSymbol "false" >> ") ") >> termParser >> " with" >> doMatchExprAlts
 
 def doCatch      := leading_parser
   ppDedent ppLine >> atomic ("catch " >> binderIdent) >> optional (" : " >> termParser) >> darrow >> doSeq

src/Lean/Parser/Term.lean

@@ -826,8 +826,7 @@ Implementation of the `show_term` term elaborator.
 `match_expr` support.
 -/
 
-def matchExprPat := leading_parser optional (atomic (ident >> "@")) >> ident >> many binderIdent
-def matchExprAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (matchExprPat >> " => " >> rhsParser)
+def matchExprAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (optional (atomic (ident >> "@")) >> ident >> many binderIdent >> " => " >> rhsParser)
 def matchExprElseAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (hole >> " => " >> rhsParser)
 def matchExprAlts (rhsParser : Parser) :=
   leading_parser withPosition $
@@ -836,9 +835,6 @@ def matchExprAlts (rhsParser : Parser) :=
 @[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

src/Lean/ParserCompiler.lean

@@ -87,7 +87,7 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do
       let c' := c ++ ctx.varName
       let cinfo ← getConstInfo c
       let resultTy ← forallTelescope cinfo.type fun _ b => pure b
-      if resultTy.isConstOf ``Lean.Parser.TrailingParser || resultTy.isConstOf ``Lean.Parser.Parser then do
+      if resultTy.isConstOf `Lean.Parser.TrailingParser || resultTy.isConstOf `Lean.Parser.Parser then do
         -- synthesize a new `[combinatorAttr c]`
         let some value ← pure cinfo.value?
           | throwError "don't know how to generate {ctx.varName} for non-definition '{e}'"
@@ -146,7 +146,7 @@ unsafe def registerParserCompiler {α} (ctx : Context α) : IO Unit := do
   Parser.registerParserAttributeHook {
     postAdd := fun catName constName builtin => do
       let info ← getConstInfo constName
-      if info.type.isConstOf ``Lean.ParserDescr || info.type.isConstOf ``Lean.TrailingParserDescr then
+      if info.type.isConstOf `Lean.ParserDescr || info.type.isConstOf `Lean.TrailingParserDescr then
         let d ← evalConstCheck ParserDescr `Lean.ParserDescr constName <|>
           evalConstCheck TrailingParserDescr `Lean.TrailingParserDescr constName
         compileEmbeddedParsers ctx d (builtin := builtin) |>.run'

src/Lean/Syntax.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Sebastian Ullrich, Leonardo de Moura
 -/
 prelude
-import Init.Data.Range
+import Init.Data.Range 
 import Init.Data.Hashable
 import Lean.Data.Name
 import Lean.Data.Format
@@ -37,9 +37,9 @@ inductive IsNode : Syntax → Prop where
 
 def SyntaxNode : Type := {s : Syntax // IsNode s }
 
-def unreachIsNodeMissing {β} : IsNode Syntax.missing → β := nofun
-def unreachIsNodeAtom {β} {info val} : IsNode (Syntax.atom info val) → β := nofun
-def unreachIsNodeIdent {β info rawVal val preresolved} : IsNode (Syntax.ident info rawVal val preresolved) → β := nofun
+def unreachIsNodeMissing {β} (h : IsNode Syntax.missing) : β := False.elim (nomatch h)
+def unreachIsNodeAtom {β} {info val} (h : IsNode (Syntax.atom info val)) : β := False.elim (nomatch h)
+def unreachIsNodeIdent {β info rawVal val preresolved} (h : IsNode (Syntax.ident info rawVal val preresolved)) : β := False.elim (nomatch h)
 
 def isLitKind (k : SyntaxNodeKind) : Bool :=
   k == strLitKind || k == numLitKind || k == charLitKind || k == nameLitKind || k == scientificLitKind

src/lake/tests/init/.gitignore

@@ -5,6 +5,6 @@
 /hello-exe
 /lean-data
 /123-hello
-/«A-B»-«C-D»
+/«A.B».«C.D»
 /meta
 /qed

src/runtime/object.cpp

@@ -579,7 +579,7 @@ struct scoped_current_task_object : flet<lean_task_object *> {
 
 class task_manager {
     mutex                                         m_mutex;
-    std::vector<std::unique_ptr<lthread>>         m_std_workers;
+    unsigned                                      m_num_std_workers{0};
     unsigned                                      m_idle_std_workers{0};
     unsigned                                      m_max_std_workers{0};
     unsigned                                      m_num_dedicated_workers{0};
@@ -588,6 +588,7 @@ class task_manager {
     unsigned                                      m_max_prio{0};
     condition_variable                            m_queue_cv;
     condition_variable                            m_task_finished_cv;
+    condition_variable                            m_worker_finished_cv;
     bool                                          m_shutting_down{false};
 
     lean_task_object * dequeue() {
@@ -618,7 +619,7 @@ class task_manager {
             m_max_prio = prio;
         m_queues[prio].push_back(t);
         m_queues_size++;
-        if (!m_idle_std_workers && m_std_workers.size() < m_max_std_workers)
+        if (!m_idle_std_workers && m_num_std_workers < m_max_std_workers)
             spawn_worker();
         else
             m_queue_cv.notify_one();
@@ -643,10 +644,8 @@ class task_manager {
     }
 
     void spawn_worker() {
-        if (m_shutting_down)
-            return;
-
-        m_std_workers.emplace_back(new lthread([this]() {
+        m_num_std_workers++;
+        lthread([this]() {
             save_stack_info(false);
             unique_lock<mutex> lock(m_mutex);
             m_idle_std_workers++;
@@ -666,7 +665,10 @@ class task_manager {
                 reset_heartbeat();
             }
             m_idle_std_workers--;
-        }));
+            m_num_std_workers--;
+            m_worker_finished_cv.notify_all();
+        });
+        // `lthread` will be implicitly freed, which frees up its control resources but does not terminate the thread
     }
 
     void spawn_dedicated_worker(lean_task_object * t) {
@@ -676,8 +678,9 @@ class task_manager {
             unique_lock<mutex> lock(m_mutex);
             run_task(lock, t);
             m_num_dedicated_workers--;
+            m_worker_finished_cv.notify_all();
         });
-        // `lthread` will be implicitly freed, which frees up its control resources but does not terminate the thread
+        // see above
     }
 
     void run_task(unique_lock<mutex> & lock, lean_task_object * t) {
@@ -766,18 +769,11 @@ public:
     }
 
     ~task_manager() {
-        {
-            unique_lock<mutex> lock(m_mutex);
-            m_shutting_down = true;
-            // we can assume that `m_std_workers` will not be changed after this line
-        }
+        unique_lock<mutex> lock(m_mutex);
+        m_shutting_down = true;
         m_queue_cv.notify_all();
-#ifndef LEAN_EMSCRIPTEN
         // wait for all workers to finish
-        for (auto & t : m_std_workers)
-            t->join();
-        // never seems to terminate under Emscripten
-#endif
+        m_worker_finished_cv.wait(lock, [&]() { return m_num_std_workers + m_num_dedicated_workers == 0; });
     }
 
     void enqueue(lean_task_object * t) {

tests/lean/binrelTypeMismatch.lean

@@ -1,20 +0,0 @@
-/-!
-# Testing that type mismatch errors for binary operations are localized to the LHS or RHS
-
-Before #3442, the error was placed on the entire expression than just the RHS.
--/
-
-/-!
-When there's no max type, the ensureHasType failure is localized to the RHS.
--/
-#check true = ()
-
-/-!
-When there's no max type, toBoolIfNecessary error is localized to LHS.
--/
-#check ∀ (p : Prop), p == ()
-
-/-!
-When there's no max type, toBoolIfNecessary error is localized to RHS.
--/
-#check ∀ (p : Prop), () == p

tests/lean/binrelTypeMismatch.lean.expected.out

@@ -1,20 +0,0 @@
-binrelTypeMismatch.lean:10:14-10:16: error: type mismatch
-  ()
-has type
-  Unit : Type
-but is expected to have type
-  Bool : Type
-binrelTypeMismatch.lean:15:21-15:22: error: type mismatch
-  p
-has type
-  Prop : Type
-but is expected to have type
-  Bool : Type
-Prop → sorryAx (Sort u_1) true : Sort (imax 1 u_1)
-binrelTypeMismatch.lean:20:27-20:28: error: type mismatch
-  p
-has type
-  Prop : Type
-but is expected to have type
-  Bool : Type
-Prop → sorryAx (Sort u_1) true : Sort (imax 1 u_1)

tests/lean/run/3524.lean

@@ -1,3 +0,0 @@
-example (a : Nat) : ((2 ^ 7) + a) - 2 ^ 7 = 0 := by
-  generalize 0 - 0 = x
-  sorry

tests/lean/run/3547.lean

@@ -1,11 +0,0 @@
-def foo : Nat → Nat
-  | 0 => 0
-  | n+1 => foo n
-decreasing_by decreasing_tactic
-
-/--
-info: Try this: simp only [foo]
--/
-#guard_msgs in
-def foo2 : foo 2 = 0 := by
-  simp? [foo]

tests/lean/run/foldLits.lean

@@ -1,56 +0,0 @@
-open BitVec
-
-example : (Fin.mk 5 (by decide) : Fin 10) + 2 = x := by
-  simp
-  guard_target =ₛ 7 = x
-  sorry
-
-example : (Fin.mk 5 (by decide) : Fin 10) + 2 = x := by
-  simp (config := { ground := true }) only
-  guard_target =ₛ 7 = x
-  sorry
-
-example : (BitVec.ofFin (Fin.mk 2 (by decide)) : BitVec 32) + 2 = x := by
-  simp
-  guard_target =ₛ 4#32 = x
-  sorry
-
-example : (BitVec.ofFin (Fin.mk 2 (by decide)) : BitVec 32) + 2 = x := by
-  simp (config := { ground := true }) only
-  guard_target =ₛ 4#32 = x
-  sorry
-
-example : (BitVec.ofFin 2 : BitVec 32) + 2 = x := by
-  simp
-  guard_target =ₛ 4#32 = x
-  sorry
-
-example (h : -2 = x) : Int.negSucc 3 + 2 = x := by
-  simp
-  guard_target =ₛ -2 = x
-  assumption
-
-example (h : -2 = x) : Int.negSucc 3 + 2 = x := by
-  simp (config := { ground := true }) only
-  guard_target =ₛ -2 = x
-  assumption
-
-example : Int.ofNat 3 + 2 = x := by
-  simp
-  guard_target =ₛ 5 = x
-  sorry
-
-example : Int.ofNat 3 + 2 = x := by
-  simp (config := { ground := true }) only
-  guard_target =ₛ 5 = x
-  sorry
-
-example (h : 5 = x) : UInt32.ofNat 2 + 3 = x := by
-  simp
-  guard_target =ₛ 5 = x
-  assumption
-
-example (h : 5 = x) : UInt32.ofNat 2 + 3 = x := by
-  simp (config := { ground := true }) only
-  guard_target =ₛ 5 = x
-  assumption

tests/lean/run/match_expr.lean

@@ -54,65 +54,3 @@ run_meta do
   discard <| isDefEq m e
   let m ← test2 m
   logInfo m
-
-def test3 (e : Expr) : Option Expr :=
-  let_expr c@Eq α a b := e | none
-  some (mkApp3 c α b a)
-
-def test4 (e : Expr) : Option Expr :=
-  let_expr Eq.refl _ a := e | none
-  some a
-
-/--
-info: 3 = 1
----
-info: 3
----
-info: 4 = 2
--/
-#guard_msgs in
-run_meta do
-  let eq ← mkEq (toExpr 1) (toExpr 3)
-  let eq := mkAnnotation `foo eq
-  let some eq := test3 eq | throwError "unexpected"
-  logInfo eq
-  let rfl ← mkEqRefl (toExpr 3)
-  let some n := test4 rfl | throwError "unexpected"
-  logInfo n
-  let eq := mkAnnotation `boo <| mkApp (mkAnnotation `bla (mkApp (mkAnnotation `foo eq.appFn!.appFn!) (toExpr 2))) (toExpr 4)
-  let some eq := test3 eq | throwError "unexpected"
-  logInfo eq
-
-def test5 (e : Expr) : MetaM Expr := do
-  let_expr HAdd.hAdd _ _ _ _ a b ← e
-    | return e
-  mkSub a b
-
-def test6 (e : Expr) : MetaM Expr := do
-  let_expr HAdd.hAdd _ _ _ _ a b := e
-    | return e
-  mkSub a b
-
-/--
-info: 2 - 5
----
-info: 2 - 5
----
-info: 2 - 5
--/
-#guard_msgs in
-run_meta do
-  let e ← mkAdd (toExpr 2) (toExpr 5)
-  let e' ← test5 e
-  logInfo e'
-  let e' ← test6 e
-  logInfo e'
-  let m ← mkFreshExprMVar none
-  let m ← test5 m
-  assert! m.isMVar
-  discard <| isDefEq m e
-  let m' ← test5 m
-  logInfo m'
-  assert! m.isMVar
-  let m' ← test6 m -- does not instantiate mvars
-  assert! m'.isMVar

tests/lean/run/match_expr_expected_type_issue.lean

@@ -1,14 +0,0 @@
-import Lean
-
-open Lean Meta Simp
-
-def foo' (e : Expr) : SimpM Step := do
-  let_expr Neg.neg _ _ arg ← e | return .continue
-  match_expr arg with
-  | OfNat.ofNat _ _ _ => return .done { expr := e }
-  | _ =>
-    let some v ← getIntValue? arg | return .continue
-    if v < 0 then
-      return .done { expr := toExpr (- v) }
-    else
-      return .done { expr := toExpr v }

tests/lean/run/match_expr_meta_modifier.lean

@@ -1,13 +0,0 @@
-import Lean
-
-open Lean Meta
-
-def f1 (e : Expr) : MetaM Expr := do
-  match_expr (← whnf e) with
-  | And a b => mkAppM ``And #[b, a]
-  | _ => return e
-
-def f2 (e : Expr) : MetaM Expr := do
-  match_expr (meta := false) (← whnf e) with
-  | And a b => mkAppM ``And #[b, a]
-  | _ => return e

tests/lean/run/match_expr_perf.lean

@@ -1,63 +0,0 @@
-/-
-Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
--/
-prelude
-import Lean.Elab.Tactic.Omega.Core
-import Lean.Elab.Tactic.FalseOrByContra
-import Lean.Meta.Tactic.Cases
-import Lean.Elab.Tactic.Config
-
-open Lean Meta Omega
-
-set_option maxHeartbeats 5000
-def pushNot (h P : Expr) : MetaM (Option Expr) := do
-  let P ← whnfR P
-  trace[omega] "pushing negation: {P}"
-  match P with
-  | .forallE _ t b _ =>
-    if (← isProp t) && (← isProp b) then
-     return some (mkApp4 (.const ``Decidable.and_not_of_not_imp []) t b
-      (.app (.const ``Classical.propDecidable []) t) h)
-    else
-      return none
-  | .app _ _ =>
-    match_expr P with
-    | LT.lt α _ x y => match_expr α with
-      | Nat => return some (mkApp3 (.const ``Nat.le_of_not_lt []) x y h)
-      | Int => return some (mkApp3 (.const ``Int.le_of_not_lt []) x y h)
-      | Fin n => return some (mkApp4 (.const ``Fin.le_of_not_lt []) n x y h)
-      | _ => return none
-    | LE.le α _ x y => match_expr α with
-      | Nat => return some (mkApp3 (.const ``Nat.lt_of_not_le []) x y h)
-      | Int => return some (mkApp3 (.const ``Int.lt_of_not_le []) x y h)
-      | Fin n => return some (mkApp4 (.const ``Fin.lt_of_not_le []) n x y h)
-      | _ => return none
-    | Eq α x y => match_expr α with
-      | Nat => return some (mkApp3 (.const ``Nat.lt_or_gt_of_ne []) x y h)
-      | Int => return some (mkApp3 (.const ``Int.lt_or_gt_of_ne []) x y h)
-      | Fin n => return some (mkApp4 (.const ``Fin.lt_or_gt_of_ne []) n x y h)
-      | _ => return none
-    | Dvd.dvd α _ k x => match_expr α with
-      | Nat => return some (mkApp3 (.const ``Nat.emod_pos_of_not_dvd []) k x h)
-      | Int =>
-        -- This introduces a disjunction that could be avoided by checking `k ≠ 0`.
-        return some (mkApp3 (.const ``Int.emod_pos_of_not_dvd []) k x h)
-      | _ => return none
-    | Prod.Lex _ _ _ _ _ _ => return some (← mkAppM ``Prod.of_not_lex #[h])
-    | Not P =>
-      return some (mkApp3 (.const ``Decidable.of_not_not []) P
-        (.app (.const ``Classical.propDecidable []) P) h)
-    | And P Q =>
-      return some (mkApp5 (.const ``Decidable.or_not_not_of_not_and []) P Q
-        (.app (.const ``Classical.propDecidable []) P)
-        (.app (.const ``Classical.propDecidable []) Q) h)
-    | Or P Q =>
-      return some (mkApp3 (.const ``and_not_not_of_not_or []) P Q h)
-    | Iff P Q =>
-      return some (mkApp5 (.const ``Decidable.and_not_or_not_and_of_not_iff []) P Q
-        (.app (.const ``Classical.propDecidable []) P)
-        (.app (.const ``Classical.propDecidable []) Q) h)
-    | _ => return none
-  | _ => return none

tests/lean/run/printEqns.lean

@@ -1,31 +0,0 @@
-/--
-info: equations:
-private theorem List.append._eq_1.{u} : ∀ {α : Type u} (x : List α), List.append [] x = x
-private theorem List.append._eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : List α),
-  List.append (a :: l) x = a :: List.append l x
--/
-#guard_msgs in
-#print eqns List.append
-
-/--
-info: equations:
-private theorem List.append._eq_1.{u} : ∀ {α : Type u} (x : List α), List.append [] x = x
-private theorem List.append._eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : List α),
-  List.append (a :: l) x = a :: List.append l x
--/
-#guard_msgs in
-#print equations List.append
-
-@[simp] def ack : Nat → Nat → Nat
-  | 0,   y   => y+1
-  | x+1, 0   => ack x 1
-  | x+1, y+1 => ack x (ack (x+1) y)
-
-/--
-info: equations:
-private theorem ack._eq_1 : ∀ (x : Nat), ack 0 x = x + 1
-private theorem ack._eq_2 : ∀ (x_2 : Nat), ack (Nat.succ x_2) 0 = ack x_2 1
-private theorem ack._eq_3 : ∀ (x_2 y : Nat), ack (Nat.succ x_2) (Nat.succ y) = ack x_2 (ack (x_2 + 1) y)
--/
-#guard_msgs in
-#print eqns ack

tests/lean/run/renameI.lean

@@ -5,19 +5,3 @@ example : ∀ a b c d : Nat, a = b → a = d → a = c → c = b := by
   apply Eq.symm
   exact h2
   exact h1
-
-/-!
-Within a tactic macro, all identifiers *not* from this quotation should be regarded as inaccessible.
--/
-
-macro "my_tac " h:ident : tactic =>
- `(tactic| (
-   cases $h:ident
-   rename_i h_p3
-   rename_i h_p1_p2 -- must rename `left`, not `h_p3`
-   cases h_p1_p2  -- fails otherwise
-   ))
-
-example (h : (p1 ∧ p2) ∧ p3) : True := by
-  my_tac h
-  sorry