fix: pretty print empty matchers as nomatch

/cc @leodemoura

src/Lean/Delaborator.lean

@@ -442,15 +442,21 @@ def delabAppMatch : Delab := whenPPOption getPPNotation do
       else
         pure { st with moreArgs := st.moreArgs.push (← delab) })
 
-  if st.rhss.size < st.info.altNumParams.size then
+  if st.discrs.size < st.info.numDiscrs || st.rhss.size < st.info.altNumParams.size then
     -- underapplied
     failure
 
-  let pats ← delabPatterns st
-  let discrs := st.discrs.map fun discr => mkNode `Lean.Parser.Term.matchDiscr #[mkNullNode, discr]
-  let alts := pats.zipWith st.rhss fun pat rhs => mkNode `Lean.Parser.Term.matchAlt #[pat, mkAtom "=>", rhs]
-  let stx ← `(match $(mkSepArray discrs (mkAtom ",")):matchDiscr* with | $(mkSepArray alts (mkAtom "|")):matchAlt*)
-  Syntax.mkApp stx st.moreArgs
+  match st.discrs, st.rhss with
+  | #[discr], #[] =>
+    let stx ← `(nomatch $discr)
+    Syntax.mkApp stx st.moreArgs
+  | _,        #[] => failure
+  | _,        _   =>
+    let discrs := st.discrs.map fun discr => mkNode `Lean.Parser.Term.matchDiscr #[mkNullNode, discr]
+    let pats ← delabPatterns st
+    let alts := pats.zipWith st.rhss fun pat rhs => mkNode `Lean.Parser.Term.matchAlt #[pat, mkAtom "=>", rhs]
+    let stx ← `(match $(mkSepArray discrs (mkAtom ",")):matchDiscr* with | $(mkSepArray alts (mkAtom "|")):matchAlt*)
+    Syntax.mkApp stx st.moreArgs
 
 @[builtinDelab mdata]
 def delabMData : Delab := do

tests/lean/match1.lean

@@ -148,3 +148,5 @@ def g {α} : List α → Nat
   | _   => 0
 
 #check g.match_1
+
+#check fun (e : Empty) => (nomatch e : False)

tests/lean/match1.lean.expected.out

@@ -48,3 +48,4 @@ fun (x : Array Nat) =>
   | x_1 => 4 : Array Nat → Nat
 g.match_1 : (motive : List ?m → Sort _) →
   (x : List ?m) → ((a : ?m) → motive [a]) → ((x_1 : List ?m) → motive x_1) → motive x
+fun (e : Empty) => nomatch e : (e : Empty) → (fun (e_1 : Empty) => False) e