diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 9e4da15fd0..7142f101df 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1673,6 +1673,7 @@ instance : Inhabited Syntax where /- Builtin kinds -/ def choiceKind : SyntaxNodeKind := `choice def nullKind : SyntaxNodeKind := `null +def groupKind : SyntaxNodeKind := `group def identKind : SyntaxNodeKind := `ident def strLitKind : SyntaxNodeKind := `strLit def charLitKind : SyntaxNodeKind := `charLit diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index e48995994d..d087d02b64 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -283,7 +283,7 @@ private def toFieldLHS (stx : Syntax) : Except String FieldLHS := return FieldLHS.modifyOp stx stx[1] else -- Note that the representation of the first field is different. - let stx := if stx.getKind == nullKind then stx[1] else stx + let stx := if stx.getKind == groupKind then stx[1] else stx if stx.isIdent then return FieldLHS.fieldName stx stx.getId.eraseMacroScopes else match stx.isFieldIdx? with diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean index 4b4fcaf925..d5aeee2098 100644 --- a/src/Lean/Parser/Extra.lean +++ b/src/Lean/Parser/Extra.lean @@ -49,7 +49,7 @@ attribute [runBuiltinParserAttributeHooks] withAntiquot (mkAntiquot "nameLit" nameLitKind) nameLitNoAntiquot @[runBuiltinParserAttributeHooks, inline] def group (p : Parser) : Parser := - node nullKind p + node groupKind p @[runBuiltinParserAttributeHooks, inline] def many1Indent (p : Parser) : Parser := withPosition $ many1 (checkColGe "irrelevant" >> p)