fix: simp fails when custom discharger makes no progress

closes #2634

src/Init.lean

@@ -8,6 +8,7 @@ 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
@@ -24,5 +25,6 @@ import Init.NotationExtra
 import Init.SimpLemmas
 import Init.Hints
 import Init.Conv
+import Init.Guard
 import Init.Simproc
 import Init.SizeOfLemmas

src/Init/Coe.lean

@@ -290,6 +290,12 @@ 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,6 +666,8 @@ 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/String/Basic.lean

@@ -515,6 +515,12 @@ 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

@@ -0,0 +1,129 @@
+/-
+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

@@ -485,6 +485,13 @@ 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/RCases.lean

@@ -0,0 +1,192 @@
+/-
+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,11 +6,15 @@ Authors: Gabriel Ebner
 prelude
 import Init.System.IO
 
+set_option linter.missingDocs true
+
 namespace IO
 
-/-- 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 ⟨⟨_⟩⟩ => ⟨‹_›⟩⟩
+private opaque PromisePointed : NonemptyType.{0}
+
+private structure PromiseImpl (α : Type) : Type where
+  prom : PromisePointed.type
+  h    : Nonempty α
 
 /--
 `Promise α` allows you to create a `Task α` whose value is provided later by calling `resolve`.
@@ -26,10 +30,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 α).1
+def Promise (α : Type) : Type := PromiseImpl α
 
-instance [Nonempty α] : Nonempty (Promise α) :=
-  (PromiseImpl α).2.1 inferInstance
+instance [s : Nonempty α] : Nonempty (Promise α) :=
+  Nonempty.intro { prom := Classical.choice PromisePointed.property, h := s }
 
 /-- Creates a new `Promise`. -/
 @[extern "lean_io_promise_new"]
@@ -43,15 +47,12 @@ 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.
 -/
-@[implemented_by Promise.resultImpl]
+@[extern "lean_io_promise_result"]
 opaque Promise.result (promise : Promise α) : Task α :=
-  have : Nonempty α := (PromiseImpl α).2.2 ⟨promise⟩
+  have : Nonempty α := promise.h
   Classical.choice inferInstance

src/Init/Tactics.lean

@@ -323,9 +323,14 @@ 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).
@@ -432,13 +437,17 @@ 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.
@@ -857,6 +866,12 @@ 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,*)
+
 end Tactic
 
 namespace Attr

src/Lean/Data/Position.lean

@@ -84,6 +84,26 @@ 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,6 +722,8 @@ 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,12 +1,14 @@
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Gabriel Ebner
 -/
 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
@@ -19,6 +21,20 @@ 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
@@ -411,4 +427,33 @@ 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/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

@@ -1243,6 +1243,12 @@ builtin_initialize
     let discrs := discrs.getElems
     if (← discrs.allM fun discr => isAtomicDiscr discr.raw) 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
     else

src/Lean/Elab/SyntheticMVars.lean

@@ -293,8 +293,10 @@ mutual
   Try to synthesize a term `val` using the tactic code `tacticCode`, and then assign `mvarId := val`.
 
   The `tacticCode` syntax comprises the whole `by ...` expression.
+
+  If `report := false`, then `runTactic` will not capture exceptions nor will report unsolved goals. Unsolved goals become exceptions.
   -/
-  partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := withoutAutoBoundImplicit do
+  partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) (report := true) : TermElabM Unit := withoutAutoBoundImplicit do
     let code := tacticCode[1]
     instantiateMVarDeclMVars mvarId
     /-
@@ -320,9 +322,12 @@ mutual
             evalTactic code
         synthesizeSyntheticMVars (mayPostpone := false)
       unless remainingGoals.isEmpty do
-        reportUnsolvedGoals remainingGoals
+        if report then
+          reportUnsolvedGoals remainingGoals
+        else
+          throwError "unsolved goals\n{goalsToMessageData remainingGoals}"
     catch ex =>
-      if (← read).errToSorry then
+      if report && (← read).errToSorry then
         for mvarId in (← getMVars (mkMVar mvarId)) do
           mvarId.admit
         logException ex

src/Lean/Elab/Tactic.lean

@@ -23,3 +23,5 @@ 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

src/Lean/Elab/Tactic/Guard.lean

@@ -0,0 +1,158 @@
+/-
+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

@@ -0,0 +1,580 @@
+/-
+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/Simp.lean

