diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 2be476a55e..7a19240085 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -134,6 +134,7 @@ stx ← quoteSyntax (elimAntiquotChoices quoted); @[builtinTermElab Parser.Term.quot] def elabTermQuot : TermElab := adaptExpander stxQuot.expand @[builtinTermElab Parser.Term.funBinder.quot] def elabfunBinderQuot : TermElab := adaptExpander stxQuot.expand @[builtinTermElab Parser.Tactic.quot] def elabTacticQuot : TermElab := adaptExpander stxQuot.expand +@[builtinTermElab Parser.Term.stx.quot] def elabStxQuot : TermElab := adaptExpander stxQuot.expand /- match_syntax -/ diff --git a/tests/lean/run/stxMacro.lean b/tests/lean/run/stxMacro.lean new file mode 100644 index 0000000000..0474ce332b --- /dev/null +++ b/tests/lean/run/stxMacro.lean @@ -0,0 +1,18 @@ +new_frontend + +-- Macro for the `syntax` category +macro "many " x:stx : stx => `(stx| ($x)*) + +syntax "sum! " (many term:max) : term + +macro_rules +| `(sum! $x*) => do + r ← `(0); + x.foldlM (fun r elem => `($r + $elem)) r + +#check sum! 1 2 3 +#eval sum! 1 2 3 +#check sum! + +theorem ex : sum! 1 2 3 = 6 := +rfl