diff --git a/library/init/lean/parser/command.lean b/library/init/lean/parser/command.lean
index 369570f497..1b96653662 100644
--- a/library/init/lean/parser/command.lean
+++ b/library/init/lean/parser/command.lean
@@ -38,7 +38,8 @@ def «protected»      := parser! "protected "
 def visibility       := «private» <|> «protected»
 def «noncomputable»  := parser! "noncomputable "
 def «unsafe»         := parser! "unsafe "
-def declModifiers    := parser! optional docComment >> optional «attributes» >> optional visibility >> optional «noncomputable» >> optional «unsafe»
+def «partial»        := parser! "partial "
+def declModifiers    := parser! optional docComment >> optional «attributes» >> optional visibility >> optional «noncomputable» >> optional «unsafe» >> optional «partial»
 def declId           := parser! ident >> optional (".{" >> sepBy1 ident ", " >> "}")
 def declSig          := parser! many Term.bracktedBinder >> Term.typeSpec
 def optDeclSig       := parser! many Term.bracktedBinder >> Term.optType