From 2b9df7d8b9d8535e8ee2b076f6c0feb36b5fdf11 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 7 Apr 2021 22:01:10 -0700 Subject: [PATCH] chore: make it clear that implementation relies on the fact that both branches of the `if-then-else` generate a node with the same kind Motivation: we want to change the kind used in the `group` combinator. --- src/Lean/Parser/Term.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 25b283f8e3..71a3da1b5d 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -91,7 +91,7 @@ def optType : Parser := optional typeSpec @[builtinTermParser] def explicit := leading_parser "@" >> termParser maxPrec @[builtinTermParser] def inaccessible := leading_parser ".(" >> termParser >> ")" def binderIdent : Parser := ident <|> hole -def binderType (requireType := false) : Parser := if requireType then group (" : " >> termParser) else optional (" : " >> termParser) +def binderType (requireType := false) : Parser := if requireType then node nullKind (" : " >> termParser) else optional (" : " >> termParser) def binderTactic := leading_parser atomic (symbol " := " >> " by ") >> Tactic.tacticSeq def binderDefault := leading_parser " := " >> termParser def explicitBinder (requireType := false) := ppGroup $ leading_parser "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")"