Idris 2中`&`为何是保留符号？其具体用途是什么？

&是Idris 2语法中硬编码的保留符号，没有被纳入可自定义运算符的符号集合，所以你无法将它声明为自定义运算符使用。
它的具体用途有两个核心场景：

• 线性类型参数的简写标记：用来声明线性绑定的参数，和1量化符功能等价。比如写法(&x : Int) -> String 完全等价于(1 x : Int) -> String，表示参数x是线性的，必须在函数体内恰好被使用一次。
• 记录更新的上下文引用标记：在记录字段更新语法中，&用来指代当前正在被更新的记录实例，简化字段引用写法。比如你要更新记录r的count字段，原本需要写record { count = r.count + 1 } r，用&可以简化为record { count = &count + 1 } r，这里&count会自动解析为当前待更新记录的count字段。

你没在编译器源码的运算符定义、测试用例中找到相关说明的原因是，&的处理逻辑在词法分析、语法解析阶段的特殊字符分支中，不属于普通的运算符注册逻辑，也没有作为可重载符号出现在常规测试用例里。

内容的提问来源于stack exchange，提问作者michaelmesser