From a276b59a80f12187e838fba28a127ff096fe478c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 11 Feb 2020 08:59:17 -0800 Subject: [PATCH] feat: allow arbitrary terms after `@` --- src/Init/Lean/Parser/Term.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean index 3c0ce25181..5beb5e0b1e 100644 --- a/src/Init/Lean/Parser/Term.lean +++ b/src/Init/Lean/Parser/Term.lean @@ -69,7 +69,7 @@ def optType : Parser := optional typeSpec @[builtinTermParser] def subtype := parser! "{" >> ident >> optType >> " // " >> termParser >> "}" @[builtinTermParser] def listLit := parser! symbol "[" appPrec >> sepBy termParser "," true >> "]" @[builtinTermParser] def arrayLit := parser! symbol "#[" appPrec >> sepBy termParser "," true >> "]" -@[builtinTermParser] def explicit := parser! symbol "@" appPrec >> id +@[builtinTermParser] def explicit := parser! symbol "@" appPrec >> termParser appPrec @[builtinTermParser] def inaccessible := parser! symbol ".(" appPrec >> termParser >> ")" def binderIdent : Parser := ident <|> hole def binderType (requireType := false) : Parser := if requireType then group (" : " >> termParser) else optional (" : " >> termParser)