diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index 116c72787a..619a3ea1b8 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -780,6 +780,20 @@ fun _ c s =>
 { fn   := identFn,
   info := mkAtomicInfo "ident" }
 
+def fieldIdxFn : BasicParserFn :=
+fun c s =>
+  let iniPos := s.pos;
+  let curr     := c.input.get iniPos;
+  if curr.isDigit && curr != '0' then
+    let s     := takeWhileFn (fun c => c.isDigit) c s;
+    mkNodeToken fieldIdxKind iniPos c s
+  else
+    s.mkErrorAt "expected field index" iniPos
+
+@[inline] def fieldIdx {k : ParserKind} : Parser k :=
+{ fn   := fun _ => fieldIdxFn,
+  info := mkAtomicInfo "fieldIdx" }
+
 instance string2basic {k : ParserKind} : HasCoe String (Parser k) :=
 ⟨symbol⟩
 
diff --git a/library/init/lean/syntax.lean b/library/init/lean/syntax.lean
index 12c43ad834..edc06051c2 100644
--- a/library/init/lean/syntax.lean
+++ b/library/init/lean/syntax.lean
@@ -35,6 +35,7 @@ abbrev SyntaxNodeKind := Name
 @[matchPattern] def nullKind : SyntaxNodeKind := `null
 def strLitKind : SyntaxNodeKind := `strLit
 def numLitKind : SyntaxNodeKind := `numLit
+def fieldIdxKind : SyntaxNodeKind := `fieldIdx
 
 /- Syntax AST -/
 
@@ -316,9 +317,9 @@ else
   else if c.isDigit then decodeDecimalLitAux s 0 0
   else none
 
-def isNatLit : Syntax → Option Nat
+def isNatLitAux (nodeKind : SyntaxNodeKind) : Syntax → Option Nat
 | (Syntax.node k args _) :=
-  if k == numLitKind && args.size == 1 then
+  if k == nodeKind && args.size == 1 then
     match args.get 0 with
     | (Syntax.atom _ val) => decodeNatLitVal val
     | _ => none
@@ -326,6 +327,12 @@ def isNatLit : Syntax → Option Nat
     none
 | _ := none
 
+def isNatLit (s : Syntax) : Option Nat :=
+isNatLitAux numLitKind s
+
+def isFieldIdx (s : Syntax) : Option Nat :=
+isNatLitAux fieldIdxKind s
+
 def isIdOrAtom : Syntax → Option String
 | (Syntax.atom _ val)           := some val
 | (Syntax.ident _ rawVal _ _ _) := some rawVal.toString