chore: migrate Std.Data.Array.Init.Basic

src/Init.lean

@@ -7,8 +7,6 @@ prelude
 import Init.Prelude
 import Init.Notation
 import Init.Tactics
-import Init.TacticsExtra
-import Init.RCases
 import Init.Core
 import Init.Control
 import Init.Data.Basic
@@ -25,6 +23,5 @@ import Init.NotationExtra
 import Init.SimpLemmas
 import Init.Hints
 import Init.Conv
-import Init.Guard
 import Init.Simproc
 import Init.SizeOfLemmas

src/Init/Classical.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Mario Carneiro
+Authors: Leonardo de Moura
 -/
 prelude
 import Init.Core
@@ -123,15 +123,21 @@ theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
 theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
   Decidable.byContradiction (dec := propDecidable _) h
 
-end Classical
-
 /--
 `by_cases (h :)? p` splits the main goal into two cases, assuming `h : p` in the first branch, and `h : ¬ p` in the second branch.
 -/
 syntax "by_cases " (atomic(ident " : "))? term : tactic
 
-macro_rules
-  | `(tactic| by_cases $e) => `(tactic| by_cases h : $e)
 macro_rules
   | `(tactic| by_cases $h : $e) =>
-    `(tactic| open Classical in refine if $h:ident : $e then ?pos else ?neg)
+    `(tactic|
+      cases em $e with
+      | inl $h => _
+      | inr $h => _)
+  | `(tactic| by_cases $e) =>
+    `(tactic|
+      cases em $e with
+      | inl h => _
+      | inr h => _)
+
+end Classical

src/Init/Coe.lean

@@ -290,12 +290,6 @@ between e.g. `↑x + ↑y` and `↑(x + y)`.
 -/
 syntax:1024 (name := coeNotation) "↑" term:1024 : term
 
-/-- `⇑ t` coerces `t` to a function. -/
-syntax:1024 (name := coeFunNotation) "⇑" term:1024 : term
-
-/-- `↥ t` coerces `t` to a type. -/
-syntax:1024 (name := coeSortNotation) "↥" term:1024 : term
-
 /-! # Basic instances -/
 
 instance boolToProp : Coe Bool Prop where

src/Init/Core.lean

@@ -666,8 +666,6 @@ theorem Iff.refl (a : Prop) : a ↔ a :=
 protected theorem Iff.rfl {a : Prop} : a ↔ a :=
   Iff.refl a
 
-macro_rules | `(tactic| rfl) => `(tactic| exact Iff.rfl)
-
 theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
   Iff.intro
     (fun ha => Iff.mp h₂ (Iff.mp h₁ ha))

src/Init/Data/AC.lean

@@ -150,18 +150,18 @@ theorem Context.evalList_mergeIdem (ctx : Context α) (h : ContextInformation.is
       rfl
     | cons z zs =>
       by_cases h₂ : x = y
-      case pos =>
+      case inl =>
         rw [h₂, mergeIdem_head, ih]
         simp [evalList, ←ctx.assoc.1, h.1, EvalInformation.evalOp]
-      case neg =>
+      case inr =>
         rw [mergeIdem_head2]
         by_cases h₃ : y = z
-        case pos =>
+        case inl =>
           simp [mergeIdem_head, h₃, evalList]
           cases h₄ : mergeIdem (z :: zs) with
           | nil => apply absurd h₄; apply mergeIdem_nonEmpty; simp
           | cons u us => simp_all [mergeIdem, mergeIdem.loop, evalList]
-        case neg =>
+        case inr =>
           simp [mergeIdem_head2, h₃, evalList] at *
           rw [ih]
         assumption

src/Init/Data/String/Basic.lean

@@ -515,12 +515,6 @@ def replace (s pattern replacement : String) : String :=
       termination_by s.endPos.1 - pos.1
     loop "" 0 0
 
-/-- Return the beginning of the line that contains character `pos`. -/
-def findLineStart (s : String) (pos : String.Pos) : String.Pos :=
-  match s.revFindAux (· = '\n') pos with
-  | none => 0
-  | some n => ⟨n.byteIdx + 1⟩
-
 end String
 
 namespace Substring

src/Init/Guard.lean

@@ -1,129 +0,0 @@
-/-
-Copyright (c) 2021 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro
--/
-prelude
-import Init.Tactics
-import Init.Conv
-import Init.NotationExtra
-
-namespace Lean.Parser
-
-/-- Reducible defeq matching for `guard_hyp` types -/
-syntax colonR := " : "
-/-- Default-reducibility defeq matching for `guard_hyp` types -/
-syntax colonD := " :~ "
-/-- Syntactic matching for `guard_hyp` types -/
-syntax colonS := " :ₛ "
-/-- Alpha-eq matching for `guard_hyp` types -/
-syntax colonA := " :ₐ "
-/-- The `guard_hyp` type specifier, one of `:`, `:~`, `:ₛ`, `:ₐ` -/
-syntax colon := colonR <|> colonD <|> colonS <|> colonA
-
-/-- Reducible defeq matching for `guard_hyp` values -/
-syntax colonEqR := " := "
-/-- Default-reducibility defeq matching for `guard_hyp` values -/
-syntax colonEqD := " :=~ "
-/-- Syntactic matching for `guard_hyp` values -/
-syntax colonEqS := " :=ₛ "
-/-- Alpha-eq matching for `guard_hyp` values -/
-syntax colonEqA := " :=ₐ "
-/-- The `guard_hyp` value specifier, one of `:=`, `:=~`, `:=ₛ`, `:=ₐ` -/
-syntax colonEq := colonEqR <|> colonEqD <|> colonEqS <|> colonEqA
-
-/-- Reducible defeq matching for `guard_expr` -/
-syntax equalR := " = "
-/-- Default-reducibility defeq matching for `guard_expr` -/
-syntax equalD := " =~ "
-/-- Syntactic matching for `guard_expr` -/
-syntax equalS := " =ₛ "
-/-- Alpha-eq matching for `guard_expr` -/
-syntax equalA := " =ₐ "
-/-- The `guard_expr` matching specifier, one of `=`, `=~`, `=ₛ`, `=ₐ` -/
-syntax equal := equalR <|> equalD <|> equalS <|> equalA
-
-namespace Tactic
-
-/--
-Tactic to check equality of two expressions.
-* `guard_expr e = e'` checks that `e` and `e'` are defeq at reducible transparency.
-* `guard_expr e =~ e'` checks that `e` and `e'` are defeq at default transparency.
-* `guard_expr e =ₛ e'` checks that `e` and `e'` are syntactically equal.
-* `guard_expr e =ₐ e'` checks that `e` and `e'` are alpha-equivalent.
-
-Both `e` and `e'` are elaborated then have their metavariables instantiated before the equality
-check. Their types are unified (using `isDefEqGuarded`) before synthetic metavariables are
-processed, which helps with default instance handling.
--/
-syntax (name := guardExpr) "guard_expr " term:51 equal term : tactic
-@[inherit_doc guardExpr]
-syntax (name := guardExprConv) "guard_expr " term:51 equal term : conv
-
-/--
-Tactic to check that the target agrees with a given expression.
-* `guard_target = e` checks that the target is defeq at reducible transparency to `e`.
-* `guard_target =~ e` checks that the target is defeq at default transparency to `e`.
-* `guard_target =ₛ e` checks that the target is syntactically equal to `e`.
-* `guard_target =ₐ e` checks that the target is alpha-equivalent to `e`.
-
-The term `e` is elaborated with the type of the goal as the expected type, which is mostly
-useful within `conv` mode.
--/
-syntax (name := guardTarget) "guard_target " equal term : tactic
-@[inherit_doc guardTarget]
-syntax (name := guardTargetConv) "guard_target " equal term : conv
-
-/--
-Tactic to check that a named hypothesis has a given type and/or value.
-
-* `guard_hyp h : t` checks the type up to reducible defeq,
-* `guard_hyp h :~ t` checks the type up to default defeq,
-* `guard_hyp h :ₛ t` checks the type up to syntactic equality,
-* `guard_hyp h :ₐ t` checks the type up to alpha equality.
-* `guard_hyp h := v` checks value up to reducible defeq,
-* `guard_hyp h :=~ v` checks value up to default defeq,
-* `guard_hyp h :=ₛ v` checks value up to syntactic equality,
-* `guard_hyp h :=ₐ v` checks the value up to alpha equality.
-
-The value `v` is elaborated using the type of `h` as the expected type.
--/
-syntax (name := guardHyp)
-  "guard_hyp " term:max (colon term)? (colonEq term)? : tactic
-@[inherit_doc guardHyp] syntax (name := guardHypConv)
-  "guard_hyp " term:max (colon term)? (colonEq term)? : conv
-
-end Tactic
-
-namespace Command
-
-/--
-Command to check equality of two expressions.
-* `#guard_expr e = e'` checks that `e` and `e'` are defeq at reducible transparency.
-* `#guard_expr e =~ e'` checks that `e` and `e'` are defeq at default transparency.
-* `#guard_expr e =ₛ e'` checks that `e` and `e'` are syntactically equal.
-* `#guard_expr e =ₐ e'` checks that `e` and `e'` are alpha-equivalent.
-
-This is a command version of the `guard_expr` tactic. -/
-syntax (name := guardExprCmd) "#guard_expr " term:51 equal term : command
-
-/--
-Command to check that an expression evaluates to `true`.
-
-`#guard e` elaborates `e` ensuring its type is `Bool` then evaluates `e` and checks that
-the result is `true`. The term is elaborated *without* variables declared using `variable`, since
-these cannot be evaluated.
-
-Since this makes use of coercions, so long as a proposition `p` is decidable, one can write
-`#guard p` rather than `#guard decide p`. A consequence to this is that if there is decidable
-equality one can write `#guard a = b`. Note that this is not exactly the same as checking
-if `a` and `b` evaluate to the same thing since it uses the `DecidableEq` instance to do
-the evaluation.
-
-Note: this uses the untrusted evaluator, so `#guard` passing is *not* a proof that the
-expression equals `true`. -/
-syntax (name := guardCmd) "#guard " term : command
-
-end Command
-
-end Lean.Parser

src/Init/Notation.lean

@@ -268,7 +268,6 @@ syntax (name := rawNatLit) "nat_lit " num : term
 @[inherit_doc] infixr:90 " ∘ "  => Function.comp
 @[inherit_doc] infixr:35 " × "  => Prod
 
-@[inherit_doc] infix:50  " ∣ " => Dvd.dvd
 @[inherit_doc] infixl:55 " ||| " => HOr.hOr
 @[inherit_doc] infixl:58 " ^^^ " => HXor.hXor
 @[inherit_doc] infixl:60 " &&& " => HAnd.hAnd
@@ -485,13 +484,6 @@ existing code. It may be removed in a future version of the library.
 -/
 syntax (name := deprecated) "deprecated" (ppSpace ident)? : attr
 
-/--
-The `@[coe]` attribute on a function (which should also appear in a
-`instance : Coe A B := ⟨myFn⟩` declaration) allows the delaborator to show
-applications of this function as `↑` when printing expressions.
--/
-syntax (name := Attr.coe) "coe" : attr
-
 /--
 When `parent_dir` contains the current Lean file, `include_str "path" / "to" / "file"` becomes
 a string literal with the contents of the file at `"parent_dir" / "path" / "to" / "file"`. If this

src/Init/Prelude.lean

@@ -1314,11 +1314,6 @@ class Mod (α : Type u) where
   /-- `a % b` computes the remainder upon dividing `a` by `b`. See `HMod`. -/
   mod : α → α → α
 
