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

feat: expand prec.quot and prio.quot, add helper command macro elabStxQuot!

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-14 13:36:26 -08:00
parent 046f4866b6
commit 65bb478f7a
1 changed files with 17 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -122,16 +122,23 @@ def stxQuot.expand (stx : Syntax) : TermElabM Syntax := do
implementation is "self-stabilizing". It was in fact originally compiled
by an unhygienic prototype implementation. -/
@[builtinTermElab Parser.Level.quot] def elabLevelQuot : TermElab := adaptExpander stxQuot.expand
@[builtinTermElab Parser.Term.quot] def elabTermQuot : TermElab := adaptExpander stxQuot.expand
@[builtinTermElab Parser.Term.funBinder.quot] def elabFunBinderQuot : TermElab := adaptExpander stxQuot.expand
@[builtinTermElab Parser.Term.bracketedBinder.quot] def elabBracketedBinderQuot : TermElab := adaptExpander stxQuot.expand
@[builtinTermElab Parser.Term.matchDiscr.quot] def elabMatchDiscrQuot : TermElab := adaptExpander stxQuot.expand
@[builtinTermElab Parser.Tactic.quot] def elabTacticQuot : TermElab := adaptExpander stxQuot.expand
@[builtinTermElab Parser.Tactic.quotSeq] def elabTacticQuotSeq : TermElab := adaptExpander stxQuot.expand
@[builtinTermElab Parser.Term.stx.quot] def elabStxQuot : TermElab := adaptExpander stxQuot.expand
@[builtinTermElab Parser.Term.doElem.quot] def elabDoElemQuot : TermElab := adaptExpander stxQuot.expand
@[builtinTermElab Parser.Term.dynamicQuot] def elabDynamicQuot : TermElab := adaptExpander stxQuot.expand
macro "elabStxQuot!" 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.prio.quot
elabStxQuot! Parser.Term.doElem.quot
elabStxQuot! Parser.Term.dynamicQuot
/- match -/