From 0883f96da0e2afafda7fb81de61767c214ff343e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 2 Sep 2020 13:18:45 -0700
Subject: [PATCH] chore: remove `optional partial` from 'let rec'

It will inherit the parent declaration annotation.
---
 src/Lean/Elab/LetRec.lean | 18 ++++--------------
 src/Lean/Parser/Term.lean |  2 +-
 2 files changed, 5 insertions(+), 15 deletions(-)

diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean
index 72b04c2af2..2a9d90a1b7 100644
--- a/src/Lean/Elab/LetRec.lean
+++ b/src/Lean/Elab/LetRec.lean
@@ -18,30 +18,20 @@ structure LetRecDeclView :=
 
 structure LetRecView :=
 (ref       : Syntax)
-(isPartial : Bool)
 (decls     : Array LetRecDeclView)
 (body      : Syntax)
 
 private def mkLetRecView (letRec : Syntax) : LetRecView :=
-let decls     := (letRec.getArg 2).getArgs.getSepElems.map fun attrDeclSyntax =>
+let decls     := (letRec.getArg 1).getArgs.getSepElems.map fun attrDeclSyntax =>
   { attrs := attrDeclSyntax.getArg 0, decl := (attrDeclSyntax.getArg 1).getArg 0 : LetRecDeclView };
 { decls     := decls,
   ref       := letRec,
-  isPartial := !(letRec.getArg 1).isNone,
-  body      := letRec.getArg 4 }
+  body      := letRec.getArg 3 }
 
 def LetRecView.review (view : LetRecView) : Syntax :=
 let result := view.ref;
-let result := result.setArg 4 view.body;
-let result :=
-  if view.isPartial then
-    if (result.getArg 1).isNone then
-      result.setArg 1 (mkNullNode #[mkAtomFrom result "partial "])
-    else
-      result
-  else
-    result.setArg 1 mkNullNode;
-let result := result.setArg 2 $ mkSepStx
+let result := result.setArg 3 view.body;
+let result := result.setArg 1 $ mkSepStx
     (view.decls.map fun decl => mkNullNode #[decl.attrs, mkNode `Lean.Parser.Term.letDecl #[decl.decl]])
     (mkAtomFrom result ", ");
 result
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index c56ada203f..bd5fd9a547 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -133,7 +133,7 @@ def attrArg : Parser := ident <|> strLit <|> numLit
 def attrInstance     := parser! rawIdent >> many attrArg
 def attributes       := parser! "@[" >> sepBy1 attrInstance ", " >> "]"
 @[builtinTermParser] def «letrec» :=
-    parser!:leadPrec group ("let " >> nonReservedSymbol "rec ") >> optional ("partial ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", " >> "; " >> termParser
+    parser!:leadPrec group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", " >> "; " >> termParser
 
 def leftArrow : Parser := unicodeSymbol " ← " " <- "
 def doLet  := parser! "let ">> letDecl