@@ -43,9 +43,11 @@ def tacticToDischarge (tacticCode : Syntax) : TacticM (IO.Ref Term.State × Simp
     let runTac? : TermElabM (Option Expr) :=
       try
         /- We must only save messages and info tree changes. Recall that `simp` uses temporary metavariables (`withNewMCtxDepth`).
-           So, we must not save references to them at `Term.State`. -/
+           So, we must not save references to them at `Term.State`.
+        -/
         withoutModifyingStateWithInfoAndMessages do
-          Term.withSynthesize (mayPostpone := false) <| Term.runTactic mvar.mvarId! tacticCode
+          Term.withSynthesize (mayPostpone := false) do
+            Term.runTactic (report := false) mvar.mvarId! tacticCode
           let result ← instantiateMVars mvar
           if result.hasExprMVar then
             return none
@@ -72,6 +74,7 @@ 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
@@ -258,8 +261,15 @@ 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) : TacticM MkSimpContextResult := do
+def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
+    (ignoreStarArg : Bool := false) (simpTheorems : CoreM SimpTheorems := getSimpTheorems) :
+    TacticM MkSimpContextResult := do
   if !stx[2].isNone then
     if kind == SimpKind.simpAll then
       throwError "'simp_all' tactic does not support 'discharger' option"
@@ -270,7 +280,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ig
   let simpTheorems ← if simpOnly then
     simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
   else
-    getSimpTheorems
+    simpTheorems
   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/Meta.lean

@@ -43,3 +43,4 @@ 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

@@ -0,0 +1,86 @@
+/-
+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

