From b098cc69eafdfc88481bf5d4296a70b2dc7d4b00 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 22 Jul 2019 15:16:17 -0700 Subject: [PATCH] chore(library/init/lean/elaborator/command): ignore Lean3 notation commands --- library/init/lean/elaborator/command.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/library/init/lean/elaborator/command.lean b/library/init/lean/elaborator/command.lean index 3a677cb5c1..b93a831417 100644 --- a/library/init/lean/elaborator/command.lean +++ b/library/init/lean/elaborator/command.lean @@ -57,5 +57,10 @@ fun n => do | none => unless (checkAnonymousScope scopes) $ throw "invalid 'end', name is missing" | some header => unless (checkEndHeader header scopes) $ throw "invalid 'end', name mismatch" +/- 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 Elab end Lean