From 7cfd3f13ca75f6ecbab46dedbc506905cff11167 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jan 2020 17:48:18 -0800 Subject: [PATCH] chore: update function name --- src/Init/Lean/Elab/Syntax.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Elab/Syntax.lean b/src/Init/Lean/Elab/Syntax.lean index d773625acc..18c77e696a 100644 --- a/src/Init/Lean/Elab/Syntax.lean +++ b/src/Init/Lean/Elab/Syntax.lean @@ -168,7 +168,7 @@ fun stx => do trace `Elab stx $ fun _ => d; withMacroExpansion stx $ elabCommand d -@[builtinCommandElab «macro_rules»] def elabMacro : CommandElab := +@[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab := adaptExpander $ fun stx => match_syntax stx with | `(macro_rules $alts*) => do -- TODO: clean up with matchAlt quotation