diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean
index 3d6d6299b1..44bb967565 100644
--- a/library/init/lean/elaborator.lean
+++ b/library/init/lean/elaborator.lean
@@ -277,6 +277,9 @@ def to_pexpr : syntax → elaborator_m expr
   | @inaccessible := do
     let v := view inaccessible stx,
     expr.mk_annotation `innaccessible <$> to_pexpr v.term  -- sic
+  | @borrowed := do
+    let v := view borrowed stx,
+    expr.mk_annotation `borrowed <$> to_pexpr v.term
   | @number := do
     let v := view number stx,
     pure $ expr.lit $ literal.nat_val v.to_nat
diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index 8f16bd0056..900b11391d 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -340,6 +340,10 @@ node! anonymous_inaccessible ["._":max_prec]
 def sorry.parser : term_parser :=
 node! «sorry» ["sorry":max_prec]
 
+@[derive parser.has_tokens parser.has_view]
+def borrowed.parser : term_parser :=
+node! borrowed ["@&":max_prec, term: term.parser]
+
 -- TODO(Sebastian): replace with attribute
 @[derive has_tokens]
 def builtin_leading_parsers : token_map term_parser := token_map.of_list [
@@ -369,7 +373,8 @@ def builtin_leading_parsers : token_map term_parser := token_map.of_list [
   ("{", subtype.parser),
   (".(", inaccessible.parser),
   ("._", anonymous_inaccessible.parser),
-  ("sorry", sorry.parser)
+  ("sorry", sorry.parser),
+  ("@&", borrowed.parser)
 ]
 
 @[derive parser.has_tokens parser.has_view]