What's "@&" in external function defination?

Stream: lean4

[HT]

I want to try programming in Lean, don't find what it does. It looks @& S corresponds to b_lean_obj_arg .

@[extern "lean_S_string"] constant S.string (s : @& S) : String

extern "C" lean_object * lean_S_string(b_lean_obj_arg s) {
    return lean::mk_string(to_S(s)->m_s);
}

[Notification Bot]

This topic was moved here from #new members > What's "@&" in external function defination? by Mario Carneiro

[Mario Carneiro]

If you are familiar with Rust or C++, this is like &Foo in function arguments, although a much simplified form. It is used on @[extern] functions to determine the calling convention on the C side: if it is passed by reference then the reference count of arguments to the function doesn't need to be incremented.

FYI, this is a lean 4 specific feature. Lean 4 is still under development and is in alpha stage, lean 3 is the latest stable version and what most mathlib users are using.

[Marc Huisinga]

If you want to learn about the formal details, see https://arxiv.org/pdf/1908.05647.pdf. @& is an explicit borrow annotation, which are inferred automatically for regular Lean code (see 5.2 in the paper).