From 6ff732f6988cfaf269b0923849b67f0f0deacc48 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Jan 2020 16:19:27 -0800 Subject: [PATCH] refactor: move notation comands to `Syntax.lean` --- src/Init/Lean/Elab/Command.lean | 5 ----- src/Init/Lean/Elab/Syntax.lean | 5 +++++ 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean index 440672bd32..8640925132 100644 --- a/src/Init/Lean/Elab/Command.lean +++ b/src/Init/Lean/Elab/Command.lean @@ -483,11 +483,6 @@ fun n => do else elabOpenRenaming body -/- We just ignore Lean3 notation declaration commands. -/ -@[builtinCommandElab «mixfix»] def elabMixfix : CommandElab := fun _ => pure () -@[builtinCommandElab «reserve»] def elabReserve : CommandElab := fun _ => pure () -@[builtinCommandElab «notation»] def elabNotation : CommandElab := fun _ => pure () - @[builtinCommandElab «variable»] def elabVariable : CommandElab := fun n => do -- `variable` bracktedBinder diff --git a/src/Init/Lean/Elab/Syntax.lean b/src/Init/Lean/Elab/Syntax.lean index 66c9ad1751..b1766567f9 100644 --- a/src/Init/Lean/Elab/Syntax.lean +++ b/src/Init/Lean/Elab/Syntax.lean @@ -173,6 +173,11 @@ adaptExpander $ fun stx => match_syntax stx with `(@[macro $(Lean.mkSimpleIdent k)] def myMacro : Macro := fun stx => match_syntax stx with $alts* | _ => throw ()) | _ => throwUnsupportedSyntax +/- We just ignore Lean3 notation declaration commands. -/ +@[builtinCommandElab «mixfix»] def elabMixfix : CommandElab := fun _ => pure () +@[builtinCommandElab «reserve»] def elabReserve : CommandElab := fun _ => pure () +@[builtinCommandElab «notation»] def elabNotation : CommandElab := fun _ => pure () + end Command end Elab end Lean