What does '@&' mean?

Stream: lean4

[Yuri de Wit]

For example, from Init/Data/Int/Basic.lean:

protected def neg (n : @& Int) : Int :=
  match n with
  | ofNat n   => negOfNat n
  | negSucc n => succ n

I see that it is a notation for marking an expression as 'borrowed', but when and how it is used?

[Henrik Böving]

The notion of borrowed is from the "counting immutable beans" paper and influences how garbage collection works on this particular function. However this notion is actually inserted automatically via a heuristic most of the time and I mean to remember that @Sebastian Ullrich mentioned in the past the compiler even ignores these annotations in favour of its heuristic? But I'm not 100% sure on that.

[Henrik Böving]

Either way it does not matter for the behaviour of the function apart from how garbage collection is performed, you can read/write the function the exact same way with and without the annotation