feat: add with_annotate_term

src/Init/Notation.lean

@@ -240,4 +240,7 @@ declare_syntax_cat rawStx
 instance : Coe Syntax (TSyntax `rawStx) where
   coe stx := ⟨stx⟩
 
+/-- `with_annotate_term stx e` annotates the lexical range of `stx : Syntax` with term info for `e`. -/
+scoped syntax (name := withAnnotateTerm) "with_annotate_term " rawStx ppSpace term : term
+
 syntax (name := deprecated) "deprecated " (ident)? : attr

src/Lean/Elab/BuiltinTerm.lean

@@ -279,4 +279,10 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
     elabTerm stx[4] expectedType?
 
+@[builtinTermElab withAnnotateTerm] def elabWithAnnotateTerm : TermElab := fun stx expectedType? => do
+  match stx with
+  | `(with_annotate_term $stx $e) =>
+    withInfoContext' stx (elabTerm e expectedType?) (mkTermInfo .anonymous (expectedType? := expectedType?) stx)
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Term