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

refactor: move notation comands to Syntax.lean

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-15 16:19:27 -08:00
parent d0f7467c95
commit 6ff732f698
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Init/Lean/Elab/Command.lean
View file

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

5
src/Init/Lean/Elab/Syntax.lean
View file

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