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

chore: use Tactic.seq1 instead of Tactic.tacticSeq1Indented

Browse source 
Reason: antiquotations.
This commit is contained in:
Leonardo de Moura 2020-10-06 08:17:02 -07:00
parent 71e6ab2a06
commit 10fc908463
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Parser/Syntax.lean
View file

@ -84,7 +84,7 @@ def optKindPrio : Parser := optional ("[" >> (parserKindPrio <|> parserKind <|>
def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> syntaxParser maxPrec
def macroArg := try strLit <|> try macroArgSimple
def macroHead := macroArg <|> try ident
def macroTailTactic : Parser := try (" : " >> identEq "tactic") >> darrow >> ("`(" >> toggleInsideQuot Tactic.tacticSeq1Indented >> ")" <|> termParser)
def macroTailTactic : Parser := try (" : " >> identEq "tactic") >> darrow >> ("`(" >> toggleInsideQuot Tactic.seq1 >> ")" <|> termParser)
def macroTailCommand : Parser := try (" : " >> identEq "command") >> darrow >> ("`(" >> toggleInsideQuot (many1Unbox commandParser) >> ")" <|> termParser)
def macroTailDefault : Parser := try (" : " >> ident) >> darrow >> (("`(" >> toggleInsideQuot (categoryParserOfStack 2) >> ")") <|> termParser)
def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault

2
src/Lean/Parser/Term.lean
View file

@ -260,7 +260,7 @@ stx.isAntiquot || stx.isIdent
end Term
@[builtinTermParser 1] def Tactic.quot : Parser := parser! "`(tactic|" >> toggleInsideQuot tacticParser >> ")"
@[builtinTermParser] def Tactic.quotSeq : Parser := parser! "`(tactic|" >> toggleInsideQuot Tactic.tacticSeq1Indented >> ")"
@[builtinTermParser] def Tactic.quotSeq : Parser := parser! "`(tactic|" >> toggleInsideQuot Tactic.seq1 >> ")"
@[builtinTermParser] def Level.quot : Parser := parser! "`(level|" >> toggleInsideQuot levelParser >> ")"