max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/lean/elaborator/command): ignore Lean3 notation commands

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-22 15:16:17 -07:00
parent 231c01bf9f
commit b098cc69ea
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/init/lean/elaborator/command.lean
View file

@ -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