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

chore: avoid ! suffix in builtin notation

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-11 10:58:06 -08:00
parent 656b7a8d87
commit ca0baf12b6
2 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Parser/Do.lean
View file

@ -34,7 +34,7 @@ builtin_initialize
def notFollowedByRedefinedTermToken :=
-- Remark: we don't currently support `open` and `set_option` in `do`-blocks, but we include them in the following list to fix the ambiguity
-- "open" command following `do`-block. If we don't add `do`, then users would have to indent `do` blocks or use `{ ... }`.
notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "let" <|> "have" <|> "do" <|> "dbgTrace!" <|> "assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try") "token at 'do' element"
notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "let" <|> "have" <|> "do" <|> "dbgTrace!" <|> "dbg_trace" <|> "assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try") "token at 'do' element"
@[builtinDoElemParser] def doLet := leading_parser "let " >> optional "mut " >> letDecl
@ -105,7 +105,7 @@ def doFinally := leading_parser "finally " >> doSeq
@[builtinDoElemParser] def doBreak := leading_parser "break"
@[builtinDoElemParser] def doContinue := leading_parser "continue"
@[builtinDoElemParser] def doReturn := leading_parser:leadPrec withPosition ("return " >> optional (checkLineEq >> termParser))
@[builtinDoElemParser] def doDbgTrace := leading_parser:leadPrec "dbgTrace! " >> ((interpolatedStr termParser) <|> termParser)
@[builtinDoElemParser] def doDbgTrace := leading_parser:leadPrec (symbol "dbgTrace! " <|> "dbg_trace ") >> ((interpolatedStr termParser) <|> termParser)
@[builtinDoElemParser] def doAssert := leading_parser:leadPrec "assert! " >> termParser
/-

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

@ -182,15 +182,15 @@ def whereDecls := leading_parser "where " >> many1Indent (group (letRecDecl >> o
@[runBuiltinParserAttributeHooks]
def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls
@[builtinTermParser] def noindex := leading_parser "noindex!" >> termParser maxPrec
@[builtinTermParser] def noindex := leading_parser (symbol "noindex! " <|> "no_index ") >> termParser maxPrec
@[builtinTermParser] def binrel := leading_parser "binrel! " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def binrel := leading_parser (symbol "binrel! " <|> "binrel%") >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def forInMacro := leading_parser "forIn! " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def forInMacro := leading_parser (symbol "forIn! " <|> "forIn% ") >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def typeOf := leading_parser "typeOf! " >> termParser maxPrec
@[builtinTermParser] def ensureTypeOf := leading_parser "ensureTypeOf! " >> termParser maxPrec >> strLit >> termParser
@[builtinTermParser] def ensureExpectedType := leading_parser "ensureExpectedType! " >> strLit >> termParser maxPrec
@[builtinTermParser] def typeOf := leading_parser (symbol "typeOf! " <|> "typeOf% ") >> termParser maxPrec
@[builtinTermParser] def ensureTypeOf := leading_parser (symbol "ensureTypeOf! " <|> "ensureTypeOf% ") >> termParser maxPrec >> strLit >> termParser
@[builtinTermParser] def ensureExpectedType := leading_parser (symbol "ensureExpectedType! " <|> "ensureExpectedType% ") >> strLit >> termParser maxPrec
def namedArgument := leading_parser atomic ("(" >> ident >> " := ") >> termParser >> ")"
def ellipsis := leading_parser ".."
@ -223,7 +223,7 @@ def bracketedBinderF := bracketedBinder -- no default arg
@[builtinTermParser] def panic := leading_parser:leadPrec "panic! " >> termParser
@[builtinTermParser] def unreachable := leading_parser:leadPrec "unreachable!"
@[builtinTermParser] def dbgTrace := leading_parser:leadPrec withPosition ("dbgTrace! " >> ((interpolatedStr termParser) <|> termParser)) >> optSemicolon termParser
@[builtinTermParser] def dbgTrace := leading_parser:leadPrec withPosition ((symbol "dbgTrace! " <|> "dbg_trace") >> ((interpolatedStr termParser) <|> termParser)) >> optSemicolon termParser
@[builtinTermParser] def assert := leading_parser:leadPrec withPosition ("assert! " >> termParser) >> optSemicolon termParser