@@ -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⟩, *, *, ⟨a,0⟩, ⟨b,0⟩
+  ⟨Add.add, 4⟩, α, *, *, *
+  ⟨Add.add, 4⟩, Nat, *, ⟨a,0⟩, ⟨b,0⟩
   ```
 
   That is, we don't reduce `Add.add Nat inst a b` into `Nat.add a b`.

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
+Authors: Leonardo de Moura, Mario Carneiro
 -/
 import Lean.Data.AssocList
 import Lean.Expr
@@ -63,6 +63,13 @@ 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/MetavarContext.lean

@@ -393,6 +393,18 @@ 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
@@ -483,6 +495,10 @@ 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 } }
 
@@ -809,6 +825,20 @@ 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 } }
@@ -840,6 +870,35 @@ 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
 
@@ -1377,4 +1436,46 @@ 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/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
+Authors: Leonardo de Moura, Sebastian Ullrich, Mario Carneiro
 -/
 import Lean.Parser.Attr
 import Lean.Parser.Level
@@ -601,6 +601,19 @@ 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
+Authors: Sebastian Ullrich, Leonardo de Moura, Gabriel Ebner, Mario Carneiro
 -/
-
+import Lean.Parser
 import Lean.PrettyPrinter.Delaborator.Basic
 import Lean.PrettyPrinter.Delaborator.SubExpr
 import Lean.PrettyPrinter.Delaborator.TopDownAnalyze
-import Lean.Parser
+import Lean.Meta.CoeAttr
 
 namespace Lean.PrettyPrinter.Delaborator
 open Lean.Meta
@@ -315,7 +315,8 @@ Default delaborator for applications.
 -/
 @[builtin_delab app]
 def delabApp : Delab := do
-  delabAppCore (← getExpr).getAppNumArgs delabAppFn
+  let e ← getExpr
+  delabAppCore e.getAppNumArgs delabAppFn
 
 /--
 The `withOverApp` combinator allows delaborators to handle "over-application" by using the core
@@ -810,6 +811,27 @@ 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,18 +68,38 @@ 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 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)
-}
+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
 
 private unsafe def evalCodeActionProviderUnsafe [MonadEnv M] [MonadOptions M] [MonadError M] [Monad M] (declName : Name) : M CodeActionProvider := do
   evalConstCheck CodeActionProvider ``CodeActionProvider declName
@@ -103,7 +123,7 @@ def handleCodeAction (params : CodeActionParams) : RequestM (RequestTask (Array
         let env ← getEnv
         let names := codeActionProviderExt.getState env |>.toArray
         let caps ← names.mapM evalCodeActionProvider
-        return Array.zip names caps
+        return (← builtinCodeActionProviders.get).toList.toArray ++ Array.zip names caps
       caps.concatMapM fun (providerName, cap) => do
         let cas ← cap params snap
         cas.mapIdxM fun i lca => do
@@ -131,7 +151,9 @@ 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 ← RequestM.runCoreM snap <| evalCodeActionProvider data.providerName
+      let cap ← match (← builtinCodeActionProviders.get).find? data.providerName with
+        | some cap => pure cap
+        | none     => 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,6 +305,10 @@ 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,6 +56,11 @@ 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
@@ -71,19 +76,38 @@ builtin_initialize moduleRegistry : ModuleRegistry ←
     toArrayFn     := fun es => es.toArray
   }
 
-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
+/--
+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
 
 /-! ## Retrieval of widget modules -/
 
@@ -101,6 +125,9 @@ 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,6 +1033,8 @@ 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;
@@ -1050,6 +1052,11 @@ 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
 

tests/lean/1021.lean.expected.out

@@ -1,8 +1,8 @@
-some { range := { pos := { line := 175, column := 42 },
+some { range := { pos := { line := 191, column := 42 },
              charUtf16 := 42,
-             endPos := { line := 181, column := 31 },
+             endPos := { line := 197, column := 31 },
              endCharUtf16 := 31 },
-  selectionRange := { pos := { line := 175, column := 46 },
+  selectionRange := { pos := { line := 191, column := 46 },
                       charUtf16 := 46,
-                      endPos := { line := 175, column := 58 },
+                      endPos := { line := 191, column := 58 },
                       endCharUtf16 := 58 } }

tests/lean/2634.lean

@@ -0,0 +1,17 @@
+example
+  {p: Prop}
+  (h: True → p)
+  : p := by
+  simp (discharger := skip) [h] -- simp made no progress
+
+example
+  {p: Prop}
+  (h: True → p)
+  : p := by
+  simp (discharger := simp) [h]
+
+example
+  {p: Prop}
+  (h: True → p)
+  : p := by
+  simp (discharger := trace "hello"; simp) [h]

tests/lean/2634.lean.expected.out

@@ -0,0 +1,2 @@
+2634.lean:5:2-5:31: error: simp made no progress
+hello

tests/lean/coe.lean

@@ -0,0 +1,53 @@
+import Lean
+
+structure WrappedNat where
+  val : Nat
+
+structure WrappedFun (α) where
+  fn : Nat → α
+
+structure WrappedType where
+  typ : Type
+
+attribute [coe] WrappedNat.val
+instance : Coe WrappedNat Nat where coe := WrappedNat.val
+
+#eval Lean.Meta.registerCoercion ``WrappedFun.fn (some ⟨2, 1, .coeFun⟩)
+instance : CoeFun (WrappedFun α) (fun _ => Nat → α) where coe := WrappedFun.fn
+
+#eval Lean.Meta.registerCoercion ``WrappedType.typ (some ⟨1, 0, .coeSort⟩)
+instance : CoeSort WrappedType Type where coe := WrappedType.typ
+
+section coe
+variable (n : WrappedNat)
+
+#check (↑n : Nat)
+
+#check n.val
+
+end coe
+
+section coeFun
+variable (f : WrappedFun Nat) (g : Nat → WrappedFun Nat) (h : WrappedFun (WrappedFun Nat))
+
+#check f.fn
+
+#check ⇑f
+
+#check ⇑f 1
+
+#check ⇑(g 1)
+
+#check g 1 2
+
+#check ⇑h
+
+end coeFun
+
+section coeSort
+variable (t : WrappedType)
+
+#check t.typ
+#check ↥t
+
+end coeSort

tests/lean/coe.lean.expected.out

@@ -0,0 +1,12 @@
+
+
+↑n : Nat
+↑n : Nat
+⇑f : Nat → Nat
+⇑f : Nat → Nat
+f 1 : Nat
+⇑(g 1) : Nat → Nat
+(g 1) 2 : Nat
+⇑h : Nat → WrappedFun Nat
+↥t : Type
+↥t : Type

tests/lean/coeAttr1.lean

@@ -0,0 +1,11 @@
+@[coe] def f (n : Nat) : String :=
+  toString n
+
+#check f 10
+
+instance : Coe Nat String where
+  coe := f
+
+def g (n : String) := n
+
+#check fun x : Nat => g x

tests/lean/coeAttr1.lean.expected.out

@@ -0,0 +1,2 @@
+↑10 : String
+fun x => g ↑x : Nat → String

tests/lean/docStr.lean

@@ -102,3 +102,6 @@ def printRangesTest : MetaM Unit := do
   printRanges `g.foo
 
 #eval printRangesTest
+
+/-- no dice -/
+add_decl_doc Nat.add

tests/lean/docStr.lean.expected.out

@@ -189,3 +189,4 @@ g.foo :=
                         charUtf16 := 44,
                         endPos := { line := 42, column := 47 },
                         endCharUtf16 := 47 } }
+docStr.lean:106:0-107:20: error: invalid 'add_decl_doc', declaration is in an imported module

tests/lean/run/1842.lean

@@ -9,7 +9,6 @@ theorem and_assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
 
 theorem and_left_comm : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) := by
   rw [← and_assoc, ← and_assoc, @And.comm a b]
-  exact Iff.rfl
 
 theorem pairwise_append {l₁ l₂ : List α} :
     (l₁ ++ l₂).Pairwise R ↔ l₁.Pairwise R ∧ l₂.Pairwise R ∧ ∀ {a} (_ : a ∈ l₁), ∀ {b} (_ : b ∈ l₂), R a b := by