-/-- Notation typeclass for the `∣` operation (typed as `\|`), which represents divisibility. -/
-class Dvd (α : Type _) where
-  /-- Divisibility. `a ∣ b` (typed as `\|`) means that there is some `c` such that `b = a * c`. -/
-  dvd : α → α → Prop
-
 /--
 The homogeneous version of `HPow`: `a ^ b : α` where `a : α`, `b : β`.
 (The right argument is not the same as the left since we often want this even

src/Init/RCases.lean

@@ -1,192 +0,0 @@
-/-
-Copyright (c) 2017 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Jacob von Raumer
--/
-prelude
-import Init.Tactics
-import Init.NotationExtra
-
-/-!
-# Recursive cases (`rcases`) tactic and related tactics
-
-`rcases` is a tactic that will perform `cases` recursively, according to a pattern. It is used to
-destructure hypotheses or expressions composed of inductive types like `h1 : a ∧ b ∧ c ∨ d` or
-`h2 : ∃ x y, trans_rel R x y`. Usual usage might be `rcases h1 with ⟨ha, hb, hc⟩ | hd` or
-`rcases h2 with ⟨x, y, _ | ⟨z, hxz, hzy⟩⟩` for these examples.
-
-Each element of an `rcases` pattern is matched against a particular local hypothesis (most of which
-are generated during the execution of `rcases` and represent individual elements destructured from
-the input expression). An `rcases` pattern has the following grammar:
-
-* A name like `x`, which names the active hypothesis as `x`.
-* A blank `_`, which does nothing (letting the automatic naming system used by `cases` name the
-  hypothesis).
-* A hyphen `-`, which clears the active hypothesis and any dependents.
-* The keyword `rfl`, which expects the hypothesis to be `h : a = b`, and calls `subst` on the
-  hypothesis (which has the effect of replacing `b` with `a` everywhere or vice versa).
-* A type ascription `p : ty`, which sets the type of the hypothesis to `ty` and then matches it
-  against `p`. (Of course, `ty` must unify with the actual type of `h` for this to work.)
-* A tuple pattern `⟨p1, p2, p3⟩`, which matches a constructor with many arguments, or a series
-  of nested conjunctions or existentials. For example if the active hypothesis is `a ∧ b ∧ c`,
-  then the conjunction will be destructured, and `p1` will be matched against `a`, `p2` against `b`
-  and so on.
-* A `@` before a tuple pattern as in `@⟨p1, p2, p3⟩` will bind all arguments in the constructor,
-  while leaving the `@` off will only use the patterns on the explicit arguments.
-* An alternation pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
-  or a nested disjunction like `a ∨ b ∨ c`.
-
-The patterns are fairly liberal about the exact shape of the constructors, and will insert
-additional alternation branches and tuple arguments if there are not enough arguments provided, and
-reuse the tail for further matches if there are too many arguments provided to alternation and
-tuple patterns.
-
-This file also contains the `obtain` and `rintro` tactics, which use the same syntax of `rcases`
-patterns but with a slightly different use case:
-
-* `rintro` (or `rintros`) is used like `rintro x ⟨y, z⟩` and is the same as `intros` followed by
-  `rcases` on the newly introduced arguments.
-* `obtain` is the same as `rcases` but with a syntax styled after `have` rather than `cases`.
-  `obtain ⟨hx, hy⟩ | hz := foo` is equivalent to `rcases foo with ⟨hx, hy⟩ | hz`. Unlike `rcases`,
-  `obtain` also allows one to omit `:= foo`, although a type must be provided in this case,
-  as in `obtain ⟨hx, hy⟩ | hz : a ∧ b ∨ c`, in which case it produces a subgoal for proving
-  `a ∧ b ∨ c` in addition to the subgoals `hx : a, hy : b |- goal` and `hz : c |- goal`.
-
-## Tags
-
-rcases, rintro, obtain, destructuring, cases, pattern matching, match
--/
-namespace Lean.Parser.Tactic
-
-/-- The syntax category of `rcases` patterns. -/
-declare_syntax_cat rcasesPat
-/-- A medium precedence `rcases` pattern is a list of `rcasesPat` separated by `|` -/
-syntax rcasesPatMed := sepBy1(rcasesPat, " | ")
-/-- A low precedence `rcases` pattern is a `rcasesPatMed` optionally followed by `: ty` -/
-syntax rcasesPatLo := rcasesPatMed (" : " term)?
-/-- `x` is a pattern which binds `x` -/
-syntax (name := rcasesPat.one) ident : rcasesPat
-/-- `_` is a pattern which ignores the value and gives it an inaccessible name -/
-syntax (name := rcasesPat.ignore) "_" : rcasesPat
-/-- `-` is a pattern which removes the value from the context -/
-syntax (name := rcasesPat.clear) "-" : rcasesPat
-/--
-A `@` before a tuple pattern as in `@⟨p1, p2, p3⟩` will bind all arguments in the constructor,
-while leaving the `@` off will only use the patterns on the explicit arguments.
--/
-syntax (name := rcasesPat.explicit) "@" noWs rcasesPat : rcasesPat
-/--
-`⟨pat, ...⟩` is a pattern which matches on a tuple-like constructor
-or multi-argument inductive constructor
--/
-syntax (name := rcasesPat.tuple) "⟨" rcasesPatLo,* "⟩" : rcasesPat
-/-- `(pat)` is a pattern which resets the precedence to low -/
-syntax (name := rcasesPat.paren) "(" rcasesPatLo ")" : rcasesPat
-
-/-- The syntax category of `rintro` patterns. -/
-declare_syntax_cat rintroPat
-/-- An `rcases` pattern is an `rintro` pattern -/
-syntax (name := rintroPat.one) rcasesPat : rintroPat
-/--
-A multi argument binder `(pat1 pat2 : ty)` binds a list of patterns and gives them all type `ty`.
--/
-syntax (name := rintroPat.binder) (priority := default+1) -- to override rcasesPat.paren
-  "(" rintroPat+ (" : " term)? ")" : rintroPat
-
-/- TODO
-/--
-`rcases? e` will perform case splits on `e` in the same way as `rcases e`,
-but rather than accepting a pattern, it does a maximal cases and prints the
-pattern that would produce this case splitting. The default maximum depth is 5,
-but this can be modified with `rcases? e : n`.
--/
-syntax (name := rcases?) "rcases?" casesTarget,* (" : " num)? : tactic
--/
-
-/--
-`rcases` is a tactic that will perform `cases` recursively, according to a pattern. It is used to
-destructure hypotheses or expressions composed of inductive types like `h1 : a ∧ b ∧ c ∨ d` or
-`h2 : ∃ x y, trans_rel R x y`. Usual usage might be `rcases h1 with ⟨ha, hb, hc⟩ | hd` or
-`rcases h2 with ⟨x, y, _ | ⟨z, hxz, hzy⟩⟩` for these examples.
-
-Each element of an `rcases` pattern is matched against a particular local hypothesis (most of which
-are generated during the execution of `rcases` and represent individual elements destructured from
-the input expression). An `rcases` pattern has the following grammar:
-
-* A name like `x`, which names the active hypothesis as `x`.
-* A blank `_`, which does nothing (letting the automatic naming system used by `cases` name the
-  hypothesis).
-* A hyphen `-`, which clears the active hypothesis and any dependents.
-* The keyword `rfl`, which expects the hypothesis to be `h : a = b`, and calls `subst` on the
-  hypothesis (which has the effect of replacing `b` with `a` everywhere or vice versa).
-* A type ascription `p : ty`, which sets the type of the hypothesis to `ty` and then matches it
-  against `p`. (Of course, `ty` must unify with the actual type of `h` for this to work.)
-* A tuple pattern `⟨p1, p2, p3⟩`, which matches a constructor with many arguments, or a series
-  of nested conjunctions or existentials. For example if the active hypothesis is `a ∧ b ∧ c`,
-  then the conjunction will be destructured, and `p1` will be matched against `a`, `p2` against `b`
-  and so on.
-* A `@` before a tuple pattern as in `@⟨p1, p2, p3⟩` will bind all arguments in the constructor,
-  while leaving the `@` off will only use the patterns on the explicit arguments.
-* An alteration pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
-  or a nested disjunction like `a ∨ b ∨ c`.
-
-A pattern like `⟨a, b, c⟩ | ⟨d, e⟩` will do a split over the inductive datatype,
-naming the first three parameters of the first constructor as `a,b,c` and the
-first two of the second constructor `d,e`. If the list is not as long as the
-number of arguments to the constructor or the number of constructors, the
-remaining variables will be automatically named. If there are nested brackets
-such as `⟨⟨a⟩, b | c⟩ | d` then these will cause more case splits as necessary.
-If there are too many arguments, such as `⟨a, b, c⟩` for splitting on
-`∃ x, ∃ y, p x`, then it will be treated as `⟨a, ⟨b, c⟩⟩`, splitting the last
-parameter as necessary.
-
-`rcases` also has special support for quotient types: quotient induction into Prop works like
-matching on the constructor `quot.mk`.
-
-`rcases h : e with PAT` will do the same as `rcases e with PAT` with the exception that an
-assumption `h : e = PAT` will be added to the context.
--/
-syntax (name := rcases) "rcases" casesTarget,* (" with " rcasesPatLo)? : tactic
-
-/--
-The `obtain` tactic is a combination of `have` and `rcases`. See `rcases` for
-a description of supported patterns.
-
-```lean
-obtain ⟨patt⟩ : type := proof
-```
-is equivalent to
-```lean
-have h : type := proof
-rcases h with ⟨patt⟩
-```
-
-If `⟨patt⟩` is omitted, `rcases` will try to infer the pattern.
-
-If `type` is omitted, `:= proof` is required.
--/
-syntax (name := obtain) "obtain" (ppSpace rcasesPatMed)? (" : " term)? (" := " term,+)? : tactic
-
-/- TODO
-/--
-`rintro?` will introduce and case split on variables in the same way as
-`rintro`, but will also print the `rintro` invocation that would have the same
-result. Like `rcases?`, `rintro? : n` allows for modifying the
-depth of splitting; the default is 5.
--/
-syntax (name := rintro?) "rintro?" (" : " num)? : tactic
--/
-
-/--
-The `rintro` tactic is a combination of the `intros` tactic with `rcases` to
-allow for destructuring patterns while introducing variables. See `rcases` for
-a description of supported patterns. For example, `rintro (a | ⟨b, c⟩) ⟨d, e⟩`
-will introduce two variables, and then do case splits on both of them producing
-two subgoals, one with variables `a d e` and the other with `b c d e`.
-
-`rintro`, unlike `rcases`, also supports the form `(x y : ty)` for introducing
-and type-ascripting multiple variables at once, similar to binders.
--/
-syntax (name := rintro) "rintro" (ppSpace colGt rintroPat)+ (" : " term)? : tactic
-
-end Lean.Parser.Tactic

src/Init/System/Promise.lean

@@ -6,15 +6,11 @@ Authors: Gabriel Ebner
 prelude
 import Init.System.IO
 
-set_option linter.missingDocs true
-
 namespace IO
 
-private opaque PromisePointed : NonemptyType.{0}
-
-private structure PromiseImpl (α : Type) : Type where
-  prom : PromisePointed.type
-  h    : Nonempty α
+/-- Internally, a `Promise` is just a `Task` that is in the "Promised" or "Finished" state. -/
+private opaque PromiseImpl (α : Type) : { P : Type // Nonempty α ↔ Nonempty P } :=
+  ⟨Task α, fun ⟨_⟩ => ⟨⟨‹_›⟩⟩, fun ⟨⟨_⟩⟩ => ⟨‹_›⟩⟩
 
 /--
 `Promise α` allows you to create a `Task α` whose value is provided later by calling `resolve`.
@@ -30,10 +26,10 @@ Every promise must eventually be resolved.
 Otherwise the memory used for the promise will be leaked,
 and any tasks depending on the promise's result will wait forever.
 -/
-def Promise (α : Type) : Type := PromiseImpl α
+def Promise (α : Type) : Type := (PromiseImpl α).1
 
-instance [s : Nonempty α] : Nonempty (Promise α) :=
-  Nonempty.intro { prom := Classical.choice PromisePointed.property, h := s }
+instance [Nonempty α] : Nonempty (Promise α) :=
+  (PromiseImpl α).2.1 inferInstance
 
 /-- Creates a new `Promise`. -/
 @[extern "lean_io_promise_new"]
@@ -47,12 +43,15 @@ Only the first call to this function has an effect.
 @[extern "lean_io_promise_resolve"]
 opaque Promise.resolve (value : α) (promise : @& Promise α) : BaseIO Unit
 
+private unsafe def Promise.resultImpl (promise : Promise α) : Task α :=
+  unsafeCast promise
+
 /--
 The result task of a `Promise`.
 
 The task blocks until `Promise.resolve` is called.
 -/
-@[extern "lean_io_promise_result"]
+@[implemented_by Promise.resultImpl]
 opaque Promise.result (promise : Promise α) : Task α :=
-  have : Nonempty α := promise.h
+  have : Nonempty α := (PromiseImpl α).2.2 ⟨promise⟩
   Classical.choice inferInstance

src/Init/Tactics.lean

@@ -207,28 +207,6 @@ the first matching constructor, or else fails.
 -/
 syntax (name := constructor) "constructor" : tactic
 
-/--
-Applies the second constructor when
-the goal is an inductive type with exactly two constructors, or fails otherwise.
-```
-example : True ∨ False := by
-  left
-  trivial
-```
--/
-syntax (name := left) "left" : tactic
-
-/--
-Applies the second constructor when
-the goal is an inductive type with exactly two constructors, or fails otherwise.
-```
-example {p q : Prop} (h : q) : p ∨ q := by
-  right
-  exact h
-```
--/
-syntax (name := right) "right" : tactic
-
 /--
 * `case tag => tac` focuses on the goal with case name `tag` and solves it using `tac`,
   or else fails.
@@ -345,14 +323,9 @@ syntax (name := eqRefl) "eq_refl" : tactic
 `rfl` tries to close the current goal using reflexivity.
 This is supposed to be an extensible tactic and users can add their own support
 for new reflexive relations.
-
-Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different
-reflexivity theorems (e.g., `Iff.rfl`).
 -/
 macro "rfl" : tactic => `(tactic| eq_refl)
 
-macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
-
 /--
 `rfl'` is similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions,
 theorems included (relevant for declarations defined by well-founded recursion).
@@ -459,17 +432,13 @@ syntax (name := rewriteSeq) "rewrite" (config)? rwRuleSeq (location)? : tactic
 /--
 `rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 -/
-macro (name := rwSeq) "rw " c:(config)? s:rwRuleSeq l:(location)? : tactic =>
+macro (name := rwSeq) "rw" c:(config)? s:rwRuleSeq l:(location)? : tactic =>
   match s with
   | `(rwRuleSeq| [$rs,*]%$rbrak) =>
     -- We show the `rfl` state on `]`
     `(tactic| (rewrite $(c)? [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl))))
   | _ => Macro.throwUnsupported
 
-/-- `rwa` calls `rw`, then closes any remaining goals using `assumption`. -/
-macro "rwa " rws:rwRuleSeq loc:(location)? : tactic =>
-  `(tactic| (rw $rws:rwRuleSeq $[$loc:location]?; assumption))
-
 /--
 The `injection` tactic is based on the fact that constructors of inductive data
 types are injections.
@@ -847,69 +816,6 @@ while `congr 2` produces the intended `⊢ x + y = y + x`.
 -/
 syntax (name := congr) "congr" (ppSpace num)? : tactic
 
-
-/--
-In tactic mode, `if h : t then tac1 else tac2` can be used as alternative syntax for:
-```
-by_cases h : t
-· tac1
-· tac2
-```
-It performs case distinction on `h : t` or `h : ¬t` and `tac1` and `tac2` are the subproofs.
-
-You can use `?_` or `_` for either subproof to delay the goal to after the tactic, but
-if a tactic sequence is provided for `tac1` or `tac2` then it will require the goal to be closed
-by the end of the block.
--/
-syntax (name := tacDepIfThenElse)
-  ppRealGroup(ppRealFill(ppIndent("if " binderIdent " : " term " then") ppSpace matchRhsTacticSeq)
-    ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic
-
-/--
-In tactic mode, `if t then tac1 else tac2` is alternative syntax for:
-```
-by_cases t
-· tac1
-· tac2
-```
-It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous
-hypothesis, and `tac1` and `tac2` are the subproofs. (It doesn't actually use
-nondependent `if`, since this wouldn't add anything to the context and hence would be
-useless for proving theorems. To actually insert an `ite` application use
-`refine if t then ?_ else ?_`.)
--/
-syntax (name := tacIfThenElse)
-  ppRealGroup(ppRealFill(ppIndent("if " term " then") ppSpace matchRhsTacticSeq)
-    ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic
-
-/--
-The tactic `nofun` is shorthand for `exact nofun`: it introduces the assumptions, then performs an
-empty pattern match, closing the goal if the introduced pattern is impossible.
--/
-macro "nofun" : tactic => `(tactic| exact nofun)
-
-/--
-The tactic `nomatch h` is shorthand for `exact nomatch h`.
--/
-macro "nomatch " es:term,+ : tactic =>
-  `(tactic| exact nomatch $es:term,*)
-
-/--
-`repeat' tac` runs `tac` on all of the goals to produce a new list of goals,
-then runs `tac` again on all of those goals, and repeats until `tac` fails on all remaining goals.
--/
-syntax (name := repeat') "repeat' " tacticSeq : tactic
-
-/--
-`repeat1' tac` applies `tac` to main goal at least once. If the application succeeds,
-the tactic is applied recursively to the generated subgoals until it eventually fails.
--/
-syntax (name := repeat1') "repeat1' " tacticSeq : tactic
-
-/-- `and_intros` applies `And.intro` until it does not make progress. -/
-syntax "and_intros" : tactic
-macro_rules | `(tactic| and_intros) => `(tactic| repeat' refine And.intro ?_ ?_)
-
 end Tactic
 
 namespace Attr

src/Init/TacticsExtra.lean

@@ -1,66 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Mario Carneiro
--/
-prelude
-import Init.Tactics
-import Init.NotationExtra
-
-/-!
-Extra tactics and implementation for some tactics defined at `Init/Tactic.lean`
--/
-namespace Lean.Parser.Tactic
-
-private def expandIfThenElse
-    (ifTk thenTk elseTk pos neg : Syntax)
-    (mkIf : Term → Term → MacroM Term) : MacroM (TSyntax `tactic) := do
-  let mkCase tk holeOrTacticSeq mkName : MacroM (Term × Array (TSyntax `tactic)) := do
-    if holeOrTacticSeq.isOfKind `Lean.Parser.Term.syntheticHole then
-      pure (⟨holeOrTacticSeq⟩, #[])
-    else if holeOrTacticSeq.isOfKind `Lean.Parser.Term.hole then
-      pure (← mkName, #[])
-    else
-      let hole ← withFreshMacroScope mkName
-      let holeId := hole.raw[1]
-      let case ← (open TSyntax.Compat in `(tactic|
-          case $holeId:ident =>%$tk
-            -- annotate `then/else` with state after `case`
-            with_annotate_state $tk skip
-            $holeOrTacticSeq))
-      pure (hole, #[case])
-  let (posHole, posCase) ← mkCase thenTk pos `(?pos)
-  let (negHole, negCase) ← mkCase elseTk neg `(?neg)
-  `(tactic| (open Classical in refine%$ifTk $(← mkIf posHole negHole); $[$(posCase ++ negCase)]*))
-
-macro_rules
-  | `(tactic| if%$tk $h : $c then%$ttk $pos else%$etk $neg) =>
-    expandIfThenElse tk ttk etk pos neg fun pos neg => `(if $h : $c then $pos else $neg)
-
-macro_rules
-  | `(tactic| if%$tk $c then%$ttk $pos else%$etk $neg) =>
-    expandIfThenElse tk ttk etk pos neg fun pos neg => `(if h : $c then $pos else $neg)
-
-/--
-`iterate n tac` runs `tac` exactly `n` times.
-`iterate tac` runs `tac` repeatedly until failure.
-
-`iterate`'s argument is a tactic sequence,
-so multiple tactics can be run using `iterate n (tac₁; tac₂; ⋯)` or
-```lean
-iterate n
-  tac₁
-  tac₂
-  ⋯
-```
--/
-syntax "iterate" (ppSpace num)? ppSpace tacticSeq : tactic
-macro_rules
-  | `(tactic| iterate $seq:tacticSeq) =>
-    `(tactic| try ($seq:tacticSeq); iterate $seq:tacticSeq)
-  | `(tactic| iterate $n $seq:tacticSeq) =>
-    match n.1.toNat with
-    | 0 => `(tactic| skip)
-    | n+1 => `(tactic| ($seq:tacticSeq); iterate $(quote n) $seq:tacticSeq)
-
-end Lean.Parser.Tactic

src/Lean/Data/Position.lean

@@ -84,26 +84,6 @@ partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
       -- Can also happen with EOF errors, which are not strictly inside the file.
       ⟨lines.back, (pos - ps.back).byteIdx⟩
 
-/-- Convert a `Lean.Position` to a `String.Pos`. -/
-def ofPosition (text : FileMap) (pos : Position) : String.Pos :=
-  let colPos :=
-    if h : pos.line - 1 < text.positions.size then
-      text.positions.get ⟨pos.line - 1, h⟩
-    else if text.positions.isEmpty then
-      0
-    else
-      text.positions.back
-  String.Iterator.nextn ⟨text.source, colPos⟩ pos.column |>.pos
-
-/--
-Returns the position of the start of (1-based) line `line`.
-This gives the stame result as `map.ofPosition ⟨line, 0⟩`, but is more efficient.
--/
-def lineStart (map : FileMap) (line : Nat) : String.Pos :=
-  if h : line - 1 < map.positions.size then
-    map.positions.get ⟨line - 1, h⟩
-  else map.positions.back?.getD 0
-
 end FileMap
 end Lean
 

src/Lean/Elab/BuiltinCommand.lean

@@ -722,8 +722,6 @@ opaque elabEval : CommandElab
   match stx with
   | `($doc:docComment add_decl_doc $id) =>
     let declName ← resolveGlobalConstNoOverloadWithInfo id
-    unless ((← getEnv).getModuleIdxFor? declName).isNone do
-      throwError "invalid 'add_decl_doc', declaration is in an imported module"
     if let .none ← findDeclarationRangesCore? declName then
       -- this is only relevant for declarations added without a declaration range
       -- in particular `Quot.mk` et al which are added by `init_quot`

src/Lean/Elab/BuiltinNotation.lean

@@ -1,14 +1,12 @@
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Gabriel Ebner
+Authors: Leonardo de Moura
 -/
 import Lean.Compiler.BorrowedAnnotation
 import Lean.Meta.KAbstract
-import Lean.Meta.Closure
 import Lean.Meta.MatchUtil
 import Lean.Elab.SyntheticMVars
-import Lean.Compiler.ImplementedByAttr
 
 namespace Lean.Elab.Term
 open Meta
@@ -21,20 +19,6 @@ open Meta
     throwError "invalid coercion notation, expected type is not known"
   ensureHasType expectedType? e
 
-@[builtin_term_elab coeFunNotation] def elabCoeFunNotation : TermElab := fun stx _ => do
-  let x ← elabTerm stx[1] none
-  if let some ty ← coerceToFunction? x then
-    return ty
-  else
-    throwError "cannot coerce to function{indentExpr x}"
-
-@[builtin_term_elab coeSortNotation] def elabCoeSortNotation : TermElab := fun stx _ => do
-  let x ← elabTerm stx[1] none
-  if let some ty ← coerceToSort? x then
-    return ty
-  else
-    throwError "cannot coerce to sort{indentExpr x}"
-
 @[builtin_term_elab anonymousCtor] def elabAnonymousCtor : TermElab := fun stx expectedType? =>
   match stx with
   | `(⟨$args,*⟩) => do
@@ -427,33 +411,4 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
   let e ← elabTerm stx[1] expectedType?
   return DiscrTree.mkNoindexAnnotation e
 
--- TODO: investigate whether we need this function
-private def mkAuxNameForElabUnsafe (hint : Name) : TermElabM Name :=
-  withFreshMacroScope do
-    let name := (← getDeclName?).getD Name.anonymous ++ hint
-    return addMacroScope (← getMainModule) name (← getCurrMacroScope)
-
-@[builtin_term_elab «unsafe»]
-def elabUnsafe : TermElab := fun stx expectedType? =>
-  match stx with
-  | `(unsafe $t) => do
-    let t ← elabTermAndSynthesize t expectedType?
-    if (← logUnassignedUsingErrorInfos (← getMVars t)) then
-      throwAbortTerm
-    let t ← mkAuxDefinitionFor (← mkAuxName `unsafe) t
-    let .const unsafeFn unsafeLvls .. := t.getAppFn | unreachable!
-    let .defnInfo unsafeDefn ← getConstInfo unsafeFn | unreachable!
-    let implName ← mkAuxNameForElabUnsafe `impl
-    addDecl <| Declaration.defnDecl {
-      name        := implName
-      type        := unsafeDefn.type
-      levelParams := unsafeDefn.levelParams
-      value       := (← mkOfNonempty unsafeDefn.type)
-      hints       := .opaque
-      safety      := .safe
-    }
-    setImplementedBy implName unsafeFn
-    return mkAppN (Lean.mkConst implName unsafeLvls) t.getAppArgs
-  | _ => throwUnsupportedSyntax
-
 end Lean.Elab.Term

src/Lean/Elab/Command.lean

@@ -1,11 +1,10 @@
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Gabriel Ebner
+Authors: Leonardo de Moura
 -/
 import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
-import Lean.Elab.SetOption
 
 namespace Lean.Elab.Command
 
@@ -504,49 +503,6 @@ def expandDeclId (declId : Syntax) (modifiers : Modifiers) : CommandElabM Expand
 
 end Elab.Command
 
-open Elab Command MonadRecDepth
-
-/--
-Lifts an action in `CommandElabM` into `CoreM`, updating the traces and the environment.
-
-Commands that modify the processing of subsequent commands,
-such as `open` and `namespace` commands,
-only have an effect for the remainder of the `CommandElabM` computation passed here,
-and do not affect subsequent commands.
--/
-def liftCommandElabM (cmd : CommandElabM α) : CoreM α := do
-  let (a, commandState) ←
-    cmd.run {
-      fileName := ← getFileName
-      fileMap := ← getFileMap
-      ref := ← getRef
-      tacticCache? := none
-    } |>.run {
-      env := ← getEnv
-      maxRecDepth := ← getMaxRecDepth
-      scopes := [{ header := "", opts := ← getOptions }]
-    }
-  modify fun coreState => { coreState with
-    traceState.traces := coreState.traceState.traces ++ commandState.traceState.traces
-    env := commandState.env
-  }
-  if let some err := commandState.messages.msgs.toArray.find? (·.severity matches .error) then
-    throwError err.data
-  pure a
-
-/--
-Given a command elaborator `cmd`, returns a new command elaborator that
-first evaluates any local `set_option ... in ...` clauses and then invokes `cmd` on what remains.
--/
-partial def withSetOptionIn (cmd : CommandElab) : CommandElab := fun stx => do
-  if stx.getKind == ``Lean.Parser.Command.in &&
-     stx[0].getKind == ``Lean.Parser.Command.set_option then
-      let opts ← Elab.elabSetOption stx[0][1] stx[0][2]
-      Command.withScope (fun scope => { scope with opts }) do
-        withSetOptionIn cmd stx[1]
-  else
-    cmd stx
-
 export Elab.Command (Linter addLinter)
 
 end Lean

src/Lean/Elab/Inductive.lean

@@ -524,14 +524,14 @@ private def updateResultingUniverse (views : Array InductiveView) (numParams : N
 register_builtin_option bootstrap.inductiveCheckResultingUniverse : Bool := {
     defValue := true,
     group    := "bootstrap",
-    descr    := "by default the `inductive`/`structure` commands report an error if the resulting universe is not zero, but may be zero for some universe parameters. Reason: unless this type is a subsingleton, it is hardly what the user wants since it can only eliminate into `Prop`. In the `Init` package, we define subsingletons, and we use this option to disable the check. This option may be deleted in the future after we improve the validator"
+    descr    := "by default the `inductive/structure commands report an error if the resulting universe is not zero, but may be zero for some universe parameters. Reason: unless this type is a subsingleton, it is hardly what the user wants since it can only eliminate into `Prop`. In the `Init` package, we define subsingletons, and we use this option to disable the check. This option may be deleted in the future after we improve the validator"
 }
 
 def checkResultingUniverse (u : Level) : TermElabM Unit := do
   if bootstrap.inductiveCheckResultingUniverse.get (← getOptions) then
     let u ← instantiateLevelMVars u
     if !u.isZero && !u.isNeverZero then
-      throwError "invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'){indentD u}"
+      throwError "invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'{indentD u}"
 
 private def checkResultingUniverses (views : Array InductiveView) (numParams : Nat) (indTypes : List InductiveType) : TermElabM Unit := do
   let u := (← instantiateLevelMVars (← getResultingUniverse indTypes)).normalize

src/Lean/Elab/Match.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Mario Carneiro
+Authors: Leonardo de Moura
 -/
 import Lean.Util.ForEachExprWhere
 import Lean.Meta.Match.Match
@@ -1236,46 +1236,17 @@ where
 builtin_initialize
   registerTraceClass `Elab.match
 
--- leading_parser:leadPrec "nomatch " >> sepBy1 termParser ", "
+-- leading_parser:leadPrec "nomatch " >> termParser
 @[builtin_term_elab «nomatch»] def elabNoMatch : TermElab := fun stx expectedType? => do
   match stx with
-  | `(nomatch $discrs,*) =>
-    let discrs := discrs.getElems
-    if (← discrs.allM fun discr => isAtomicDiscr discr.raw) then
+  | `(nomatch $discrExpr) =>
+    if (← isAtomicDiscr discrExpr) then
       let expectedType ← waitExpectedType expectedType?
-      /- Wait for discriminant types. -/
-      for discr in discrs do
-        let d ← elabTerm discr none
-        let dType ← inferType d
-        trace[Elab.match] "discr {d} : {← instantiateMVars dType}"
-        tryPostponeIfMVar dType
-      let discrs := discrs.map fun discr => mkNode ``Lean.Parser.Term.matchDiscr #[mkNullNode, discr.raw]
-      elabMatchAux none discrs #[] mkNullNode expectedType
+      let discr := mkNode ``Lean.Parser.Term.matchDiscr #[mkNullNode, discrExpr]
+      elabMatchAux none #[discr] #[] mkNullNode expectedType
     else
-      let rec loop (discrs : List Term) (discrsNew : Array Syntax) : TermElabM Term := do
-        match discrs with
-        | [] =>
-          return ⟨stx.setArg 1 (Syntax.mkSep discrsNew (mkAtomFrom stx ", "))⟩
-        | discr :: discrs =>
-          if (← isAtomicDiscr discr) then
-            loop discrs (discrsNew.push discr)
-          else
-            withFreshMacroScope do
-              let discrNew ← `(?x)
-              let r ← loop discrs (discrsNew.push discrNew)
-              `(let_mvar% ?x := $discr; $r)
-      let stxNew ← loop discrs.toList #[]
+      let stxNew ← `(let_mvar% ?x := $discrExpr; nomatch ?x)
       withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
   | _ => throwUnsupportedSyntax
 
-@[builtin_term_elab «nofun»] def elabNoFun : TermElab := fun stx expectedType? => do
-  match stx with
-  | `($tk:nofun) =>
-    let expectedType ← waitExpectedType expectedType?
-    let binders ← forallTelescopeReducing expectedType fun args _ =>
-      args.mapM fun _ => withFreshMacroScope do `(a)
-    let stxNew ← `(fun%$tk $binders* => nomatch%$tk $binders,*)
-    withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
-  | _ => throwUnsupportedSyntax
-
 end Lean.Elab.Term

src/Lean/Elab/Tactic.lean

@@ -23,7 +23,3 @@ import Lean.Elab.Tactic.Unfold
 import Lean.Elab.Tactic.Cache
 import Lean.Elab.Tactic.Calc
 import Lean.Elab.Tactic.Congr
-import Lean.Elab.Tactic.Guard
-import Lean.Elab.Tactic.RCases
-import Lean.Elab.Tactic.Repeat
-import Lean.Elab.Tactic.Change

src/Lean/Elab/Tactic/Basic.lean

@@ -335,15 +335,6 @@ def evalTacticAt (tac : Syntax) (mvarId : MVarId) : TacticM (List MVarId) := do
   finally
     setGoals gs
 
-/--
-Like `evalTacticAt`, but without restoring the goal list or pruning solved goals.
-Useful when these tasks are already being done in an outer loop.
--/
-def evalTacticAtRaw (tac : Syntax) (mvarId : MVarId) : TacticM (List MVarId) := do
-  setGoals [mvarId]
-  evalTactic tac
-  getGoals
-
 def ensureHasNoMVars (e : Expr) : TacticM Unit := do
   let e ← instantiateMVars e
   let pendingMVars ← getMVars e

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Assumption
 import Lean.Meta.Tactic.Contradiction
 import Lean.Meta.Tactic.Refl
@@ -324,12 +323,6 @@ def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) :
 @[builtin_tactic Lean.Parser.Tactic.substVars] def evalSubstVars : Tactic := fun _ =>
   liftMetaTactic fun mvarId => return [← substVars mvarId]
 
-/--
-`subst_eq` repeatedly substitutes according to the equality proof hypotheses in the context,
-replacing the left side of the equality with the right, until no more progress can be made.
--/
-elab "subst_eqs" : tactic => Elab.Tactic.liftMetaTactic1 (·.substEqs)
-
 /--
   Searches for a metavariable `g` s.t. `tag` is its exact name.
   If none then searches for a metavariable `g` s.t. `tag` is a suffix of its name.
@@ -475,10 +468,4 @@ where
   | none    => throwIllFormedSyntax
   | some ms => IO.sleep ms.toUInt32
 
-@[builtin_tactic left] def evalLeft : Tactic := fun _stx => do
-  liftMetaTactic (fun g => g.nthConstructor `left 0 (some 2))
-
-@[builtin_tactic right] def evalRight : Tactic := fun _stx => do
-  liftMetaTactic (fun g => g.nthConstructor `right 1 (some 2))
-
 end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Change.lean

@@ -1,51 +0,0 @@
-/-
-Copyright (c) 2023 Kyle Miller. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kyle Miller
--/
-import Lean.Meta.Tactic.Replace
-import Lean.Elab.Tactic.Location
-
-namespace Lean.Elab.Tactic
-open Meta
-/-!
-# Implementation of the `change` tactic
--/
-
-/-- `change` can be used to replace the main goal or its hypotheses with
-different, yet definitionally equal, goal or hypotheses.
-
-For example, if `n : Nat` and the current goal is `⊢ n + 2 = 2`, then
-```lean
-change _ + 1 = _
-```
-changes the goal to `⊢ n + 1 + 1 = 2`.
-
-The tactic also applies to hypotheses. If `h : n + 2 = 2` and `h' : n + 3 = 4`
-are hypotheses, then
-```lean
-change _ + 1 = _ at h h'
-```
-changes their types to be `h : n + 1 + 1 = 2` and `h' : n + 2 + 1 = 4`.
-
-Change is like `refine` in that every placeholder needs to be solved for by unification,
-but using named placeholders or `?_` results in `change` to creating new goals.
-
-The tactic `show e` is interchangeable with `change e`, where the pattern `e` is applied to
-the main goal. -/
-@[builtin_tactic change] elab_rules : tactic
-  | `(tactic| change $newType:term $[$loc:location]?) => do
-    withLocation (expandOptLocation (Lean.mkOptionalNode loc))
-      (atLocal := fun h => do
-        let hTy ← h.getType
-        -- This is a hack to get the new type to elaborate in the same sort of way that
-        -- it would for a `show` expression for the goal.
-        let mvar ← mkFreshExprMVar none
-        let (_, mvars) ← elabTermWithHoles
-                          (← `(term | show $newType from $(← Term.exprToSyntax mvar))) hTy `change
-        liftMetaTactic fun mvarId => do
-          return (← mvarId.changeLocalDecl h (← inferType mvar)) :: mvars)
-      (atTarget := evalTactic <| ← `(tactic| refine_lift show $newType from ?_))
-      (failed := fun _ => throwError "change tactic failed")
-
-end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Guard.lean

@@ -1,158 +0,0 @@
-/-
-Copyright (c) 2021 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Leonardo de Moura
--/
-import Lean.Elab.Command
-import Lean.Elab.Tactic.Conv.Basic
-import Lean.Meta.Basic
-import Lean.Meta.Eval
-
-namespace Lean.Elab.Tactic.GuardExpr
-open Meta
-
-/--
-The various `guard_*` tactics have similar matching specifiers for how equal expressions
-have to be to pass the tactic.
-This inductive gives the different specifiers that can be selected.
--/
-inductive MatchKind
-/-- A syntactic match means that the `Expr`s are `==` after stripping `MData` -/
-| syntactic
-/-- A defeq match `isDefEqGuarded` returns true. (Note that unification is allowed here.) -/
-| defEq (red : TransparencyMode := .reducible)
-/-- An alpha-eq match means that `Expr.eqv` returns true. -/
-| alphaEq
-
-open Lean.Parser Lean.Parser.Tactic Lean.Parser.Command
-
-/-- Converts a `colon` syntax into a `MatchKind` -/
-def colon.toMatchKind : TSyntax ``colon → Option MatchKind
-  | `(colon| :) => some .defEq
-  | `(colon| :~) => some (.defEq .default)
-  | `(colon| :ₛ) => some .syntactic
-  | `(colon| :ₐ) => some .alphaEq
-  | _ => none
-
-/-- Converts a `colonEq` syntax into a `MatchKind` -/
-def colonEq.toMatchKind : TSyntax ``colonEq → Option MatchKind
-  | `(colonEq| :=) => some .defEq
-  | `(colonEq| :=~) => some (.defEq .default)
-  | `(colonEq| :=ₛ) => some .syntactic
-  | `(colonEq| :=ₐ) => some .alphaEq
-  | _ => none
-
-/-- Converts a `equal` syntax into a `MatchKind` -/
-def equal.toMatchKind : TSyntax ``equal → Option MatchKind
-  | `(equal| =) => some .defEq
-  | `(equal| =~) => some (.defEq .default)
-  | `(equal| =ₛ) => some .syntactic
-  | `(equal| =ₐ) => some .alphaEq
-  | _ => none
-
-/-- Applies the selected matching rule to two expressions. -/
-def MatchKind.isEq (a b : Expr) : MatchKind → MetaM Bool
-  | .syntactic => return a.consumeMData == b.consumeMData
-  | .alphaEq => return a.eqv b
-  | .defEq red => withoutModifyingState <| withTransparency red <| Lean.Meta.isDefEqGuarded a b
-
-
-/-- Elaborate `a` and `b` and then do the given equality test `mk`. We make sure to unify
-the types of `a` and `b` after elaboration so that when synthesizing pending metavariables
-we don't get the wrong instances due to default instances (for example, for nat literals). -/
-def elabAndEvalMatchKind (mk : MatchKind) (a b : Term) : TermElabM Bool :=
-  Term.withoutErrToSorry do
-    let a ← Term.elabTerm a none
-    let b ← Term.elabTerm b none
-    -- Unify types before synthesizing pending metavariables:
-    _ ← isDefEqGuarded (← inferType a) (← inferType b)
-    Term.synthesizeSyntheticMVarsNoPostponing
-    mk.isEq (← instantiateMVars a) (← instantiateMVars b)
-
-@[builtin_tactic guardExpr]
-def evalGuardExpr : Tactic := fun
-  | `(tactic| guard_expr $r $eq:equal $p)
-  | `(conv| guard_expr $r $eq:equal $p) => withMainContext do
-    let some mk := equal.toMatchKind eq | throwUnsupportedSyntax
-    let res ← elabAndEvalMatchKind mk r p
-    -- Note: `{eq}` itself prints a space before the relation.
-    unless res do throwError "failed: {r}{eq} {p} is not true"
-  | _ => throwUnsupportedSyntax
-
--- TODO: This is workaround. We currently allow two occurrences of `builtin_tactic`.
-@[builtin_tactic guardExprConv]
-def evalGuardExprConv : Tactic := evalGuardExpr
-
-@[builtin_tactic guardTarget]
-def evalGuardTarget : Tactic :=
-  let go eq r getTgt := withMainContext do
-    let t ← getTgt >>= instantiateMVars
-    let r ← elabTerm r (← inferType t)
-    let some mk := equal.toMatchKind eq | throwUnsupportedSyntax
-    unless ← mk.isEq r t do
-      throwError "target of main goal is{indentExpr t}\nnot{indentExpr r}"
-  fun
-  | `(tactic| guard_target $eq $r) => go eq r getMainTarget
-  | `(conv| guard_target $eq $r) => go eq r Conv.getLhs
-  | _ => throwUnsupportedSyntax
-
--- See comment above
-@[builtin_tactic guardTargetConv]
-def evalGuardTargetConv : Tactic := evalGuardTarget
-
-@[builtin_tactic guardHyp]
-def evalGuardHyp : Tactic := fun
-  | `(tactic| guard_hyp $h $[$c $ty]? $[$eq $val]?)
-  | `(conv| guard_hyp $h $[$c $ty]? $[$eq $val]?) => withMainContext do
-    let fvarid ← getFVarId h
-    let lDecl ←
-      match (← getLCtx).find? fvarid with
-      | none => throwError m!"hypothesis {h} not found"
-      | some lDecl => pure lDecl
-    if let (some c, some p) := (c, ty) then
-      let some mk := colon.toMatchKind c | throwUnsupportedSyntax
-      let e ← elabTerm p none
-      let hty ← instantiateMVars lDecl.type
-      unless ← mk.isEq e hty do
-        throwError m!"hypothesis {h} has type{indentExpr hty}\nnot{indentExpr e}"
-    match lDecl.value?, val with
-    | none, some _        => throwError m!"{h} is not a let binding"
-    | some _, none        => throwError m!"{h} is a let binding"
-    | some hval, some val =>
-      let some mk := eq.bind colonEq.toMatchKind | throwUnsupportedSyntax
-      let e ← elabTerm val lDecl.type
-      let hval ← instantiateMVars hval
-      unless ← mk.isEq e hval do
-        throwError m!"hypothesis {h} has value{indentExpr hval}\nnot{indentExpr e}"
-    | none, none          => pure ()
-  | _ => throwUnsupportedSyntax
-
-@[builtin_tactic guardHypConv]
-def evalGuardHypConv : Tactic := evalGuardHyp
-
-@[builtin_command_elab guardExprCmd]
-def evalGuardExprCmd : Lean.Elab.Command.CommandElab
-  | `(command| #guard_expr $r $eq:equal $p) =>
-    Lean.Elab.Command.runTermElabM fun _ => do
-      let some mk := equal.toMatchKind eq | throwUnsupportedSyntax
-      let res ← elabAndEvalMatchKind mk r p
-      -- Note: `{eq}` itself prints a space before the relation.
-      unless res do throwError "failed: {r}{eq} {p} is not true"
-  | _ => throwUnsupportedSyntax
-
-@[builtin_command_elab guardCmd]
-def evalGuardCmd : Lean.Elab.Command.CommandElab
-  | `(command| #guard $e:term) => Lean.Elab.Command.liftTermElabM do
-    let e ← Term.elabTermEnsuringType e (mkConst ``Bool)
-    Term.synthesizeSyntheticMVarsNoPostponing
-    let e ← instantiateMVars e
-    let mvars ← getMVars e
-    if mvars.isEmpty then
-      let v ← unsafe evalExpr Bool (mkConst ``Bool) e
-      unless v do
-        throwError "expression{indentExpr e}\ndid not evaluate to `true`"
-    else
-      _ ← Term.logUnassignedUsingErrorInfos mvars
-  | _ => throwUnsupportedSyntax
-
-end Lean.Elab.Tactic.GuardExpr

src/Lean/Elab/Tactic/RCases.lean

@@ -1,580 +0,0 @@
-/-
-Copyright (c) 2017 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Jacob von Raumer
--/
-import Lean.Elab.Tactic.Induction
-
-namespace Lean.Elab.Tactic.RCases
-open Meta Parser Tactic
-
-/--
-Enables the 'unused rcases pattern' linter. This will warn when a pattern is ignored by
-`rcases`, `rintro`, `ext` and similar tactics.
--/
-register_option linter.unusedRCasesPattern : Bool := {
-  defValue := true
-  descr := "enable the 'unused rcases pattern' linter"
-}
-
-instance : Coe Ident (TSyntax `rcasesPat) where
-  coe stx := Unhygienic.run `(rcasesPat| $stx:ident)
-instance : Coe (TSyntax `rcasesPat) (TSyntax ``rcasesPatMed) where
-  coe stx := Unhygienic.run `(rcasesPatMed| $stx:rcasesPat)
-instance : Coe (TSyntax ``rcasesPatMed) (TSyntax ``rcasesPatLo) where
-  coe stx := Unhygienic.run `(rcasesPatLo| $stx:rcasesPatMed)
-instance : Coe (TSyntax `rcasesPat) (TSyntax `rintroPat) where
-  coe stx := Unhygienic.run `(rintroPat| $stx:rcasesPat)
-
-/-- A list, with a disjunctive meaning (like a list of inductive constructors, or subgoals) -/
-local notation "ListΣ" => List
-
-/-- A list, with a conjunctive meaning (like a list of constructor arguments, or hypotheses) -/
-local notation "ListΠ" => List
-
-/--
-An `rcases` pattern can be one of the following, in a nested combination:
-
-* A name like `foo`
-* The special keyword `rfl` (for pattern matching on equality using `subst`)
-* A hyphen `-`, which clears the active hypothesis and any dependents.
-* A type ascription like `pat : ty` (parentheses are optional)
-* A tuple constructor like `⟨p1, p2, p3⟩`
-* An alternation / variant pattern `p1 | p2 | p3`
-
-Parentheses can be used for grouping; alternation is higher precedence than type ascription, so
-`p1 | p2 | p3 : ty` means `(p1 | p2 | p3) : ty`.
-
-N-ary alternations are treated as a group, so `p1 | p2 | p3` is not the same as `p1 | (p2 | p3)`,
-and similarly for tuples. However, note that an n-ary alternation or tuple can match an n-ary
-conjunction or disjunction, because if the number of patterns exceeds the number of constructors in
-the type being destructed, the extra patterns will match on the last element, meaning that
-`p1 | p2 | p3` will act like `p1 | (p2 | p3)` when matching `a1 ∨ a2 ∨ a3`. If matching against a
-type with 3 constructors,  `p1 | (p2 | p3)` will act like `p1 | (p2 | p3) | _` instead.
--/
-inductive RCasesPatt : Type
-  /-- A parenthesized expression, used for hovers -/
-  | paren (ref : Syntax) : RCasesPatt → RCasesPatt
-  /-- A named pattern like `foo` -/
-  | one (ref : Syntax) : Name → RCasesPatt
-  /-- A hyphen `-`, which clears the active hypothesis and any dependents. -/
-  | clear (ref : Syntax) : RCasesPatt
-  /-- An explicit pattern `@pat`. -/
-  | explicit (ref : Syntax) : RCasesPatt → RCasesPatt
-  /-- A type ascription like `pat : ty` (parentheses are optional) -/
-  | typed (ref : Syntax) : RCasesPatt → Term → RCasesPatt
-  /-- A tuple constructor like `⟨p1, p2, p3⟩` -/
-  | tuple (ref : Syntax) : ListΠ RCasesPatt → RCasesPatt
-  /-- An alternation / variant pattern `p1 | p2 | p3` -/
-  | alts (ref : Syntax) : ListΣ RCasesPatt → RCasesPatt
-  deriving Repr
-
-namespace RCasesPatt
-
-instance : Inhabited RCasesPatt := ⟨RCasesPatt.one Syntax.missing `_⟩
-
-/-- Get the name from a pattern, if provided -/
-partial def name? : RCasesPatt → Option Name
-  | one _ `_    => none
-  | one _ `rfl  => none
-  | one _ n     => n
-  | paren _ p
-  | typed _ p _
-  | alts _ [p]  => p.name?
-  | _           => none
-
-/-- Get the syntax node from which this pattern was parsed. Used for error messages -/
-def ref : RCasesPatt → Syntax
-  | paren ref _
-  | one ref _
-  | clear ref
-  | explicit ref _
-  | typed ref _ _
-  | tuple ref _
-  | alts ref _ => ref
-
-/--
-Interpret an rcases pattern as a tuple, where `p` becomes `⟨p⟩` if `p` is not already a tuple.
--/
-def asTuple : RCasesPatt → Bool × ListΠ RCasesPatt
-  | paren _ p    => p.asTuple
-  | explicit _ p => (true, p.asTuple.2)
-  | tuple _ ps   => (false, ps)
-  | p            => (false, [p])
-
-/--
-Interpret an rcases pattern as an alternation, where non-alternations are treated as one
-alternative.
--/
-def asAlts : RCasesPatt → ListΣ RCasesPatt
-  | paren _ p => p.asAlts
-  | alts _ ps => ps
-  | p         => [p]
-
-/-- Convert a list of patterns to a tuple pattern, but mapping `[p]` to `p` instead of `⟨p⟩`. -/
-def typed? (ref : Syntax) : RCasesPatt → Option Term → RCasesPatt
-  | p, none => p
-  | p, some ty => typed ref p ty
-
-/-- Convert a list of patterns to a tuple pattern, but mapping `[p]` to `p` instead of `⟨p⟩`. -/
-def tuple' : ListΠ RCasesPatt → RCasesPatt
-  | [p] => p
-  | ps  => tuple (ps.head?.map (·.ref) |>.getD .missing) ps
-
-/--
-Convert a list of patterns to an alternation pattern, but mapping `[p]` to `p` instead of
-a unary alternation `|p`.
--/
-def alts' (ref : Syntax) : ListΣ RCasesPatt → RCasesPatt
-  | [p] => p
-  | ps  => alts ref ps
-
-/--
-This function is used for producing rcases patterns based on a case tree. Suppose that we have
-a list of patterns `ps` that will match correctly against the branches of the case tree for one
-constructor. This function will merge tuples at the end of the list, so that `[a, b, ⟨c, d⟩]`
-becomes `⟨a, b, c, d⟩` instead of `⟨a, b, ⟨c, d⟩⟩`.
-
-We must be careful to turn `[a, ⟨⟩]` into `⟨a, ⟨⟩⟩` instead of `⟨a⟩` (which will not perform the
-nested match).
--/
-def tuple₁Core : ListΠ RCasesPatt → ListΠ RCasesPatt
-  | []         => []
-  | [tuple ref []] => [tuple ref []]
-  | [tuple _ ps] => ps
-  | p :: ps    => p :: tuple₁Core ps
-
-/--
-This function is used for producing rcases patterns based on a case tree. This is like
-`tuple₁Core` but it produces a pattern instead of a tuple pattern list, converting `[n]` to `n`
-instead of `⟨n⟩` and `[]` to `_`, and otherwise just converting `[a, b, c]` to `⟨a, b, c⟩`.
--/
-def tuple₁ : ListΠ RCasesPatt → RCasesPatt
-  | []      => default
-  | [one ref n] => one ref n
-  | ps      => tuple ps.head!.ref $ tuple₁Core ps
-
-/--
-This function is used for producing rcases patterns based on a case tree. Here we are given
-the list of patterns to apply to each argument of each constructor after the main case, and must
-produce a list of alternatives with the same effect. This function calls `tuple₁` to make the
-individual alternatives, and handles merging `[a, b, c | d]` to `a | b | c | d` instead of
-`a | b | (c | d)`.
--/
-def alts₁Core : ListΣ (ListΠ RCasesPatt) → ListΣ RCasesPatt
-  | []          => []
-  | [[alts _ ps]] => ps
-  | p :: ps     => tuple₁ p :: alts₁Core ps
-
-/--
-This function is used for producing rcases patterns based on a case tree. This is like
-`alts₁Core`, but it produces a cases pattern directly instead of a list of alternatives. We
-specially translate the empty alternation to `⟨⟩`, and translate `|(a | b)` to `⟨a | b⟩` (because we
-don't have any syntax for unary alternation). Otherwise we can use the regular merging of
-alternations at the last argument so that `a | b | (c | d)` becomes `a | b | c | d`.
--/
-def alts₁ (ref : Syntax) : ListΣ (ListΠ RCasesPatt) → RCasesPatt
-  | [[]]        => tuple .missing []
-  | [[alts ref ps]] => tuple ref ps
-  | ps          => alts' ref $ alts₁Core ps
-
-open MessageData in
-partial instance : ToMessageData RCasesPatt := ⟨fmt 0⟩ where
-  /-- parenthesize the message if the precedence is above `tgt` -/
-  parenAbove (tgt p : Nat) (m : MessageData) : MessageData :=
-    if tgt < p then m.paren else m
-  /-- format an `RCasesPatt` with the given precedence: 0 = lo, 1 = med, 2 = hi -/
-  fmt : Nat → RCasesPatt → MessageData
-  | p, paren _ pat => fmt p pat
-  | _, one _ n => n
-  | _, clear _ => "-"
-  | _, explicit _ pat => m!"@{fmt 2 pat}"
-  | p, typed _ pat ty => parenAbove 0 p m!"{fmt 1 pat}: {ty}"
-  | _, tuple _ pats => bracket "⟨" (joinSep (pats.map (fmt 0)) ("," ++ Format.line)) "⟩"
-  | p, alts _ pats => parenAbove 1 p (joinSep (pats.map (fmt 2)) " | ")
-
-end RCasesPatt
-
-/--
-Takes the number of fields of a single constructor and patterns to match its fields against
-(not necessarily the same number). The returned lists each contain one element per field of the
-constructor. The `name` is the name which will be used in the top-level `cases` tactic, and the
-`rcases_patt` is the pattern which the field will be matched against by subsequent `cases`
-tactics.
--/
-def processConstructor (ref : Syntax) (info : Array ParamInfo)
-    (explicit : Bool) (idx : Nat) (ps : ListΠ RCasesPatt) : ListΠ Name × ListΠ RCasesPatt :=
-  if _ : idx < info.size then
-    if !explicit && info[idx].binderInfo != .default then
-      let (ns, tl) := processConstructor ref info explicit (idx+1) ps
-      (`_ :: ns, default :: tl)
-    else if idx+1 < info.size then
-      let p := ps.headD default
-      let (ns, tl) := processConstructor ref info explicit (idx+1) (ps.tailD [])
-      (p.name?.getD `_ :: ns, p :: tl)
-    else match ps with
-      | []  => ([`_], [default])
-      | [p] => ([p.name?.getD `_], [p])
-      | ps  => ([`_], [(bif explicit then .explicit ref else id) (.tuple ref ps)])
-  else ([], [])
-termination_by info.size - idx
-
-/--
-Takes a list of constructor names, and an (alternation) list of patterns, and matches each
-pattern against its constructor. It returns the list of names that will be passed to `cases`,
-and the list of `(constructor name, patterns)` for each constructor, where `patterns` is the
-(conjunctive) list of patterns to apply to each constructor argument.
--/
-def processConstructors (ref : Syntax) (params : Nat) (altVarNames : Array AltVarNames := #[]) :
-    ListΣ Name → ListΣ RCasesPatt → MetaM (Array AltVarNames × ListΣ (Name × ListΠ RCasesPatt))
-  | [], _ => pure (altVarNames, [])
-  | c :: cs, ps => do
-    let info := (← getFunInfo (← mkConstWithLevelParams c)).paramInfo
-    let p := ps.headD default
-    let t := ps.tailD []
-    let ((explicit, h), t) := match cs, t with
-    | [], _ :: _ => ((false, [RCasesPatt.alts ref ps]), [])
-    | _,  _      => (p.asTuple, t)
-    let (ns, ps) := processConstructor p.ref info explicit params h
-    let (altVarNames, r) ← processConstructors ref params (altVarNames.push ⟨true, ns⟩) cs t
-    pure (altVarNames, (c, ps) :: r)
-
-open Elab Tactic
-
--- TODO(Mario): this belongs in core
-/-- Like `Lean.Meta.subst`, but preserves the `FVarSubst`. -/
-def subst' (goal : MVarId) (hFVarId : FVarId)
-    (fvarSubst : FVarSubst := {}) : MetaM (FVarSubst × MVarId) := do
-  let hLocalDecl ← hFVarId.getDecl
-  let error {α} _ : MetaM α := throwTacticEx `subst goal
-    m!"invalid equality proof, it is not of the form (x = t) or (t = x){indentExpr hLocalDecl.type}"
-  let some (_, lhs, rhs) ← matchEq? hLocalDecl.type | error ()
-  let substReduced (newType : Expr) (symm : Bool) : MetaM (FVarSubst × MVarId) := do
-    let goal ← goal.assert hLocalDecl.userName newType (mkFVar hFVarId)
-    let (hFVarId', goal) ← goal.intro1P
-    let goal ← goal.clear hFVarId
-    substCore goal hFVarId' (symm := symm) (tryToSkip := true) (fvarSubst := fvarSubst)
-  let rhs' ← whnf rhs
-  if rhs'.isFVar then
-    if rhs != rhs' then
-      substReduced (← mkEq lhs rhs') true
-    else
-      substCore goal hFVarId (symm := true) (tryToSkip := true) (fvarSubst := fvarSubst)
-  else
-    let lhs' ← whnf lhs
-    if lhs'.isFVar then
-      if lhs != lhs' then
-        substReduced (← mkEq lhs' rhs) false
-      else
-        substCore goal hFVarId (symm := false) (tryToSkip := true) (fvarSubst := fvarSubst)
-    else error ()
-
-mutual
-
-/--
-This will match a pattern `pat` against a local hypothesis `e`.
-* `g`: The initial subgoal
-* `fs`: A running variable substitution, the result of `cases` operations upstream.
-  The variable `e` must be run through this map before locating it in the context of `g`,
-  and the output variable substitutions will be end extensions of this one.
-* `clears`: The list of variables to clear in all subgoals generated from this point on.
-  We defer clear operations because clearing too early can cause `cases` to fail.
-  The actual clearing happens in `RCases.finish`.
-* `e`: a local hypothesis, the scrutinee to match against.
-* `a`: opaque "user data" which is passed through all the goal calls at the end.
-* `pat`: the pattern to match against
-* `cont`: A continuation. This is called on every goal generated by the result of the pattern
-  match, with updated values for `g` , `fs`, `clears`, and `a`.
--/
-partial def rcasesCore (g : MVarId) (fs : FVarSubst) (clears : Array FVarId) (e : Expr) (a : α)
-    (pat : RCasesPatt) (cont : MVarId → FVarSubst → Array FVarId → α → TermElabM α) :
-    TermElabM α := do
-  let asFVar : Expr → MetaM _
-    | .fvar e => pure e
-    | e => throwError "rcases tactic failed: {e} is not a fvar"
-  withRef pat.ref <| g.withContext do match pat with
-  | .one ref `rfl =>
-    Term.synthesizeSyntheticMVarsNoPostponing
-    -- Note: the mdata prevents the span from getting highlighted like a variable
-    Term.addTermInfo' ref (.mdata {} e)
-    let (fs, g) ← subst' g (← asFVar (fs.apply e)) fs
-    cont g fs clears a
-  | .one ref _ =>
-    if e.isFVar then
-      Term.addLocalVarInfo ref e
-    cont g fs clears a
-  | .clear ref =>
-    Term.addTermInfo' ref (.mdata {} e)
-    cont g fs (if let .fvar e := e then clears.push e else clears) a
-  | .typed ref pat ty =>
-    Term.addTermInfo' ref (.mdata {} e)
-    let expected ← Term.elabType ty
-    let e := fs.apply e
-    let etype ← inferType e
-    unless ← isDefEq etype expected do
-      Term.throwTypeMismatchError "rcases: scrutinee" expected etype e
-    let g ← if let .fvar e := e then g.replaceLocalDeclDefEq e expected else pure g
-    rcasesCore g fs clears e a pat cont
-  | .paren ref p
-  | .alts ref [p] =>
-    Term.addTermInfo' ref (.mdata {} e)
-    rcasesCore g fs clears e a p cont
-  | _ =>
-    Term.addTermInfo' pat.ref (.mdata {} e)
-    let e := fs.apply e
-    let _ ← asFVar e
-    Term.synthesizeSyntheticMVarsNoPostponing
-    let type ← whnfD (← inferType e)
-    let failK {α} _ : TermElabM α :=
-      throwError "rcases tactic failed: {e} : {type} is not an inductive datatype"
-    let (r, subgoals) ← matchConst type.getAppFn failK fun
-      | ConstantInfo.quotInfo info, _ => do
-        unless info.kind matches QuotKind.type do failK ()
-        let pat := pat.asAlts.headD default
-        let (explicit, pat₁) := pat.asTuple
-        let ([x], ps) := processConstructor pat.ref #[{}] explicit 0 pat₁ | unreachable!
-        let (vars, g) ← g.revert (← getFVarsToGeneralize #[e])
-        g.withContext do
-          let elimInfo ← getElimInfo `Quot.ind
-          let res ← ElimApp.mkElimApp elimInfo #[e] (← g.getTag)
-          let elimArgs := res.elimApp.getAppArgs
-          ElimApp.setMotiveArg g elimArgs[elimInfo.motivePos]!.mvarId! #[e.fvarId!]
-          g.assign res.elimApp
-          let #[{ name := n, mvarId := g, .. }] := res.alts | unreachable!
-          let (v, g) ← g.intro x
-          let (varsOut, g) ← g.introNP vars.size
-          let fs' := (vars.zip varsOut).foldl (init := fs) fun fs (v, w) => fs.insert v (mkFVar w)
-          pure ([(n, ps)], #[⟨⟨g, #[mkFVar v], fs'⟩, n⟩])
-      | ConstantInfo.inductInfo info, _ => do
-        let (altVarNames, r) ← processConstructors pat.ref info.numParams #[] info.ctors pat.asAlts
-        (r, ·) <$> g.cases e.fvarId! altVarNames
-      | _, _ => failK ()
-    (·.2) <$> subgoals.foldlM (init := (r, a)) fun (r, a) ⟨goal, ctorName⟩ => do
-      let rec
-      /-- Runs `rcasesContinue` on the first pattern in `r` with a matching `ctorName`.
-      The unprocessed patterns (subsequent to the matching pattern) are returned. -/
-      align : ListΠ (Name × ListΠ RCasesPatt) → TermElabM (ListΠ (Name × ListΠ RCasesPatt) × α)
-      | [] => pure ([], a)
-      | (tgt, ps) :: as => do
-        if tgt == ctorName then
-          let fs := fs.append goal.subst
-          (as, ·) <$> rcasesContinue goal.mvarId fs clears a (ps.zip goal.fields.toList) cont
-        else
-          align as
-      align r
-
-/--
-This will match a list of patterns against a list of hypotheses `e`. The arguments are similar
-to `rcasesCore`, but the patterns and local variables are in `pats`. Because the calls are all
-nested in continuations, later arguments can be matched many times, once per goal produced by
-earlier arguments. For example `⟨a | b, ⟨c, d⟩⟩` performs the `⟨c, d⟩` match twice, once on the
-`a` branch and once on `b`.
--/
-partial def rcasesContinue (g : MVarId) (fs : FVarSubst) (clears : Array FVarId) (a : α)
-  (pats : ListΠ (RCasesPatt × Expr)) (cont : MVarId → FVarSubst → Array FVarId → α → TermElabM α) :
-  TermElabM α :=
-  match pats with
-  | []  => cont g fs clears a
-  | ((pat, e) :: ps) =>
-    rcasesCore g fs clears e a pat fun g fs clears a =>
-      rcasesContinue g fs clears a ps cont
-
-end
-
-/-- Like `tryClearMany`, but also clears dependent hypotheses if possible -/
-def tryClearMany' (goal : MVarId) (fvarIds : Array FVarId) : MetaM MVarId := do
-  let mut toErase := fvarIds
-  for localDecl in (← goal.getDecl).lctx do
-    if ← findLocalDeclDependsOn localDecl toErase.contains then
-      toErase := toErase.push localDecl.fvarId
-  goal.tryClearMany toErase
-
-/--
-The terminating continuation used in `rcasesCore` and `rcasesContinue`. We specialize the type
-`α` to `Array MVarId` to collect the list of goals, and given the list of `clears`, it attempts to
-clear them from the goal and adds the goal to the list.
--/
-def finish (toTag : Array (Ident × FVarId) := #[])
-  (g : MVarId) (fs : FVarSubst) (clears : Array FVarId)
-  (gs : Array MVarId) : TermElabM (Array MVarId) := do
-  let cs : Array Expr := (clears.map fs.get).filter Expr.isFVar
-  let g ← tryClearMany' g (cs.map Expr.fvarId!)
-  g.withContext do
-    for (stx, fvar) in toTag do
-      Term.addLocalVarInfo stx (fs.get fvar)
-  return gs.push g
-
-open Elab
-
-/-- Parses a `Syntax` into the `RCasesPatt` type used by the `RCases` tactic. -/
-partial def RCasesPatt.parse (stx : Syntax) : MetaM RCasesPatt :=
-  match stx with
-  | `(rcasesPatMed| $ps:rcasesPat|*) => return .alts' stx (← ps.getElems.toList.mapM (parse ·.raw))
-  | `(rcasesPatLo| $pat:rcasesPatMed : $t:term) => return .typed stx (← parse pat) t
-  | `(rcasesPatLo| $pat:rcasesPatMed) => parse pat
-  | `(rcasesPat| _) => return .one stx `_
-  | `(rcasesPat| $h:ident) => return .one h h.getId
-  | `(rcasesPat| -) => return .clear stx
-  | `(rcasesPat| @$pat) => return .explicit stx (← parse pat)
-  | `(rcasesPat| ⟨$ps,*⟩) => return .tuple stx (← ps.getElems.toList.mapM (parse ·.raw))
-  | `(rcasesPat| ($pat)) => return .paren stx (← parse pat)
-  | _ => throwUnsupportedSyntax
-
--- extracted from elabCasesTargets
-/-- Generalize all the arguments as specified in `args` to fvars if they aren't already -/
-def generalizeExceptFVar (goal : MVarId) (args : Array GeneralizeArg) :
-    MetaM (Array Expr × Array FVarId × MVarId) := do
-  let argsToGeneralize := args.filter fun arg => !(arg.expr.isFVar && arg.hName?.isNone)
-  let (fvarIdsNew, goal) ← goal.generalize argsToGeneralize
-  let mut result := #[]
-  let mut j := 0
-  for arg in args do
-    if arg.expr.isFVar && arg.hName?.isNone then
-      result := result.push arg.expr
-    else
-      result := result.push (mkFVar fvarIdsNew[j]!)
-      j := j+1
-  pure (result, fvarIdsNew[j:], goal)
-
-/--
-Given a list of targets of the form `e` or `h : e`, and a pattern, match all the targets
-against the pattern. Returns the list of produced subgoals.
--/
-def rcases (tgts : Array (Option Ident × Syntax))
-  (pat : RCasesPatt) (g : MVarId) : TermElabM (List MVarId) := Term.withSynthesize do
-  let pats ← match tgts.size with
-  | 0 => return [g]
-  | 1 => pure [pat]
-  | _ => pure (processConstructor pat.ref (tgts.map fun _ => {}) false 0 pat.asTuple.2).2
-  let (pats, args) := Array.unzip <|← (tgts.zip pats.toArray).mapM fun ((hName?, tgt), pat) => do
-    let (pat, ty) ← match pat with
-    | .typed ref pat ty => withRef ref do
-      let ty ← Term.elabType ty
-      pure (.typed ref pat (← Term.exprToSyntax ty), some ty)
-    | _ => pure (pat, none)
-    let expr ← Term.ensureHasType ty (← Term.elabTerm tgt ty)
-    pure (pat, { expr, xName? := pat.name?, hName? := hName?.map (·.getId) : GeneralizeArg })
-  let (vs, hs, g) ← generalizeExceptFVar g args
-  let toTag := tgts.filterMap (·.1) |>.zip hs
-  let gs ← rcasesContinue g {} #[] #[] (pats.zip vs).toList (finish (toTag := toTag))
-  pure gs.toList
-
-/--
-The `obtain` tactic in the no-target case. Given a type `T`, create a goal `|- T` and
-and pattern match `T` against the given pattern. Returns the list of goals, with the assumed goal
-first followed by the goals produced by the pattern match.
--/
-def obtainNone (pat : RCasesPatt) (ty : Syntax) (g : MVarId) : TermElabM (List MVarId) :=
-  Term.withSynthesize do
-    let ty ← Term.elabType ty
-    let g₁ ← mkFreshExprMVar (some ty)
-    let (v, g₂) ← (← g.assert (pat.name?.getD default) ty g₁).intro1
-    let gs ← rcasesCore g₂ {} #[] (.fvar v) #[] pat finish
-    pure (g₁.mvarId! :: gs.toList)
-
-mutual
-variable [Monad m] [MonadQuotation m]
-
-/-- Expand a `rintroPat` into an equivalent list of `rcasesPat` patterns. -/
-partial def expandRIntroPat (pat : TSyntax `rintroPat)
-    (acc : Array (TSyntax `rcasesPat) := #[]) (ty? : Option Term := none) :
-    Array (TSyntax `rcasesPat) :=
-  match pat with
-  | `(rintroPat| $p:rcasesPat) => match ty? with
-    | some ty => acc.push <| Unhygienic.run <| withRef p `(rcasesPat| ($p:rcasesPat : $ty))
-    | none => acc.push p
-  | `(rintroPat| ($(pats)* $[: $ty?']?)) => expandRIntroPats pats acc (ty?' <|> ty?)
-  | _ => acc
-
-/-- Expand a list of `rintroPat` into an equivalent list of `rcasesPat` patterns. -/
-partial def expandRIntroPats (pats : Array (TSyntax `rintroPat))
-    (acc : Array (TSyntax `rcasesPat) := #[]) (ty? : Option Term := none) :
-    Array (TSyntax `rcasesPat) :=
-  pats.foldl (fun acc p => expandRIntroPat p acc ty?) acc
-
-end
-
-mutual
-
-/--
-This introduces the pattern `pat`. It has the same arguments as `rcasesCore`, plus:
-* `ty?`: the nearest enclosing type ascription on the current pattern
--/
-partial def rintroCore (g : MVarId) (fs : FVarSubst) (clears : Array FVarId) (a : α)
-    (ref : Syntax) (pat : TSyntax `rintroPat) (ty? : Option Term)
-    (cont : MVarId → FVarSubst → Array FVarId → α → TermElabM α) : TermElabM α := do
-  match pat with
-  | `(rintroPat| $pat:rcasesPat) =>
-    let pat := (← RCasesPatt.parse pat).typed? ref ty?
-    let (v, g) ← g.intro (pat.name?.getD `_)
-    rcasesCore g fs clears (.fvar v) a pat cont
-  | `(rintroPat| ($(pats)* $[: $ty?']?)) =>
-    let ref := if pats.size == 1 then pat.raw else .missing
-    rintroContinue g fs clears ref pats (ty?' <|> ty?) a cont
-  | _ => throwUnsupportedSyntax
-
-/--
-This introduces the list of patterns `pats`. It has the same arguments as `rcasesCore`, plus:
-* `ty?`: the nearest enclosing type ascription on the current pattern
--/
-partial def rintroContinue (g : MVarId) (fs : FVarSubst) (clears : Array FVarId)
-    (ref : Syntax) (pats : TSyntaxArray `rintroPat) (ty? : Option Term) (a : α)
-    (cont : MVarId → FVarSubst → Array FVarId → α → TermElabM α) : TermElabM α := do
-  g.withContext (loop 0 g fs clears a)
-where
-  /-- Runs `rintroContinue` on `pats[i:]` -/
-  loop i g fs clears a := do
-    if h : i < pats.size then
-      rintroCore g fs clears a ref (pats.get ⟨i, h⟩) ty? (loop (i+1))
-    else cont g fs clears a
-
-end
-
-/--
-The implementation of the `rintro` tactic. It takes a list of patterns `pats` and
-an optional type ascription `ty?` and introduces the patterns, resulting in zero or more goals.
--/
-def rintro (pats : TSyntaxArray `rintroPat) (ty? : Option Term)
-    (g : MVarId) : TermElabM (List MVarId) := Term.withSynthesize do
-  (·.toList) <$> rintroContinue g {} #[] .missing pats ty? #[] finish
-
-@[builtin_tactic Lean.Parser.Tactic.rcases] def evalRCases : Tactic := fun stx => do
-  match stx with
-  | `(tactic| rcases%$tk $tgts,* $[with $pat?]?) =>
-    let pat ← match pat? with
-      | some pat => RCasesPatt.parse pat
-      | none     => pure $ RCasesPatt.tuple tk []
-    let tgts := tgts.getElems.map fun tgt =>
-      (if tgt.raw[0].isNone then none else some ⟨tgt.raw[0][0]⟩, tgt.raw[1])
-    let g ← getMainGoal
-    g.withContext do replaceMainGoal (← RCases.rcases tgts pat g)
-  | _ => throwUnsupportedSyntax
-
-@[builtin_tactic Lean.Parser.Tactic.obtain] def evalObtain : Tactic := fun stx => do
-  match stx with
-  | `(tactic| obtain%$tk $[$pat?:rcasesPatMed]? $[: $ty?]? $[:= $val?,*]?) =>
-    let pat? ← liftM <| pat?.mapM RCasesPatt.parse
-    if let some val := val? then
-      let pat  := pat?.getD (RCasesPatt.one tk `_)
-      let pat  := pat.typed? tk ty?
-      let tgts := val.getElems.map fun val => (none, val.raw)
-      let g ← getMainGoal
-      g.withContext do replaceMainGoal (← RCases.rcases tgts pat g)
-    else if let some ty := ty? then
-      let pat := pat?.getD (RCasesPatt.one tk `this)
-      let g ← getMainGoal
-      g.withContext do replaceMainGoal (← RCases.obtainNone pat ty g)
-    else
-      throwError "\
-        `obtain` requires either an expected type or a value.\n\
-        usage: `obtain ⟨patt⟩? : type (:= val)?` or `obtain ⟨patt⟩? (: type)? := val`"
-  | _ => throwUnsupportedSyntax
-
-@[builtin_tactic Lean.Parser.Tactic.rintro] def evalRIntro : Tactic := fun stx => do
-  match stx with
-  | `(tactic| rintro $pats* $[: $ty?]?) =>
-    let g ← getMainGoal
-    g.withContext do replaceMainGoal (← RCases.rintro pats ty? g)
-  | _ => throwUnsupportedSyntax
-
-end RCases

src/Lean/Elab/Tactic/Repeat.lean

@@ -1,25 +0,0 @@
-/-
-Copyright (c) 2022 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Scott Morrison
--/
-import Lean.Meta.Tactic.Repeat
-import Lean.Elab.Tactic.Basic
-
-namespace Lean.Elab.Tactic
-
-@[builtin_tactic repeat']
-def evalRepeat' : Tactic := fun stx => do
-  match stx with
-  | `(tactic| repeat' $tac:tacticSeq) =>
-     setGoals (← Meta.repeat' (evalTacticAtRaw tac) (← getGoals))
-  | _ => throwUnsupportedSyntax
-
-@[builtin_tactic repeat1']
-def evalRepeat1' : Tactic := fun stx => do
-  match stx with
-  | `(tactic| repeat1' $tac:tacticSeq) =>
-    setGoals (← Meta.repeat1' (evalTacticAtRaw tac) (← getGoals))
-  | _ => throwUnsupportedSyntax
-
-end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Simp.lean

@@ -72,7 +72,6 @@ def Simp.DischargeWrapper.with (w : Simp.DischargeWrapper) (x : Option Simp.Disc
     finally
       set (← ref.get)
 
-/-- Construct a `Simp.DischargeWrapper` from the `Syntax` for a `simp` discharger. -/
 private def mkDischargeWrapper (optDischargeSyntax : Syntax) : TacticM Simp.DischargeWrapper := do
   if optDischargeSyntax.isNone then
     return Simp.DischargeWrapper.default
@@ -259,15 +258,8 @@ structure MkSimpContextResult where
    If `kind != SimpKind.simp`, the `discharge` option must be `none`
 
    TODO: generate error message if non `rfl` theorems are provided as arguments to `dsimp`.
-
-   The argument `simpTheorems` defaults to `getSimpTheorems`,
-   but allows overriding with an arbitrary mechanism to choose
-   the simp theorems besides those specified in the syntax.
-   Note that if the syntax includes `simp only`, the `simpTheorems` argument is ignored.
 -/
-def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
-    (ignoreStarArg : Bool := false) (simpTheorems : CoreM SimpTheorems := getSimpTheorems) :
-    TacticM MkSimpContextResult := do
+def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ignoreStarArg : Bool := false) : TacticM MkSimpContextResult := do
   if !stx[2].isNone then
     if kind == SimpKind.simpAll then
       throwError "'simp_all' tactic does not support 'discharger' option"
@@ -278,7 +270,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
   let simpTheorems ← if simpOnly then
     simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
   else
-    simpTheorems
+    getSimpTheorems
   let simprocs ← if simpOnly then pure {} else Simp.getSimprocs
   let congrTheorems ← getSimpCongrTheorems
   let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := #[simprocs]) {

src/Lean/LocalContext.lean

@@ -141,15 +141,6 @@ def hasExprMVar : LocalDecl → Bool
   | cdecl (type := t) ..              => t.hasExprMVar
   | ldecl (type := t) (value := v) .. => t.hasExprMVar || v.hasExprMVar
 
-/--
-Set the kind of a `LocalDecl`.
--/
-def setKind : LocalDecl → LocalDeclKind → LocalDecl
-  | cdecl index fvarId userName type bi _, kind =>
-      cdecl index fvarId userName type bi kind
-  | ldecl index fvarId userName type value nonDep _, kind =>
-      ldecl index fvarId userName type value nonDep kind
-
 end LocalDecl
 
 /-- A LocalContext is an ordered set of local variable declarations.
@@ -320,13 +311,6 @@ def renameUserName (lctx : LocalContext) (fromName : Name) (toName : Name) : Loc
       { fvarIdToDecl := map.insert decl.fvarId decl
         decls        := decls.set decl.index decl }
 
-/--
-Set the kind of the given fvar.
--/
-def setKind (lctx : LocalContext) (fvarId : FVarId)
-    (kind : LocalDeclKind) : LocalContext :=
-  lctx.modifyLocalDecl fvarId (·.setKind kind)
-
 def setBinderInfo (lctx : LocalContext) (fvarId : FVarId) (bi : BinderInfo) : LocalContext :=
   modifyLocalDecl lctx fvarId fun decl => decl.setBinderInfo bi
 
@@ -467,27 +451,6 @@ def sanitizeNames (lctx : LocalContext) : StateM NameSanitizerState LocalContext
             modify fun s => s.insert decl.userName
             pure lctx
 
-/--
-Given an `FVarId`, this function returns the corresponding user name,
-but only if the name can be used to recover the original FVarId.
--/
-def getRoundtrippingUserName? (lctx : LocalContext) (fvarId : FVarId) : Option Name := do
-  let ldecl₁ ← lctx.find? fvarId
-  let ldecl₂ ← lctx.findFromUserName? ldecl₁.userName
-  guard <| ldecl₁.fvarId == ldecl₂.fvarId
-  some ldecl₁.userName
-
-/--
-Sort the given `FVarId`s by the order in which they appear in `lctx`. If any of
-the `FVarId`s do not appear in `lctx`, the result is unspecified.
--/
-def sortFVarsByContextOrder (lctx : LocalContext) (hyps : Array FVarId) : Array FVarId :=
-  let hyps := hyps.map fun fvarId =>
-    match lctx.fvarIdToDecl.find? fvarId with
-    | none => (0, fvarId)
-    | some ldecl => (ldecl.index, fvarId)
-  hyps.qsort (fun h i => h.fst < i.fst) |>.map (·.snd)
-
 end LocalContext
 
 /-- Class used to denote that `m` has a local context. -/

src/Lean/Meta.lean

@@ -43,4 +43,3 @@ import Lean.Meta.CasesOn
 import Lean.Meta.ExprLens
 import Lean.Meta.ExprTraverse
 import Lean.Meta.Eval
-import Lean.Meta.CoeAttr

src/Lean/Meta/CoeAttr.lean

@@ -1,86 +0,0 @@
-/-
-Copyright (c) 2022 Gabriel Ebner. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Mario Carneiro, Leonardo de Moura
--/
-import Lean.Attributes
-import Lean.ScopedEnvExtension
-import Lean.Meta.FunInfo
-
-/-!
-# The `@[coe]` attribute, used to delaborate coercion functions as `↑`
-
-When writing a coercion, if the pattern
-```
-@[coe]
-def A.toB (a : A) : B := sorry
-
-instance : Coe A B where coe := A.toB
-```
-is used, then `A.toB a` will be pretty-printed as `↑a`.
--/
-
-namespace Lean.Meta
-
-/-- The different types of coercions that are supported by the `coe` attribute. -/
-inductive CoeFnType
-  /-- The basic coercion `↑x`, see `CoeT.coe` -/
-  | coe
-  /-- The coercion to a function type, see `CoeFun.coe` -/
-  | coeFun
-  /-- The coercion to a type, see `CoeSort.coe` -/
-  | coeSort
-  deriving Inhabited, Repr, DecidableEq
-
-instance : ToExpr CoeFnType where
-  toTypeExpr := mkConst ``CoeFnType
-  toExpr := open CoeFnType in fun
-    | coe => mkConst ``coe
-    | coeFun => mkConst ``coeFun
-    | coeSort => mkConst ``coeSort
-
-/-- Information associated to a coercion function to enable sensible delaboration. -/
-structure CoeFnInfo where
-  /-- The number of arguments to the coercion function -/
-  numArgs : Nat
-  /-- The argument index that represents the value being coerced -/
-  coercee : Nat
-  /-- The type of coercion -/
-  type : CoeFnType
-  deriving Inhabited, Repr
-
-instance : ToExpr CoeFnInfo where
-  toTypeExpr := mkConst ``CoeFnInfo
-  toExpr | ⟨a, b, c⟩ => mkApp3 (mkConst ``CoeFnInfo.mk) (toExpr a) (toExpr b) (toExpr c)
-
-/-- The environment extension for tracking coercion functions for delaboration -/
--- TODO: does it need to be a scoped extension
-initialize coeExt : SimpleScopedEnvExtension (Name × CoeFnInfo) (NameMap CoeFnInfo) ←
-  registerSimpleScopedEnvExtension {
-    addEntry := fun st (n, i) => st.insert n i
-    initial := {}
-  }
-
-/-- Lookup the coercion information for a given function -/
-def getCoeFnInfo? (fn : Name) : CoreM (Option CoeFnInfo) :=
-  return (coeExt.getState (← getEnv)).find? fn
-
-/-- Add `name` to the coercion extension and add a coercion delaborator for the function. -/
-def registerCoercion (name : Name) (info : Option CoeFnInfo := none) : MetaM Unit := do
-  let info ← match info with | some info => pure info | none => do
-    let fnInfo ← getFunInfo (← mkConstWithLevelParams name)
-    let some coercee := fnInfo.paramInfo.findIdx? (·.binderInfo.isExplicit)
-      | throwError "{name} has no explicit arguments"
-    pure { numArgs := coercee + 1, coercee, type := .coe }
-  modifyEnv fun env => coeExt.addEntry env (name, info)
-
-builtin_initialize registerBuiltinAttribute {
-  name := `coe
-  descr := "Adds a definition as a coercion"
-  add := fun decl _stx kind => MetaM.run' do
-    unless kind == .global do
-      throwError "cannot add local or scoped coe attribute"
-    registerCoercion decl
-}
-
-end Lean.Meta

src/Lean/Meta/DiscrTree.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Jannis Limperg, Scott Morrison
+Authors: Leonardo de Moura
 -/
 import Lean.Meta.WHNF
 import Lean.Meta.Transform
@@ -32,8 +32,8 @@ namespace Lean.Meta.DiscrTree
   and `Add.add Nat Nat.hasAdd a b` generates paths with the following keys
   respectively
   ```
-  ⟨Add.add, 4⟩, α, *, *, *
-  ⟨Add.add, 4⟩, Nat, *, ⟨a,0⟩, ⟨b,0⟩
+  ⟨Add.add, 4⟩, *, *, *, *
+  ⟨Add.add, 4⟩, *, *, ⟨a,0⟩, ⟨b,0⟩
   ```
 
   That is, we don't reduce `Add.add Nat inst a b` into `Nat.add a b`.
@@ -450,18 +450,6 @@ def insert [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (config : WhnfCoreCon
   let keys ← mkPath e config
   return d.insertCore keys v
 
-/--
-Inserts a value into a discrimination tree,
-but only if its key is not of the form `#[*]` or `#[=, *, *, *]`.
--/
-def insertIfSpecific [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (config : WhnfCoreConfig) : MetaM (DiscrTree α) := do
-  let keys ← mkPath e config
-  return if keys == #[Key.star] || keys == #[Key.const `Eq 3, Key.star, Key.star, Key.star] then
-    d
-  else
-    d.insertCore keys v
-
-
 private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig) : MetaM (Key × Array Expr) := do
   let e ← reduceDT e root config
   unless root do
@@ -688,124 +676,4 @@ where
         | .arrow => visitNonStar .other #[] (← visitNonStar k args (← visitStar result))
         | _      => visitNonStar k args (← visitStar result)
 
-namespace Trie
-
--- `Inhabited` instance to allow `partial` definitions below.
-private local instance [Monad m] : Inhabited (σ → β → m σ) := ⟨fun s _ => pure s⟩
-
-/--
-Monadically fold the keys and values stored in a `Trie`.
--/
-partial def foldM [Monad m] (initialKeys : Array Key)
-    (f : σ → Array Key → α → m σ) : (init : σ) → Trie α → m σ
-  | init, Trie.node vs children => do
-    let s ← vs.foldlM (init := init) fun s v => f s initialKeys v
-    children.foldlM (init := s) fun s (k, t) =>
-      t.foldM (initialKeys.push k) f s
-
-/--
-Fold the keys and values stored in a `Trie`.
--/
-@[inline]
-def fold (initialKeys : Array Key) (f : σ → Array Key → α → σ) (init : σ) (t : Trie α) : σ :=
-  Id.run <| t.foldM initialKeys (init := init) fun s k a => return f s k a
-
-/--
-Monadically fold the values stored in a `Trie`.
--/
-partial def foldValuesM [Monad m] (f : σ → α → m σ) : (init : σ) → Trie α → m σ
-  | init, node vs children => do
-    let s ← vs.foldlM (init := init) f
-    children.foldlM (init := s) fun s (_, c) => c.foldValuesM (init := s) f
-
-/--
-Fold the values stored in a `Trie`.
--/
-@[inline]
-def foldValues (f : σ → α → σ) (init : σ) (t : Trie α) : σ :=
-  Id.run <| t.foldValuesM (init := init) f
-
-/--
-The number of values stored in a `Trie`.
--/
-partial def size : Trie α → Nat
-  | Trie.node vs children =>
-    children.foldl (init := vs.size) fun n (_, c) => n + size c
-
-end Trie
-
-
-/--
-Monadically fold over the keys and values stored in a `DiscrTree`.
--/
-@[inline]
-def foldM [Monad m] (f : σ → Array Key → α → m σ) (init : σ)
-    (t : DiscrTree α) : m σ :=
-  t.root.foldlM (init := init) fun s k t => t.foldM #[k] (init := s) f
-
-/--
-Fold over the keys and values stored in a `DiscrTree`
--/
-@[inline]
-def fold (f : σ → Array Key → α → σ) (init : σ) (t : DiscrTree α) : σ :=
-  Id.run <| t.foldM (init := init) fun s keys a => return f s keys a
-
-/--
-Monadically fold over the values stored in a `DiscrTree`.
--/
-@[inline]
-def foldValuesM [Monad m] (f : σ → α → m σ) (init : σ) (t : DiscrTree α) :
-    m σ :=
-  t.root.foldlM (init := init) fun s _ t => t.foldValuesM (init := s) f
-
-/--
-Fold over the values stored in a `DiscrTree`.
--/
-@[inline]
-def foldValues (f : σ → α → σ) (init : σ) (t : DiscrTree α) : σ :=
-  Id.run <| t.foldValuesM (init := init) f
-
-/--
-Check for the presence of a value satisfying a predicate.
--/
-@[inline]
-def containsValueP [BEq α] (t : DiscrTree α) (f : α → Bool) : Bool :=
-  t.foldValues (init := false) fun r a => r || f a
-
-/--
-Extract the values stored in a `DiscrTree`.
--/
-@[inline]
-def values (t : DiscrTree α) : Array α :=
-  t.foldValues (init := #[]) fun as a => as.push a
-
-/--
-Extract the keys and values stored in a `DiscrTree`.
--/
-@[inline]
-def toArray (t : DiscrTree α) : Array (Array Key × α) :=
-  t.fold (init := #[]) fun as keys a => as.push (keys, a)
-
-/--
-Get the number of values stored in a `DiscrTree`. O(n) in the size of the tree.
--/
-@[inline]
-def size (t : DiscrTree α) : Nat :=
-  t.root.foldl (init := 0) fun n _ t => n + t.size
-
-variable {m : Type → Type} [Monad m]
-
-/-- Apply a monadic function to the array of values at each node in a `DiscrTree`. -/
-partial def Trie.mapArraysM (t : DiscrTree.Trie α) (f : Array α → m (Array β)) :
-    m (DiscrTree.Trie β) :=
-  match t with
-  | .node vs children =>
-    return .node (← f vs) (← children.mapM fun (k, t') => do pure (k, ← t'.mapArraysM f))
-
-/-- Apply a monadic function to the array of values at each node in a `DiscrTree`. -/
-def mapArraysM (d : DiscrTree α) (f : Array α → m (Array β)) : m (DiscrTree β) := do
-  pure { root := ← d.root.mapM (fun t => t.mapArraysM f) }
-
-/-- Apply a function to the array of values at each node in a `DiscrTree`. -/
-def mapArrays (d : DiscrTree α) (f : Array α → Array β) : DiscrTree β :=
-  Id.run <| d.mapArraysM fun A => pure (f A)
+end Lean.Meta.DiscrTree

src/Lean/Meta/Tactic.lean

@@ -28,5 +28,4 @@ import Lean.Meta.Tactic.Rename
 import Lean.Meta.Tactic.LinearArith
 import Lean.Meta.Tactic.AC
 import Lean.Meta.Tactic.Refl
-import Lean.Meta.Tactic.Congr
-import Lean.Meta.Tactic.Repeat
+import Lean.Meta.Tactic.Congr

src/Lean/Meta/Tactic/Apply.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Siddhartha Gadgil
+Authors: Leonardo de Moura
 -/
 import Lean.Util.FindMVar
 import Lean.Meta.SynthInstance
@@ -230,25 +230,4 @@ def _root_.Lean.MVarId.exfalso (mvarId : MVarId) : MetaM MVarId :=
     mvarId.assign (mkApp2 (mkConst ``False.elim [u]) target mvarIdNew)
     return mvarIdNew.mvarId!
 
-/--
-Apply the `n`-th constructor of the target type,
-checking that it is an inductive type,
-and that there are the expected number of constructors.
--/
-def _root_.Lean.MVarId.nthConstructor
-    (name : Name) (idx : Nat) (expected? : Option Nat := none) (goal : MVarId) :
-    MetaM (List MVarId) := do
-  goal.withContext do
-    goal.checkNotAssigned name
-    matchConstInduct (← goal.getType').getAppFn
-      (fun _ => throwTacticEx name goal "target is not an inductive datatype")
-      fun ival us => do
-        if let some e := expected? then unless ival.ctors.length == e do
-          throwTacticEx name goal
-            s!"{name} tactic works for inductive types with exactly {e} constructors"
-        if h : idx < ival.ctors.length then
-          goal.apply <| mkConst ival.ctors[idx] us
-        else
-          throwTacticEx name goal s!"index {idx} out of bounds, only {ival.ctors.length} constructors"
-
 end Lean.Meta

src/Lean/Meta/Tactic/FVarSubst.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Mario Carneiro
+Authors: Leonardo de Moura
 -/
 import Lean.Data.AssocList
 import Lean.Expr
@@ -63,13 +63,6 @@ def domain (s : FVarSubst) : List FVarId :=
 def any (p : FVarId → Expr → Bool) (s : FVarSubst) : Bool :=
   s.map.any p
 
-/--
-Constructs a substitution consisting of `s` followed by `t`.
-This satisfies `(s.append t).apply e = t.apply (s.apply e)`
--/
-def append (s t : FVarSubst) : FVarSubst :=
-  s.1.foldl (fun s' k v => s'.insert k (t.apply v)) t
-
 end FVarSubst
 end Meta
 

src/Lean/Meta/Tactic/Repeat.lean

@@ -1,64 +0,0 @@
-/-
-Copyright (c) 2022 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Scott Morrison
--/
-import Lean.Meta.Basic
-
-namespace Lean.Meta
-/--
-Implementation of `repeat'` and `repeat1'`.
-
-`repeat'Core f` runs `f` on all of the goals to produce a new list of goals,
-then runs `f` again on all of those goals, and repeats until `f` fails on all remaining goals,
-or until `maxIters` total calls to `f` have occurred.
-
-Returns a boolean indicating whether `f` succeeded at least once, and
-all the remaining goals (i.e. those on which `f` failed).
--/
-def repeat'Core [Monad m] [MonadExcept ε m] [MonadBacktrack s m] [MonadMCtx m]
-    (f : MVarId → m (List MVarId)) (goals : List MVarId) (maxIters := 100000) :
-    m (Bool × List MVarId) := do
-  let (progress, acc) ← go maxIters false goals [] #[]
-  pure (progress, (← acc.filterM fun g => not <$> g.isAssigned).toList)
-where
-  /-- Auxiliary for `repeat'Core`. `repeat'Core.go f maxIters progress goals stk acc` evaluates to
-  essentially `acc.toList ++ repeat' f (goals::stk).join maxIters`: that is, `acc` are goals we will
-  not revisit, and `(goals::stk).join` is the accumulated todo list of subgoals. -/
-  go : Nat → Bool → List MVarId → List (List MVarId) → Array MVarId → m (Bool × Array MVarId)
-  | _, p, [], [], acc => pure (p, acc)
-  | n, p, [], goals::stk, acc => go n p goals stk acc
-  | n, p, g::goals, stk, acc => do
-    if ← g.isAssigned then
-      go n p goals stk acc
-    else
-      match n with
-      | 0 => pure <| (p, acc.push g ++ goals |> stk.foldl .appendList)
-      | n+1 =>
-        match ← observing? (f g) with
-        | some goals' => go n true goals' (goals::stk) acc
-        | none => go n p goals stk (acc.push g)
-termination_by n p goals stk _ => (n, stk, goals)
-
-/--
-`repeat' f` runs `f` on all of the goals to produce a new list of goals,
-then runs `f` again on all of those goals, and repeats until `f` fails on all remaining goals,
-or until `maxIters` total calls to `f` have occurred.
-Always succeeds (returning the original goals if `f` fails on all of them).
--/
-def repeat' [Monad m] [MonadExcept ε m] [MonadBacktrack s m] [MonadMCtx m]
-    (f : MVarId → m (List MVarId)) (goals : List MVarId) (maxIters := 100000) : m (List MVarId) :=
-  repeat'Core f goals maxIters <&> (·.2)
-
-/--
-`repeat1' f` runs `f` on all of the goals to produce a new list of goals,
-then runs `f` again on all of those goals, and repeats until `f` fails on all remaining goals,
-or until `maxIters` total calls to `f` have occurred.
-Fails if `f` does not succeed at least once.
--/
-def repeat1' [Monad m] [MonadError m] [MonadExcept ε m] [MonadBacktrack s m] [MonadMCtx m]
-    (f : MVarId → m (List MVarId)) (goals : List MVarId) (maxIters := 100000) : m (List MVarId) := do
-  let (.true, goals) ← repeat'Core f goals maxIters | throwError "repeat1' made no progress"
-  pure goals
-
-end Lean.Meta

src/Lean/Meta/Tactic/Replace.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Util.ForEachExpr
-import Lean.Elab.InfoTree.Main
 import Lean.Meta.AppBuilder
 import Lean.Meta.MatchUtil
 import Lean.Meta.Tactic.Util
@@ -140,54 +139,29 @@ def _root_.Lean.MVarId.change (mvarId : MVarId) (targetNew : Expr) (checkDefEq :
 def change (mvarId : MVarId) (targetNew : Expr) (checkDefEq := true) : MetaM MVarId := mvarId.withContext do
   mvarId.change targetNew checkDefEq
 
-/-- Runs the continuation `k` after temporarily reverting some variables from the local context of a metavariable (identified by `mvarId`), then reintroduces local variables as specified by `k`.
-
-The argument `fvarIds` is an array of `fvarIds` to revert in the order specified. An error is thrown if they cannot be reverted in order.
-
-Once the local variables have been reverted, `k` is passed `mvarId` along with an array of local variables that were reverted. This array always has `fvarIds` as a prefix, but it may contain additional variables that were reverted due to dependencies. `k` returns a value, a goal, an array of _link variables_.
-
-Once `k` has completed, one variable is introduced for each link variable returned by `k`. If the returned variable is `none`, the variable is just introduced. If it is `some fv`, the variable is introduced and then linked as an alias of `fv` in the info tree. For example, having `k` return `fvars.map .some` as the link variables causes all reverted variables to be introduced and linked.
-
-Returns the value returned by `k` along with the resulting goal.
- -/
-def _root_.Lean.MVarId.withReverted (mvarId : MVarId) (fvarIds : Array FVarId)
-    (k : MVarId → Array FVarId → MetaM (α × Array (Option FVarId) × MVarId))
-    (clearAuxDeclsInsteadOfRevert := false) : MetaM (α × MVarId) := do
-  let (xs, mvarId) ← mvarId.revert fvarIds true clearAuxDeclsInsteadOfRevert
-  let (r, xs', mvarId) ← k mvarId xs
-  let (ys, mvarId) ← mvarId.introNP xs'.size
-  mvarId.withContext do
-    for x? in xs', y in ys do
-      if let some x := x? then
-        Elab.pushInfoLeaf (.ofFVarAliasInfo { id := y, baseId := x, userName := ← y.getUserName })
-  return (r, mvarId)
-
 /--
-Replaces the type of the free variable `fvarId` with `typeNew`.
-
-If `checkDefEq` is `true` then an error is thrown if `typeNew` is not definitionally
-equal to the type of `fvarId`. Otherwise this function assumes `typeNew` and the type
-of `fvarId` are definitionally equal.
-
-This function is the same as `Lean.MVarId.changeLocalDecl` but makes sure to push substitution
-information into the info tree.
+Replace the type of the free variable `fvarId` with `typeNew`.
+If `checkDefEq = false`, this method assumes that `typeNew` is definitionally equal to `fvarId` type.
+If `checkDefEq = true`, throw an error if `typeNew` is not definitionally equal to `fvarId` type.
 -/
-def _root_.Lean.MVarId.changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr)
-    (checkDefEq := true) : MetaM MVarId := do
+def _root_.Lean.MVarId.changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkDefEq := true) : MetaM MVarId := do
   mvarId.checkNotAssigned `changeLocalDecl
-  let (_, mvarId) ← mvarId.withReverted #[fvarId] fun mvarId fvars => mvarId.withContext do
+  let (xs, mvarId) ← mvarId.revert #[fvarId] true
+  mvarId.withContext do
+    let numReverted := xs.size
+    let target ← mvarId.getType
     let check (typeOld : Expr) : MetaM Unit := do
       if checkDefEq then
-        unless ← isDefEq typeNew typeOld do
-          throwTacticEx `changeLocalDecl mvarId
-            m!"given type{indentExpr typeNew}\nis not definitionally equal to{indentExpr typeOld}"
-    let finalize (targetNew : Expr) := do
-      return ((), fvars.map .some, ← mvarId.replaceTargetDefEq targetNew)
-    match ← mvarId.getType with
-    | .forallE n d b bi => do check d; finalize (.forallE n typeNew b bi)
-    | .letE n t v b ndep => do check t; finalize (.letE n typeNew v b ndep)
-    | _ => throwTacticEx `changeLocalDecl mvarId "unexpected auxiliary target"
-  return mvarId
+        unless (← isDefEq typeNew typeOld) do
+          throwTacticEx `changeHypothesis mvarId m!"given type{indentExpr typeNew}\nis not definitionally equal to{indentExpr typeOld}"
+    let finalize (targetNew : Expr) : MetaM MVarId := do
+      let mvarId ← mvarId.replaceTargetDefEq targetNew
+      let (_, mvarId) ← mvarId.introNP numReverted
+      pure mvarId
+    match target with
+    | .forallE n d b c => do check d; finalize (mkForall n c typeNew b)
+    | .letE n t v b _  => do check t; finalize (mkLet n typeNew v b)
+    | _ => throwTacticEx `changeHypothesis mvarId "unexpected auxiliary target"
 
 @[deprecated MVarId.changeLocalDecl]
 def changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkDefEq := true) : MetaM MVarId := do

src/Lean/MetavarContext.lean

@@ -393,18 +393,6 @@ def _root_.Lean.MVarId.isDelayedAssigned [Monad m] [MonadMCtx m] (mvarId : MVarI
 def isMVarDelayedAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool := do
   mvarId.isDelayedAssigned
 
-/--
-Check whether a metavariable is assigned or delayed-assigned. A
-delayed-assigned metavariable is already 'solved' but the solution cannot be
-substituted yet because we have to wait for some other metavariables to be
-assigned first. So in many situations you want to treat a delayed-assigned
-metavariable as assigned.
--/
-def _root_.Lean.MVarId.isAssignedOrDelayedAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) :
-    m Bool := do
-  let mctx ← getMCtx
-  return mctx.eAssignment.contains mvarId || mctx.dAssignment.contains mvarId
-
 def isLevelMVarAssignable [Monad m] [MonadMCtx m] (mvarId : LMVarId) : m Bool := do
   let mctx ← getMCtx
   match mctx.lDepth.find? mvarId with
@@ -495,10 +483,6 @@ def _root_.Lean.MVarId.assign [MonadMCtx m] (mvarId : MVarId) (val : Expr) : m U
 def assignExprMVar [MonadMCtx m] (mvarId : MVarId) (val : Expr) : m Unit :=
   mvarId.assign val
 
-/--
-Add a delayed assignment for the given metavariable. You must make sure that
-the metavariable is not already assigned or delayed-assigned.
--/
 def assignDelayedMVar [MonadMCtx m] (mvarId : MVarId) (fvars : Array Expr) (mvarIdPending : MVarId) : m Unit :=
   modifyMCtx fun m => { m with dAssignment := m.dAssignment.insert mvarId { fvars, mvarIdPending } }
 
@@ -825,20 +809,6 @@ def findDecl? (mctx : MetavarContext) (mvarId : MVarId) : Option MetavarDecl :=
 def findUserName? (mctx : MetavarContext) (userName : Name) : Option MVarId :=
   mctx.userNames.find? userName
 
-/--
-Modify the declaration of a metavariable. If the metavariable is not declared,
-the `MetavarContext` is returned unchanged.
-
-You must ensure that the modification is legal. In particular, expressions may
-only be replaced with defeq expressions.
--/
-def modifyExprMVarDecl (mctx : MetavarContext) (mvarId : MVarId)
-    (f : MetavarDecl → MetavarDecl) : MetavarContext :=
-  if let some mdecl := mctx.decls.find? mvarId then
-    { mctx with decls := mctx.decls.insert mvarId (f mdecl) }
-  else
-    mctx
-
 def setMVarKind (mctx : MetavarContext) (mvarId : MVarId) (kind : MetavarKind) : MetavarContext :=
   let decl := mctx.getDecl mvarId
   { mctx with decls := mctx.decls.insert mvarId { decl with kind := kind } }
@@ -870,35 +840,6 @@ def setMVarType (mctx : MetavarContext) (mvarId : MVarId) (type : Expr) : Metava
   let decl := mctx.getDecl mvarId
   { mctx with decls := mctx.decls.insert mvarId { decl with type := type } }
 
-/--
-Modify the local context of a metavariable. If the metavariable is not declared,
-the `MetavarContext` is returned unchanged.
-
-You must ensure that the modification is legal. In particular, expressions may
-only be replaced with defeq expressions.
--/
-def modifyExprMVarLCtx (mctx : MetavarContext) (mvarId : MVarId)
-    (f : LocalContext → LocalContext) : MetavarContext :=
-  mctx.modifyExprMVarDecl mvarId fun mdecl => { mdecl with lctx := f mdecl.lctx }
-
-/--
-Set the kind of an fvar. If the given metavariable is not declared or the
-given fvar doesn't exist in its context, the `MetavarContext` is returned
-unchanged.
--/
-def setFVarKind (mctx : MetavarContext) (mvarId : MVarId) (fvarId : FVarId)
-    (kind : LocalDeclKind) : MetavarContext :=
-  mctx.modifyExprMVarLCtx mvarId (·.setKind fvarId kind)
-
-/--
-Set the `BinderInfo` of an fvar. If the given metavariable is not declared or
-the given fvar doesn't exist in its context, the `MetavarContext` is returned
-unchanged.
--/
-def setFVarBinderInfo (mctx : MetavarContext) (mvarId : MVarId)
-    (fvarId : FVarId) (bi : BinderInfo) : MetavarContext :=
-  mctx.modifyExprMVarLCtx mvarId (·.setBinderInfo fvarId bi)
-
 def findLevelDepth? (mctx : MetavarContext) (mvarId : LMVarId) : Option Nat :=
   mctx.lDepth.find? mvarId
 
@@ -1436,46 +1377,4 @@ def getExprAssignmentDomain (mctx : MetavarContext) : Array MVarId :=
 
 end MetavarContext
 
-namespace MVarId
-
-/--
-Modify the declaration of a metavariable. If the metavariable is not declared,
-nothing happens.
-
-You must ensure that the modification is legal. In particular, expressions may
-only be replaced with defeq expressions.
--/
-def modifyDecl [MonadMCtx m] (mvarId : MVarId)
-    (f : MetavarDecl → MetavarDecl) : m Unit :=
-  modifyMCtx (·.modifyExprMVarDecl mvarId f)
-
-/--
-Modify the local context of a metavariable. If the metavariable is not declared,
-nothing happens.
-
-You must ensure that the modification is legal. In particular, expressions may
-only be replaced with defeq expressions.
--/
-def modifyLCtx [MonadMCtx m] (mvarId : MVarId)
-    (f : LocalContext → LocalContext) : m Unit :=
-  modifyMCtx (·.modifyExprMVarLCtx mvarId f)
-
-/--
-Set the kind of an fvar. If the given metavariable is not declared or the
-given fvar doesn't exist in its context, nothing happens.
--/
-def setFVarKind [MonadMCtx m] (mvarId : MVarId) (fvarId : FVarId)
-    (kind : LocalDeclKind) : m Unit :=
-  modifyMCtx (·.setFVarKind mvarId fvarId kind)
-
-/--
-Set the `BinderInfo` of an fvar. If the given metavariable is not declared or
-the given fvar doesn't exist in its context, nothing happens.
--/
-def setFVarBinderInfo [MonadMCtx m] (mvarId : MVarId) (fvarId : FVarId)
-    (bi : BinderInfo) : m Unit :=
-  modifyMCtx (·.setFVarBinderInfo mvarId fvarId bi)
-
-end MVarId
-
 end Lean

src/Lean/Parser/Tactic.lean

@@ -92,9 +92,6 @@ example : (List.range 1000).length = 1000 := by native_decide
 @[builtin_tactic_parser] def nativeDecide := leading_parser
   nonReservedSymbol "native_decide"
 
-builtin_initialize
-  register_parser_alias "matchRhsTacticSeq" matchRhs
-
 end Tactic
 end Parser
 end Lean

src/Lean/Parser/Term.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Sebastian Ullrich, Mario Carneiro
+Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 import Lean.Parser.Attr
 import Lean.Parser.Level
@@ -432,9 +432,7 @@ Empty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if
 Lean can show that an empty set of patterns is exhaustive given `e`'s type,
 e.g. because it has no constructors.
 -/
-@[builtin_term_parser] def «nomatch» := leading_parser:leadPrec "nomatch " >> sepBy1 termParser ", "
-
-@[builtin_term_parser] def «nofun» := leading_parser "nofun"
+@[builtin_term_parser] def «nomatch» := leading_parser:leadPrec "nomatch " >> termParser
 
 def funImplicitBinder := withAntiquot (mkAntiquot "implicitBinder" ``implicitBinder) <|
   atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder
@@ -601,19 +599,6 @@ def matchAltsWhereDecls := leading_parser
 @[builtin_term_parser] def noindex := leading_parser
   "no_index " >> termParser maxPrec
 
-/--
-`unsafe t : α` is an expression constructor which allows using unsafe declarations inside the
-body of `t : α`, by creating an auxiliary definition containing `t` and using `implementedBy` to
-wrap it in a safe interface. It is required that `α` is nonempty for this to be sound,
-but even beyond that, an `unsafe` block should be carefully inspected for memory safety because
-the compiler is unable to guarantee the safety of the operation.
-
-For example, the `evalExpr` function is unsafe, because the compiler cannot guarantee that when
-you call ```evalExpr Foo ``Foo e``` that the type `Foo` corresponds to the name `Foo`, but in a
-particular use case, we can ensure this, so `unsafe (evalExpr Foo ``Foo e)` is a correct usage.
--/
-@[builtin_term_parser] def «unsafe» := leading_parser:leadPrec "unsafe " >> termParser
-
 /-- `binrel% r a b` elaborates `r a b` as a binary relation using the type propogation protocol in `Lean.Elab.Extra`. -/
 @[builtin_term_parser] def binrel := leading_parser
   "binrel% " >> ident >> ppSpace >> termParser maxPrec >> ppSpace >> termParser maxPrec

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1,13 +1,13 @@
 /-
 Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich, Leonardo de Moura, Gabriel Ebner, Mario Carneiro
+Authors: Sebastian Ullrich
 -/
-import Lean.Parser
+
 import Lean.PrettyPrinter.Delaborator.Basic
 import Lean.PrettyPrinter.Delaborator.SubExpr
 import Lean.PrettyPrinter.Delaborator.TopDownAnalyze
-import Lean.Meta.CoeAttr
+import Lean.Parser
 
 namespace Lean.PrettyPrinter.Delaborator
 open Lean.Meta
@@ -315,8 +315,7 @@ Default delaborator for applications.
 -/
 @[builtin_delab app]
 def delabApp : Delab := do
-  let e ← getExpr
-  delabAppCore e.getAppNumArgs delabAppFn
+  delabAppCore (← getExpr).getAppNumArgs delabAppFn
 
 /--
 The `withOverApp` combinator allows delaborators to handle "over-application" by using the core
@@ -811,27 +810,6 @@ def delabProjectionApp : Delab := whenPPOption getPPStructureProjections $ do
     let appStx ← withAppArg delab
     `($(appStx).$(mkIdent f):ident)
 
-/--
-This delaborator tries to elide functions which are known coercions.
-For example, `Int.ofNat` is a coercion, so instead of printing `ofNat n` we just print `↑n`,
-and when re-parsing this we can (usually) recover the specific coercion being used.
--/
-@[builtin_delab app]
-def coeDelaborator : Delab := whenPPOption getPPCoercions do
-  let e ← getExpr
-  let .const declName _ := e.getAppFn | failure
-  let some info ← Meta.getCoeFnInfo? declName | failure
-  let n := e.getAppNumArgs
-  withOverApp info.numArgs do
-    match info.type with
-    | .coe => `(↑$(← withNaryArg info.coercee delab))
-    | .coeFun =>
-      if n = info.numArgs then
-        `(⇑$(← withNaryArg info.coercee delab))
-      else
-        withNaryArg info.coercee delab
-    | .coeSort => `(↥$(← withNaryArg info.coercee delab))
-
 @[builtin_delab app.dite]
 def delabDIte : Delab := whenPPOption getPPNotation <| withOverApp 5 do
   -- Note: we keep this as a delaborator for now because it actually accesses the expression.

src/Lean/Server/CodeActions.lean

@@ -68,38 +68,18 @@ to perform the computation after the user has clicked on the code action in thei
 def CodeActionProvider := CodeActionParams → Snapshot → RequestM (Array LazyCodeAction)
 deriving instance Inhabited for CodeActionProvider
 
-private builtin_initialize builtinCodeActionProviders : IO.Ref (NameMap CodeActionProvider) ←
-  IO.mkRef ∅
-
-def addBuiltinCodeActionProvider (decl : Name) (provider : CodeActionProvider) : IO Unit :=
-  builtinCodeActionProviders.modify (·.insert decl provider)
-
 builtin_initialize codeActionProviderExt : SimplePersistentEnvExtension Name NameSet ← registerSimplePersistentEnvExtension {
   addImportedFn := fun nss => nss.foldl (fun acc ns => ns.foldl NameSet.insert acc) ∅
   addEntryFn := fun s n => s.insert n
   toArrayFn  := fun es => es.toArray.qsort Name.quickLt
 }
 
-builtin_initialize
-  let mkAttr (builtin : Bool) (name : Name) := registerBuiltinAttribute {
-    name
-    descr           := (if builtin then "(builtin) " else "") ++
-      "Use to decorate methods for suggesting code actions. This is a low-level interface for making code actions."
-    applicationTime := .afterCompilation
-    add             := fun decl stx kind => do
-      Attribute.Builtin.ensureNoArgs stx
-      unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
-      unless (← getConstInfo decl).type.isConstOf ``CodeActionProvider do
-        throwError "invalid attribute '{name}', must be of type `Lean.Server.CodeActionProvider`"
-      let env ← getEnv
-      if builtin then
-        let h := mkConst decl
-        declareBuiltin decl <| mkApp (mkConst ``addBuiltinCodeActionProvider) h
-      else
-        setEnv <| codeActionProviderExt.addEntry env decl
-  }
-  mkAttr true `builtin_code_action_provider
-  mkAttr false `code_action_provider
+builtin_initialize registerBuiltinAttribute {
+  name := `code_action_provider
+  descr := "Use to decorate methods for suggesting code actions. This is a low-level interface for making code actions."
+  add := fun src _stx _kind => do
+    modifyEnv (codeActionProviderExt.addEntry · src)
+}
 
 private unsafe def evalCodeActionProviderUnsafe [MonadEnv M] [MonadOptions M] [MonadError M] [Monad M] (declName : Name) : M CodeActionProvider := do
   evalConstCheck CodeActionProvider ``CodeActionProvider declName
@@ -123,7 +103,7 @@ def handleCodeAction (params : CodeActionParams) : RequestM (RequestTask (Array
         let env ← getEnv
         let names := codeActionProviderExt.getState env |>.toArray
         let caps ← names.mapM evalCodeActionProvider
-        return (← builtinCodeActionProviders.get).toList.toArray ++ Array.zip names caps
+        return Array.zip names caps
       caps.concatMapM fun (providerName, cap) => do
         let cas ← cap params snap
         cas.mapIdxM fun i lca => do
@@ -151,9 +131,7 @@ def handleCodeActionResolve (param : CodeAction) : RequestM (RequestTask CodeAct
   withWaitFindSnap doc (fun s => s.endPos ≥ pos)
     (notFoundX := throw <| RequestError.internalError "snapshot not found")
     fun snap => do
-      let cap ← match (← builtinCodeActionProviders.get).find? data.providerName with
-        | some cap => pure cap
-        | none     => RequestM.runCoreM snap <| evalCodeActionProvider data.providerName
+      let cap ← RequestM.runCoreM snap <| evalCodeActionProvider data.providerName
       let cas ← cap data.params snap
       let some ca := cas[data.providerResultIndex]?
         | throw <| RequestError.internalError s!"Failed to resolve code action index {data.providerResultIndex}."

src/Lean/Syntax.lean

@@ -305,10 +305,6 @@ def getRange? (stx : Syntax) (canonicalOnly := false) : Option String.Range :=
   | some start, some stop => some { start, stop }
   | _,          _         => none
 
-/-- Returns a synthetic Syntax which has the specified `String.Range`. -/
-def ofRange (range : String.Range) (canonical := true) : Lean.Syntax :=
-  .atom (.synthetic range.start range.stop canonical) ""
-
 /--
 Represents a cursor into a syntax tree that can be read, written, and advanced down/up/left/right.
 Indices are allowed to be out-of-bound, in which case `cur` is `Syntax.missing`.

src/Lean/Widget/UserWidget.lean

@@ -56,11 +56,6 @@ class ToModule (α : Type u) where
 
 instance : ToModule Module := ⟨id⟩
 
-private builtin_initialize builtinModulesRef : IO.Ref (RBMap UInt64 Module compare) ← IO.mkRef ∅
-
-def addBuiltinModule (m : Module) : IO Unit :=
-  builtinModulesRef.modify (·.insert m.javascriptHash m)
-
 /-- Every constant `c : α` marked with `@[widget_module]` is registered here.
 The registry maps `hash (toModule c).javascript` to ``(`c, `(@toModule α inst c))``
 where `inst : ToModule α` is synthesized during registration time
@@ -76,38 +71,19 @@ builtin_initialize moduleRegistry : ModuleRegistry ←
     toArrayFn     := fun es => es.toArray
   }
 
-/--
-Registers `[builtin_widget_module]` and `[widget_module]` and binds the latter's implementation
-(used for creating the obsolete `[widget]` alias below).
- -/
-builtin_initialize widgetModuleAttrImpl : AttributeImpl ←
-  let mkAttr (builtin : Bool) (name : Name) := do
-    let impl := {
-      name
-      descr           := (if builtin then "(builtin) " else "") ++
-        "Registers a widget module. Its type must implement Lean.Widget.ToModule."
-      applicationTime := .afterCompilation
-      add             := fun decl stx kind => Prod.fst <$> MetaM.run do
-        Attribute.Builtin.ensureNoArgs stx
-        unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
-        let e ← mkAppM ``ToModule.toModule #[.const decl []]
-        let mod ← evalModule e
-        let env ← getEnv
-        if let some _ := (← builtinModulesRef.get).find? mod.javascriptHash then
-          logWarning m!"A builtin widget module with the same hash(JS source code) was already registered."
-        if let some (n, _) := moduleRegistry.getState env |>.find? mod.javascriptHash then
-          logWarning m!"A widget module with the same hash(JS source code) was already registered at {Expr.const n []}."
-        let env ← getEnv
-        if builtin then
-          let h := mkConst decl
-          declareBuiltin decl <| mkApp (mkConst ``addBuiltinModule) h
-        else
-          setEnv <| moduleRegistry.addEntry env (mod.javascriptHash, decl, e)
-    }
-    registerBuiltinAttribute impl
-    return impl
-  let _ ← mkAttr true `builtin_widget_module
-  mkAttr false `widget_module
+private def widgetModuleAttrImpl : AttributeImpl where
+  name := `widget_module
+  descr := "Registers a widget module. Its type must implement Lean.Widget.ToModule."
+  applicationTime := AttributeApplicationTime.afterCompilation
+  add decl _stx _kind := Prod.fst <$> MetaM.run do
+    let e ← mkAppM ``ToModule.toModule #[.const decl []]
+    let mod ← evalModule e
+    let env ← getEnv
+    if let some (n, _) := moduleRegistry.getState env |>.find? mod.javascriptHash then
+      logWarning m!"A widget module with the same hash(JS source code) was already registered at {Expr.const n []}."
+    setEnv <| moduleRegistry.addEntry env (mod.javascriptHash, decl, e)
+
+builtin_initialize registerBuiltinAttribute widgetModuleAttrImpl
 
 /-! ## Retrieval of widget modules -/
 
@@ -125,9 +101,6 @@ structure WidgetSource where
 open Server RequestM in
 @[server_rpc_method]
 def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask WidgetSource) := do
-  if let some m := (← builtinModulesRef.get).find? args.hash then
-    return .pure { sourcetext := m.javascript }
-
   let doc ← readDoc
   let pos := doc.meta.text.lspPosToUtf8Pos args.pos
   let notFound := throwThe RequestError ⟨.invalidParams, s!"No widget module with hash {args.hash} registered"⟩

src/runtime/object.cpp

@@ -1033,8 +1033,6 @@ extern "C" LEAN_EXPORT b_obj_res lean_io_wait_any_core(b_obj_arg task_list) {
     return g_task_manager->wait_any(task_list);
 }
 
-// Internally, a `Promise` is just a `Task` that is in the "Promised" or "Finished" state
-
 extern "C" LEAN_EXPORT obj_res lean_io_promise_new(obj_arg) {
     lean_always_assert(g_task_manager);
     bool keep_alive = false;
@@ -1052,11 +1050,6 @@ extern "C" LEAN_EXPORT obj_res lean_io_promise_resolve(obj_arg value, b_obj_arg
     return io_result_mk_ok(box(0));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_promise_result(obj_arg promise) {
-    // the task is the promise itself
-    return promise;
-}
-
 // =======================================
 // Natural numbers