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

chore: avoid ! in keywords

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-13 17:24:27 -08:00
parent e04e9ff87e
commit 12aa5cc461
1 changed files with 14 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/Lean/Elab/Quotation.lean
View file

@ -156,24 +156,24 @@ def stxQuot.expand (stx : Syntax) : TermElabM Syntax := do
implementation is "self-stabilizing". It was in fact originally compiled
by an unhygienic prototype implementation. -/
macro "elabStxQuot!" kind:ident : command =>
macro "elab_stx_quot" kind:ident : command =>
`(@[builtinTermElab $kind:ident] def elabQuot : TermElab := adaptExpander stxQuot.expand)
--
elabStxQuot! Parser.Level.quot
elabStxQuot! Parser.Term.quot
elabStxQuot! Parser.Term.funBinder.quot
elabStxQuot! Parser.Term.bracketedBinder.quot
elabStxQuot! Parser.Term.matchDiscr.quot
elabStxQuot! Parser.Tactic.quot
elabStxQuot! Parser.Tactic.quotSeq
elabStxQuot! Parser.Term.stx.quot
elabStxQuot! Parser.Term.prec.quot
elabStxQuot! Parser.Term.attr.quot
elabStxQuot! Parser.Term.prio.quot
elabStxQuot! Parser.Term.doElem.quot
elabStxQuot! Parser.Term.dynamicQuot
elab_stx_quot Parser.Level.quot
elab_stx_quot Parser.Term.quot
elab_stx_quot Parser.Term.funBinder.quot
elab_stx_quot Parser.Term.bracketedBinder.quot
elab_stx_quot Parser.Term.matchDiscr.quot
elab_stx_quot Parser.Tactic.quot
elab_stx_quot Parser.Tactic.quotSeq
elab_stx_quot Parser.Term.stx.quot
elab_stx_quot Parser.Term.prec.quot
elab_stx_quot Parser.Term.attr.quot
elab_stx_quot Parser.Term.prio.quot
elab_stx_quot Parser.Term.doElem.quot
elab_stx_quot Parser.Term.dynamicQuot
/- match -/