feat(library/init): use new "empty match" syntax

lean4-mode/lean4-syntax.el

@@ -14,7 +14,7 @@
     "open" "export" "axiom" "inductive" "coinductive" "with" "without"
     "structure" "universe" "universes" "hide"
     "precedence" "reserve"
-    "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "instance"
+    "match" "nomatch" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "instance"
     "end" "this" "using" "using_well_founded" "namespace" "section"
     "attribute" "local" "set_option" "extends" "include" "omit" "classes" "class"
     "attributes" "raw" "replacing"

library/init/control/estate.lean

@@ -23,7 +23,7 @@ inductive Result.IsOk : Result ε σ α → Prop
 | mk (a : α) (s : σ) : Result.IsOk (Result.ok a s)
 
 theorem notIsOkError {e : ε} {s : σ} (h : @Result.IsOk _ _ α (Result.error e s)) : False :=
-match h with end
+nomatch h
 
 @[inline] def unreachableError {β : Type v} {e : ε} {s : σ} (h : @Result.IsOk _ _ α (Result.error e s)) : β :=
 False.elim (notIsOkError h)

library/init/data/int/basic.lean

@@ -98,7 +98,7 @@ instance Int.DecidableEq : DecidableEq Int :=
 private def decNonneg (m : @& Int) : Decidable (NonNeg m) :=
 match m with
 | ofNat m   => isTrue $ NonNeg.mk m
-| negSucc m => isFalse $ fun h => match h with end
+| negSucc m => isFalse $ fun h => nomatch h
 
 @[extern cpp "lean::int_dec_le"]
 instance decLe (a b : @& Int) : Decidable (a ≤ b) :=

library/init/data/list/basic.lean

@@ -301,9 +301,9 @@ instance [HasLess α] : HasLess (List α) :=
 ⟨List.Less⟩
 
 instance hasDecidableLt [HasLess α] [h : DecidableRel HasLess.Less] : ∀ (l₁ l₂ : List α), Decidable (l₁ < l₂)
-| []      []      := isFalse (fun h => match h with end)
+| []      []      := isFalse (fun h => nomatch h)
 | []      (b::bs) := isTrue (Less.nil _ _)
-| (a::as) []      := isFalse (fun h => match h with end)
+| (a::as) []      := isFalse (fun h => nomatch h)
 | (a::as) (b::bs) :=
   match h a b with
   | isTrue h₁  => isTrue (Less.head _ _ h₁)

library/init/lean/syntax.lean

@@ -47,14 +47,14 @@ inductive IsNode : Syntax → Prop
 
 def SyntaxNode : Type := {s : Syntax // IsNode s }
 
-def notIsNodeMissing (h : IsNode Syntax.missing) : False                   := match h with end
-def notIsNodeAtom   {info val} (h : IsNode (Syntax.atom info val)) : False := match h with end
-def notIsNodeIdent  {info rawVal val preresolved} (h : IsNode (Syntax.ident info rawVal val preresolved)) : False := match h with end
+def notIsNodeMissing (h : IsNode Syntax.missing) : False                   := nomatch h
+def notIsNodeAtom   {info val} (h : IsNode (Syntax.atom info val)) : False := nomatch h
+def notIsNodeIdent  {info rawVal val preresolved} (h : IsNode (Syntax.ident info rawVal val preresolved)) : False := nomatch h
 
 def unreachIsNodeMissing {α : Type} (h : IsNode Syntax.missing) : α := False.elim (notIsNodeMissing h)
 def unreachIsNodeAtom {α : Type} {info val} (h : IsNode (Syntax.atom info val)) : α := False.elim (notIsNodeAtom h)
 def unreachIsNodeIdent {α : Type} {info rawVal val preresolved} (h : IsNode (Syntax.ident info rawVal val preresolved)) : α :=
-False.elim (match h with end)
+False.elim (nomatch h)
 
 @[inline] def withArgs {α : Type} (n : SyntaxNode) (fn : Array Syntax → α) : α :=
 match n with

src/frontends/lean/match_expr.cpp

@@ -40,13 +40,6 @@ expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
 
         p.check_token_next(get_with_tk(), "invalid 'match' expression, 'with' expected");
 
-        if (p.curr_is_token(get_end_tk())) {
-            /* Empty match */
-            p.next();
-            eqns.push_back(Fun(fn, mk_no_equation()));
-            expr f = p.save_pos(mk_equations(header, eqns.size(), eqns.data()), pos);
-            return p.mk_app(f, ts, pos);
-        }
         unsigned case_column = p.pos().second;
         if (is_eqn_prefix(p))
             p.next(); // optional '|' in the first case