From bbad6d1efe7464ac9ea860fdb579279928b100f1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 26 Jul 2022 15:13:28 -0700
Subject: [PATCH] feat: add `with_annotate_term`

---
 src/Init/Notation.lean         | 3 +++
 src/Lean/Elab/BuiltinTerm.lean | 6 ++++++
 2 files changed, 9 insertions(+)

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index a60cf45bdb..8b2e7ae892 100644
--- a/src/Init/Notation.lean
+++ b/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
diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean
index bd759892c1..229faee57e 100644
--- a/src/Lean/Elab/BuiltinTerm.lean
+++ b/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