diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 0103f0c8ba..98755ee815 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -857,6 +857,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 diff --git a/tests/lean/run/nomatch_tac.lean b/tests/lean/run/nomatch_tac.lean new file mode 100644 index 0000000000..59bd9f6dce --- /dev/null +++ b/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