fix: letDecl

use `simpleBinderWithoutType` at `declSig` and `optDeclSig`

src/Lean/Parser/Command.lean

@@ -33,8 +33,8 @@ def «unsafe»         := parser! "unsafe "
 def «partial»        := parser! "partial "
 def declModifiers (inline : Bool) := parser! optional docComment >> optional (Term.«attributes» >> if inline then skip else ppDedent ppLine) >> optional visibility >> optional «noncomputable» >> optional «unsafe» >> optional «partial»
 def declId           := parser! ident >> optional (".{" >> sepBy1 ident ", " >> "}")
-def declSig          := parser! many (ppSpace >> Term.bracketedBinder) >> Term.typeSpec
-def optDeclSig       := parser! many (ppSpace >> Term.bracketedBinder) >> Term.optType
+def declSig          := parser! many (ppSpace >> (Term.simpleBinderWithoutType <|> Term.bracketedBinder)) >> Term.typeSpec
+def optDeclSig       := parser! many (ppSpace >> (Term.simpleBinderWithoutType <|> Term.bracketedBinder)) >> Term.optType
 def declValSimple    := parser! " :=\n" >> termParser
 def declValEqns      := parser! Term.matchAlts false
 def declVal          := declValSimple <|> declValEqns

src/Lean/Parser/Term.lean

@@ -149,8 +149,10 @@ def optExprPrecedence := optional («try» ":" >> termParser maxPrec)
 -- NOTE: syntax quotations are defined in Init.Lean.Parser.Command
 @[builtinTermParser] def «match_syntax» := parser!:leadPrec "match_syntax" >> termParser >> " with " >> matchAlts
 
+def simpleBinderWithoutType := node `Lean.Parser.Term.simpleBinder (many1 binderIdent >> pushNone)
+
 /- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/
-def letIdLhs    : Parser := ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> (simpleBinder <|> bracketedBinder)) >> optType
+def letIdLhs    : Parser := ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> (simpleBinderWithoutType <|> bracketedBinder)) >> optType
 def letIdDecl   := node `Lean.Parser.Term.letIdDecl   $ «try» (letIdLhs >> " := ") >> termParser
 def letPatDecl  := node `Lean.Parser.Term.letPatDecl  $ «try» (termParser >> pushNone >> optType >> " := ") >> termParser
 def letEqnsDecl := node `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts false

tests/lean/run/newfrontend1.lean

@@ -371,3 +371,16 @@ def f1 (x : Nat) : Nat :=
   loop x
 
 #eval f1 5
+
+def f2 (x : Nat) : String :=
+  let bad x : String := toString x
+  bad x
+
+def f3 x y :=
+  x + y + 1
+
+theorem f3eq x y : f3 x y = x + y + 1 :=
+  rfl
+
+def f4 x y : String :=
+  if x > y + 1 then "hello" else "world"