fix: annotate let rec declarations as auxDecl

Reason:
1- Tactics such as `assumption` should ignore them.
2- We must annotate recursive applications with `mkRecAppWithSyntax`.

src/Lean/Elab/LetRec.lean

@@ -79,7 +79,7 @@ private partial def withAuxLocalDecls {α} (views : Array LetRecDeclView) (k : A
   let rec loop (i : Nat) (fvars : Array Expr) : TermElabM α :=
     if h : i < views.size then
       let view := views.get ⟨i, h⟩
-      withLocalDeclD view.shortDeclName view.type fun fvar => loop (i+1) (fvars.push fvar)
+      withLocalDecl view.shortDeclName BinderInfo.auxDecl view.type fun fvar => loop (i+1) (fvars.push fvar)
     else
       k fvars
   loop 0 #[]

tests/lean/letRecMissingAnnotation.lean

@@ -0,0 +1,8 @@
+def sum (as : Array Nat) : Nat :=
+  let rec go (i : Nat) (s : Nat) : Nat :=
+    if h : i < as.size then
+      go (i+2) (s + as.get ⟨i, h⟩) -- Error
+    else
+      s
+  go 0 0
+termination_by measure (fun ⟨a, i, _⟩ => a.size - i)

tests/lean/letRecMissingAnnotation.lean.expected.out

@@ -0,0 +1,5 @@
+letRecMissingAnnotation.lean:4:6-4:34: error: unsolved goals
+as : Array Nat
+i s : Nat
+h : i < Array.size as
+⊢ Array.size as - (i + 2) < Array.size as - i