From be571e8d4237238fa10a575037bc50323ebd5cfd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 Jan 2020 19:41:17 -0800 Subject: [PATCH] feat: elaborate new macro argument types --- src/Init/Lean/Elab/Syntax.lean | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/Init/Lean/Elab/Syntax.lean b/src/Init/Lean/Elab/Syntax.lean index 70f70c4dc2..1feddd5428 100644 --- a/src/Init/Lean/Elab/Syntax.lean +++ b/src/Init/Lean/Elab/Syntax.lean @@ -263,7 +263,14 @@ else def expandMacroArgIntoSyntaxItem (stx : Syntax) : CommandElabM Syntax := let k := stx.getKind; if k == `Lean.Parser.Command.macroArgSimple then - pure $ Syntax.node `Lean.Parser.Syntax.cat #[stx.getArg 2, stx.getArg 3] + let argType := stx.getArg 2; + match argType with + | Syntax.atom _ "ident" => pure $ Syntax.node `Lean.Parser.Syntax.ident #[argType] + | Syntax.atom _ "num" => pure $ Syntax.node `Lean.Parser.Syntax.num #[argType] + | Syntax.atom _ "str" => pure $ Syntax.node `Lean.Parser.Syntax.str #[argType] + | Syntax.atom _ "char" => pure $ Syntax.node `Lean.Parser.Syntax.char #[argType] + | Syntax.ident _ _ _ _ => pure $ Syntax.node `Lean.Parser.Syntax.cat #[stx.getArg 2, stx.getArg 3] + | _ => throwUnsupportedSyntax else if k == `Lean.Parser.Command.strLitPrec then pure $ Syntax.node `Lean.Parser.Syntax.atom stx.getArgs else