Zulip Chat Archive

Stream: lean4

Topic: What does '@&' mean?


Yuri de Wit (Feb 24 2022 at 20:37):

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 (Feb 24 2022 at 20:39):

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 (Feb 24 2022 at 20:41):

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


Last updated: Dec 20 2023 at 11:08 UTC