chore: update stage0

closes #3279

src/Init/Tactics.lean

@@ -851,6 +851,12 @@ syntax (name := tacIfThenElse)
   ppRealGroup(ppRealFill(ppIndent("if " term " then") ppSpace matchRhsTacticSeq)
     ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic
 
+/--
+The tactic `nofun` is shorthand for `exact nofun`: it introduces the assumptions, then performs an
+empty pattern match, closing the goal if the introduced pattern is impossible.
+-/
+macro "nofun" : tactic => `(tactic| exact nofun)
+
 end Tactic
 
 namespace Attr

src/Lean/Elab/Match.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Mario Carneiro
 -/
 import Lean.Util.ForEachExprWhere
 import Lean.Meta.Match.Match
@@ -1262,4 +1262,14 @@ builtin_initialize
       withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
   | _ => throwUnsupportedSyntax
 
+@[builtin_term_elab «nofun»] def elabNoFun : TermElab := fun stx expectedType? => do
+  match stx with
+  | `($tk:nofun) =>
+    let expectedType ← waitExpectedType expectedType?
+    let binders ← forallTelescopeReducing expectedType fun args _ =>
+      args.mapM fun _ => withFreshMacroScope do `(a)
+    let stxNew ← `(fun%$tk $binders* => nomatch%$tk $binders,*)
+    withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Term

src/Lean/Parser/Term.lean

@@ -434,6 +434,8 @@ e.g. because it has no constructors.
 -/
 @[builtin_term_parser] def «nomatch» := leading_parser:leadPrec "nomatch " >> sepBy1 termParser ", "
 
+@[builtin_term_parser] def «nofun» := leading_parser "nofun"
+
 def funImplicitBinder := withAntiquot (mkAntiquot "implicitBinder" ``implicitBinder) <|
   atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder
 def funStrictImplicitBinder :=

tests/lean/run/nofun1.lean

@@ -0,0 +1,11 @@
+theorem Sum.inl_ne_inr : inl a ≠ inr b := nofun
+
+theorem Sum.inr_ne_inl : inr b ≠ inl a := nofun
+
+theorem Sum.inl_ne_inr' : inl a ≠ inr b := by nofun
+
+theorem Sum.inr_ne_inl' : inr b ≠ inl a := by nofun
+
+def f (a b : Bool) (_ : Sum.inr b ≠ Sum.inl a) : Nat := 0
+
+example : f true true nofun = 0 := rfl