diff --git a/src/Init/Lean/Elab/BuiltinNotation.lean b/src/Init/Lean/Elab/BuiltinNotation.lean
index 0bf81a2c30..e502678f04 100644
--- a/src/Init/Lean/Elab/BuiltinNotation.lean
+++ b/src/Init/Lean/Elab/BuiltinNotation.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Lean.Elab.Term
+import Init.Lean.Elab.Quotation
 
 namespace Lean
 namespace Elab
@@ -77,6 +78,29 @@ adaptExpander $ fun stx => match_syntax stx with
     body
 | _                      => throwUnexpectedSyntax stx "where"
 
+@[termElab «parser!»] def elabParserMacro : TermElab :=
+adaptExpander $ fun stx => match_syntax stx with
+| `(parser! $e) => do
+  declName? ← getDeclName?;
+  match declName? with
+  | some declName@(Name.str _ s _) => do
+    let kind := quote declName;
+    let s    := quote s;
+    -- TODO simplify the following quotation as soon as we have coercions and autoparams
+    `(HasOrelse.orelse (Lean.Parser.mkAntiquot $s (some $kind) true) (Lean.Parser.leadingNode $kind $e))
+  | none          => throwError stx "invalid `parser!` macro, it must be used in definitions"
+  | _             => throwError stx "invalid `parser!` macro, unexpected declaration name"
+| _             => throwUnexpectedSyntax stx "parser!"
+
+@[termElab «tparser!»] def elabTParserMacro : TermElab :=
+adaptExpander $ fun stx => match_syntax stx with
+| `(tparser! $e) => do
+  declName? ← getDeclName?;
+  match declName? with
+  | some declName => let kind := quote declName; `(Lean.Parser.trailingNode $kind $e)
+  | none          => throwError stx "invalid `tparser!` macro, it must be used in definitions"
+| _             => throwUnexpectedSyntax stx "tparser!"
+
 def elabInfix (f : Syntax) : TermElab :=
 fun stx expectedType? => do
   -- term `op` term
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index 8f4e52d11f..bb7f8269d1 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -200,3 +200,5 @@ f a
 #eval run "variables {β σ} universes w1 w2 /-- Testing axiom -/ unsafe axiom Nat.aux.{u, v} (γ : Type w1) (v : Nat) : β → (α : Type _) → v = zero /- Nat.zero -/ → Array α #check @Nat.aux"
 #eval run "def x : Nat := Nat.zero #check x"
 #eval run "def x := Nat.zero #check x"
+#eval run "open Lean.Parser def x := parser! symbol \"foo\" Nat.zero #check x"
+#eval run "open Lean.Parser def x := tparser! symbol \"foo\" Nat.zero #check x"