tests/lean/run/deq.lean

@@ -27,8 +27,8 @@ theorem deq_correct_2 (Q : LazyList τ)
   : deq Q = none ↔ Q.force = none
   := by
     cases h' : Q.force with
-    | none => unfold deq; rw [h']; simp
-    | some => unfold deq; rw [h']; simp
+    | none => unfold deq; rw [h']
+    | some => unfold deq; rw [h']
 
 theorem deq_correct_3 (Q : LazyList τ)
   : deq Q = none ↔ Q.force = none

tests/lean/run/guardexpr.lean

@@ -0,0 +1,57 @@
+example (n : Nat) : Nat := by
+  guard_hyp n :ₛ Nat
+  let m : Nat := 1
+  guard_expr 1 =ₛ (by exact 1)
+  fail_if_success guard_expr 1 = (by exact 2)
+  guard_hyp m := 1
+  guard_hyp m : (fun x => x) Nat :=~ id 1
+  guard_target = Nat
+  have : 1 = 1 := by conv =>
+    guard_hyp m := 1
+    guard_expr ‹Nat› = m
+    fail_if_success guard_target = 1
+    lhs
+    guard_target = 1
+  exact 0
+
+-- Now with a generic type to test that default instances work correctly
+example [∀ n, OfNat α n] (n : α) : α := by
+  guard_hyp n
+  fail_if_success guard_hyp m
+  guard_hyp n :ₛ α
+  let q : α := 1
+  guard_expr (1 : α) =ₛ 1
+  fail_if_success guard_expr 1 =ₛ (2 : α)
+  fail_if_success guard_expr 1 =ₛ (by exact (2 : α))
+  guard_hyp q := 1
+  guard_hyp q : α := 1
+  guard_hyp q : (fun x => x) α :=~ id 1
+  guard_target = α
+  have : (1 : α) = 1 := by conv =>
+    guard_hyp q := 1
+    guard_expr ‹α› = q
+    fail_if_success guard_target = 1
+    lhs
+    guard_target = 1
+  exact 0
+
+#guard_expr 1 = 1
+#guard_expr 1 =ₛ 1
+#guard_expr 2 = 1 + 1
+
+section
+variable {α : Type} [∀ n, OfNat α n]
+#guard_expr (1 : α) = 1
+end
+
+#guard true
+#guard 2 == 1 + 1
+#guard 2 = 1 + 1
+
+instance (p : Bool → Prop) [DecidablePred p] : Decidable (∀ b, p b) :=
+  if h : p false ∧ p true then
+    isTrue (by { intro b; cases h; cases b <;> assumption })
+  else
+    isFalse (by { intro h'; simp [h'] at h })
+
+#guard ∀ (b : Bool), b = !!b

tests/lean/run/nomatch_regression.lean

@@ -0,0 +1,220 @@
+inductive RBColor where
+  | red
+  | black
+
+inductive RBNode (α : Type u) where
+  | nil
+  | node (c : RBColor) (l : RBNode α) (v : α) (r : RBNode α)
+
+namespace RBNode
+open RBColor
+
+inductive Balanced : RBNode α → RBColor → Nat → Prop where
+  | protected nil : Balanced nil black 0
+  | protected red : Balanced x black n → Balanced y black n → Balanced (node red x v y) red n
+  | protected black : Balanced x c₁ n → Balanced y c₂ n → Balanced (node black x v y) black (n + 1)
+
+@[inline] def balance1 : RBNode α → α → RBNode α → RBNode α
+  | node red (node red a x b) y c, z, d
+  | node red a x (node red b y c), z, d => node red (node black a x b) y (node black c z d)
+  | a,                             x, b => node black a x b
+
+@[inline] def balance2 : RBNode α → α → RBNode α → RBNode α
+  | a, x, node red (node red b y c) z d
+  | a, x, node red b y (node red c z d) => node red (node black a x b) y (node black c z d)
+  | a, x, b                             => node black a x b
+
+theorem balance1_eq {l : RBNode α} {v : α} {r : RBNode α}
+    (hl : l.Balanced c n) : balance1 l v r = node black l v r := by
+  unfold balance1; split <;> first | rfl | exact nomatch hl
+
+@[inline] def isBlack : RBNode α → RBColor
+  | node c .. => c
+  | _         => red
+
+def setRed : RBNode α → RBNode α
+  | node _ a v b => node red a v b
+  | nil          => nil
+
+def balLeft (l : RBNode α) (v : α) (r : RBNode α) : RBNode α :=
+  match l with
+  | node red a x b                    => node red (node black a x b) v r
+  | l => match r with
+    | node black a y b                => balance2 l v (node red a y b)
+    | node red (node black a y b) z c => node red (node black l v a) y (balance2 b z (setRed c))
+    | r                               => node red l v r -- unreachable
+
+def balRight (l : RBNode α) (v : α) (r : RBNode α) : RBNode α :=
+  match r with
+  | node red b y c                    => node red l v (node black b y c)
+  | r => match l with
+    | node black a x b                => balance1 (node red a x b) v r
+    | node red a x (node black b y c) => node red (balance1 (setRed a) x b) y (node black c v r)
+    | l                               => node red l v r -- unreachable
+
+@[simp] def size : RBNode α → Nat
+  | nil => 0
+  | node _ x _ y => x.size + y.size + 1
+
+def append : RBNode α → RBNode α → RBNode α
+  | nil, x | x, nil => x
+  | node red a x b, node red c y d =>
+    match append b c with
+    | node red b' z c' => node red (node red a x b') z (node red c' y d)
+    | bc               => node red a x (node red bc y d)
+  | node black a x b, node black c y d =>
+    match append b c with
+    | node red b' z c' => node red (node black a x b') z (node black c' y d)
+    | bc               => balLeft a x (node black bc y d)
+  | a@(node black ..), node red b x c => node red (append a b) x c
+  | node red a x b, c@(node black ..) => node red a x (append b c)
+termination_by x y => x.size + y.size
+
+def del (cut : α → Ordering) : RBNode α → RBNode α
+  | nil          => nil
+  | node _ a y b =>
+    match cut y with
+    | .lt => match a.isBlack with
+      | black => balLeft (del cut a) y b
+      | red => node red (del cut a) y b
+    | .gt => match b.isBlack with
+      | black => balRight a y (del cut b)
+      | red => node red a y (del cut b)
+    | .eq => append a b
+
+inductive RedRed (p : Prop) : RBNode α → Nat → Prop where
+  | balanced : Balanced t c n → RedRed p t n
+  | redred : p → Balanced a c₁ n → Balanced b c₂ n → RedRed p (node red a x b) n
+
+def DelProp (p : RBColor) (t : RBNode α) (n : Nat) : Prop :=
+  match p with
+  | black => ∃ n', n = n' + 1 ∧ RedRed True t n'
+  | red => ∃ c, Balanced t c n
+
+protected theorem RedRed.of_red : RedRed p (node red a x b) n →
+    ∃ c₁ c₂, Balanced a c₁ n ∧ Balanced b c₂ n
+  | .balanced (.red ha hb) | .redred _ ha hb => ⟨_, _, ha, hb⟩
+
+protected theorem RedRed.balance2 {l : RBNode α} {v : α} {r : RBNode α}
+    (hl : l.Balanced c n) (hr : r.RedRed p n) : ∃ c, (balance2 l v r).Balanced c (n + 1) := by
+  unfold balance2; split
+  · have .redred _ (.red ha hb) hc := hr; exact ⟨_, .red (.black hl ha) (.black hb hc)⟩
+  · have .redred _ ha (.red hb hc) := hr; exact ⟨_, .red (.black hl ha) (.black hb hc)⟩
+  · next H1 H2 => match hr with
+    | .balanced hr => exact ⟨_, .black hl hr⟩
+    | .redred _ (c₁ := black) (c₂ := black) ha hb => exact ⟨_, .black hl (.red ha hb)⟩
+    | .redred _ (c₁ := red) (.red ..) _ => cases H1 _ _ _ _ _ rfl
+    | .redred _ (c₂ := red) _ (.red ..) => cases H2 _ _ _ _ _ rfl
+
+protected theorem RedRed.balance1 {l : RBNode α} {v : α} {r : RBNode α}
+    (hl : l.RedRed p n) (hr : r.Balanced c n) : ∃ c, (balance1 l v r).Balanced c (n + 1) := by
+  unfold balance1; split
+  · have .redred _ (.red ha hb) hc := hl; exact ⟨_, .red (.black ha hb) (.black hc hr)⟩
+  · have .redred _ ha (.red hb hc) := hl; exact ⟨_, .red (.black ha hb) (.black hc hr)⟩
+  · next H1 H2 => match hl with
+    | .balanced hl => exact ⟨_, .black hl hr⟩
+    | .redred _ (c₁ := black) (c₂ := black) ha hb => exact ⟨_, .black (.red ha hb) hr⟩
+    | .redred _ (c₁ := red) (.red ..) _ => cases H1 _ _ _ _ _ rfl
+    | .redred _ (c₂ := red) _ (.red ..) => cases H2 _ _ _ _ _ rfl
+
+protected theorem Balanced.balRight (hl : l.Balanced cl (n + 1)) (hr : r.RedRed True n) :
+    (balRight l v r).RedRed (cl = red) (n + 1) := by
+  unfold balRight; split
+  · next b y c => exact
+    let ⟨cb, cc, hb, hc⟩ := hr.of_red
+    match cl with
+    | red => .redred rfl hl (.black hb hc)
+    | black => .balanced (.red hl (.black hb hc))
+  · next H => exact match hr with
+    | .redred .. => nomatch H _ _ _ rfl
+    | .balanced hr => match hl with
+      | .black hb hc =>
+        let ⟨c, h⟩ := RedRed.balance1 (.redred trivial hb hc) hr; .balanced h
+      | .red (.black ha hb) (.black hc hd) =>
+        let ⟨c, h⟩ := RedRed.balance1 (.redred trivial ha hb) hc; .redred rfl h (.black hd hr)
+
+protected theorem Balanced.balLeft (hl : l.RedRed True n) (hr : r.Balanced cr (n + 1)) :
+    (balLeft l v r).RedRed (cr = red) (n + 1) := by
+  unfold balLeft; split
+  · next a x b => exact
+    let ⟨ca, cb, ha, hb⟩ := hl.of_red
+    match cr with
+    | red => .redred rfl (.black ha hb) hr
+    | black => .balanced (.red (.black ha hb) hr)
+  · next H => exact match hl with
+    | .redred .. => nomatch H _ _ _ rfl
+    | .balanced hl => match hr with
+      | .black ha hb =>
+        let ⟨c, h⟩ := RedRed.balance2 hl (.redred trivial ha hb); .balanced h
+      | .red (.black ha hb) (.black hc hd) =>
+        let ⟨c, h⟩ := RedRed.balance2 hb (.redred trivial hc hd); .redred rfl (.black hl ha) h
+
+protected theorem RedRed.imp (h : p → q) : RedRed p t n → RedRed q t n
+  | .balanced h => .balanced h
+  | .redred hp ha hb => .redred (h hp) ha hb
+
+protected theorem RedRed.of_false (h : ¬p) : RedRed p t n → ∃ c, Balanced t c n
+  | .balanced h => ⟨_, h⟩
+  | .redred hp .. => nomatch h hp
+
+protected theorem Balanced.append {l r : RBNode α}
+    (hl : l.Balanced c₁ n) (hr : r.Balanced c₂ n) :
+    (l.append r).RedRed (c₁ = black → c₂ ≠ black) n := by
+  unfold append; split
+  · exact .balanced hr
+  · exact .balanced hl
+  · next b c _ _ =>
+    have .red ha hb := hl; have .red hc hd := hr
+    have ⟨_, IH⟩ := (hb.append hc).of_false (· rfl rfl); split
+    · next e =>
+      have .red hb' hc' := e ▸ IH
+      exact .redred (nofun) (.red ha hb') (.red hc' hd)
+    · next bcc _ H =>
+      match bcc, append b c, IH, H with
+      | black, _, IH, _ => exact .redred (nofun) ha (.red IH hd)
+      | red, _, .red .., H => cases H _ _ _ rfl
+  · next b c _ _ =>
+    have .black ha hb := hl; have .black hc hd := hr
+    have IH := hb.append hc; split
+    · next e => match e ▸ IH with
+      | .balanced (.red hb' hc') | .redred _ hb' hc' =>
+        exact .balanced (.red (.black ha hb') (.black hc' hd))
+    · next H =>
+      match append b c, IH, H with
+      | bc, .balanced hbc, _ =>
+        unfold balLeft; split
+        · have .red ha' hb' := ha
+          exact .balanced (.red (.black ha' hb') (.black hbc hd))
+        · exact have ⟨c, h⟩ := RedRed.balance2 ha (.redred trivial hbc hd); .balanced h
+      | _, .redred .., H => cases H _ _ _ rfl
+  · have .red hc hd := hr; have IH := hl.append hc
+    have .black ha hb := hl; have ⟨c, IH⟩ := IH.of_false (· rfl rfl)
+    exact .redred (nofun) IH hd
+  · have .red ha hb := hl; have IH := hb.append hr
+    have .black hc hd := hr; have ⟨c, IH⟩ := IH.of_false (· rfl rfl)
+    exact .redred (nofun) ha IH
+termination_by l.size + r.size
+
+protected theorem Balanced.del {t : RBNode α} (h : t.Balanced c n) :
+    (t.del cut).DelProp t.isBlack n := by
+  induction h with
+  | nil => exact ⟨_, .nil⟩
+  | @black a _ n b _ _ ha hb iha ihb =>
+    refine ⟨_, rfl, ?_⟩
+    unfold del; split
+    · exact match a, n, iha with
+      | .nil, _, ⟨c, ha⟩ | .node red .., _, ⟨c, ha⟩ => .redred ⟨⟩ ha hb
+      | .node black .., _, ⟨n, rfl, ha⟩ => (hb.balLeft ha).imp fun _ => ⟨⟩
+    · exact match b, n, ihb with
+      | .nil, _, ⟨c, hb⟩ | .node .red .., _, ⟨c, hb⟩ => .redred ⟨⟩ ha hb
+      | .node black .., _, ⟨n, rfl, hb⟩ => (ha.balRight hb).imp fun _ => ⟨⟩
+    · exact (ha.append hb).imp fun _ => ⟨⟩
+  | @red a n b _ ha hb iha ihb =>
+    unfold del; split
+    · exact match a, n, iha with
+      | .nil, _, _ => ⟨_, .red ha hb⟩
+      | .node black .., _, ⟨n, rfl, ha⟩ => (hb.balLeft ha).of_false nofun
+    · exact match b, n, ihb with
+      | .nil, _, _ => ⟨_, .red ha hb⟩
+      | .node black .., _, ⟨n, rfl, hb⟩ => (ha.balRight hb).of_false nofun
+    · exact (ha.append hb).of_false (· rfl rfl)

tests/lean/run/nomatch_tac.lean

@@ -0,0 +1,5 @@
+example (h : Empty) : False := by
+  nomatch h
+
+example (x : Nat) (f : Nat → Fin n) (h : n = 0 ∧ True) : False := by
+  nomatch f x, h.1

tests/lean/run/rcases1.lean

@@ -0,0 +1,71 @@
+example (x : α × β × γ) : True := by
+  rcases x with ⟨a, b, c⟩
+  trivial
+
+example (x : α × β × γ) : True := by
+  rcases x with ⟨(a : α) : id α, -, c : id γ⟩
+  fail_if_success have : β := by assumption
+  trivial
+
+example (x : (α × β) × γ) : True := by
+  fail_if_success rcases x with ⟨_a, b, c⟩
+  fail_if_success rcases x with ⟨⟨a:β, b⟩, c⟩
+  rcases x with ⟨⟨a:α, b⟩, c⟩
+  trivial
+
+example : @Inhabited.{1} α × Option β ⊕ γ → True := by
+  rintro (⟨⟨a⟩, _ | b⟩ | c)
+  · trivial
+  · trivial
+  · trivial
+
+example : cond false Nat Int → cond true Int Nat → Nat ⊕ Unit → True := by
+  rintro (x y : Int) (z | u)
+  · trivial
+  · trivial
+
+example (h : x = 3) (h₂ : x < 4) : x < 4 := by
+  rcases h with ⟨⟩
+  exact h₂
+
+example : True := by
+  obtain (h : True) | ⟨⟨⟩⟩ : True ∨ False
+  · exact Or.inl trivial
+  trivial
+
+example : True := by
+  obtain h | ⟨⟨⟩⟩ : True ∨ False := Or.inl trivial
+  trivial
+
+example : True := by
+  obtain ⟨h, h2⟩ := And.intro trivial trivial
+  trivial
+
+example : True := by
+  fail_if_success obtain ⟨h, h2⟩
+  trivial
+
+example (x y : α × β) : True := by
+  rcases x, y with ⟨⟨a, b⟩, c, d⟩
+  trivial
+
+example (x y : α ⊕ β) : True := by
+  rcases x, y with ⟨a|b, c|d⟩
+  repeat trivial
+
+example (i j : Nat) : (Σ' x, i ≤ x ∧ x ≤ j) → i ≤ j := by
+  intro h
+  rcases h' : h with ⟨x, h₀, h₁⟩
+  apply Nat.le_trans h₀ h₁
+
+example (x : Quot fun _ _ : α => True) (h : x = x): x = x := by
+  rcases x with ⟨z⟩
+  exact h
+
+example (n : Nat) : True := by
+  obtain _one_lt_n | _n_le_one : 1 < n + 1 ∨ n + 1 ≤ 1 := Nat.lt_or_ge 1 (n + 1)
+  {trivial}; trivial
+
+example (n : Nat) : True := by
+  obtain _one_lt_n | (_n_le_one : n + 1 ≤ 1) := Nat.lt_or_ge 1 (n + 1)
+  {trivial}; trivial

tests/lean/run/rw_inst_mvars.lean

@@ -1,6 +1,4 @@
 example  (p : Nat → Prop) (h : ∀ n, p (n+1) = p n) : (p m ↔ p 0) := by
   induction m
-  case succ ih =>
-    rw [h, ih]
-    exact Iff.rfl
+  case succ ih => rw [h, ih]
   case zero => exact Iff.rfl

tests/lean/run/sharecommon.lean

@@ -2,7 +2,7 @@ import Lean.Util.ShareCommon
 
 open Lean.ShareCommon
 def check (b : Bool) : ShareCommonT IO Unit := do
-unless b do throw $ IO.userError "check failed"
+  unless b do throw $ IO.userError "check failed"
 
 unsafe def tst1 : ShareCommonT IO Unit := do
 let x := [1]

tests/lean/run/unsafeTerm.lean

@@ -0,0 +1,3 @@
+def cool :=
+  unsafe (unsafeCast () : Nat)
+#eval cool

tests/lean/runTacticMustCatchExceptions.lean.expected.out

@@ -1,27 +1,36 @@
-runTacticMustCatchExceptions.lean:2:25-2:28: error: tactic 'rfl' failed, equality expected
-  Nat.le 1 (a + b)
-a b : Nat
-⊢ 1 ≤ a + b
-runTacticMustCatchExceptions.lean:3:25-3:28: error: tactic 'rfl' failed, equality expected
-  Nat.le (a + b) b
-a b : Nat
-this : 1 ≤ a + b
-⊢ a + b ≤ b
-runTacticMustCatchExceptions.lean:4:25-4:28: error: tactic 'rfl' failed, equality expected
-  Nat.le b 2
-a b : Nat
-this✝ : 1 ≤ a + b
-this : a + b ≤ b
-⊢ b ≤ 2
-runTacticMustCatchExceptions.lean:9:18-9:21: error: tactic 'rfl' failed, equality expected
-  Nat.le 1 (a + b)
-a b : Nat
-⊢ 1 ≤ a + b
-runTacticMustCatchExceptions.lean:10:14-10:17: error: tactic 'rfl' failed, equality expected
-  Nat.le (a + b) b
-a b : Nat
-⊢ a + b ≤ b
-runTacticMustCatchExceptions.lean:11:14-11:17: error: tactic 'rfl' failed, equality expected
-  Nat.le b 2
-a b : Nat
-⊢ b ≤ 2
+runTacticMustCatchExceptions.lean:2:25-2:28: error: type mismatch
+  Iff.rfl
+has type
+  ?m ↔ ?m : Prop
+but is expected to have type
+  1 ≤ a + b : Prop
+runTacticMustCatchExceptions.lean:3:25-3:28: error: type mismatch
+  Iff.rfl
+has type
+  ?m ↔ ?m : Prop
+but is expected to have type
+  a + b ≤ b : Prop
+runTacticMustCatchExceptions.lean:4:25-4:28: error: type mismatch
+  Iff.rfl
+has type
+  ?m ↔ ?m : Prop
+but is expected to have type
+  b ≤ 2 : Prop
+runTacticMustCatchExceptions.lean:9:18-9:21: error: type mismatch
+  Iff.rfl
+has type
+  ?m ↔ ?m : Prop
+but is expected to have type
+  1 ≤ a + b : Prop
+runTacticMustCatchExceptions.lean:10:14-10:17: error: type mismatch
+  Iff.rfl
+has type
+  ?m ↔ ?m : Prop
+but is expected to have type
+  a + b ≤ b : Prop
+runTacticMustCatchExceptions.lean:11:14-11:17: error: type mismatch
+  Iff.rfl
+has type
+  ?m ↔ ?m : Prop
+but is expected to have type
+  b ≤ 2 : Prop

tests/lean/univInference.lean.expected.out

@@ -4,7 +4,7 @@ structure resulting type
   Type ?u
 recall that Lean only infers the resulting universe level automatically when there is a unique solution for the universe level constraints, consider explicitly providing the structure resulting universe level
 S6 : Sort (max w₁ w₂) → Type w₂ → Sort (max w₁ (w₂ + 1))
-univInference.lean:45:0-46:17: error: 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'
+univInference.lean:45:0-46:17: error: 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')
   max u v
 univInference.lean:65:2-65:22: error: failed to compute resulting universe level of inductive datatype, constructor 'Induct.S4.mk' has type
   {α : Sort u} → {β : Sort v} → α → β → S4 α β
@@ -13,7 +13,7 @@ parameter 'a' has type
 inductive type resulting type
   Type ?u
 recall that Lean only infers the resulting universe level automatically when there is a unique solution for the universe level constraints, consider explicitly providing the inductive type resulting universe level
-univInference.lean:73:0-74:22: error: 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'
+univInference.lean:73:0-74:22: error: 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')
   max u v
-univInference.lean:81:0-82:22: error: 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'
+univInference.lean:81:0-82:22: error: 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')
   max u v