An infix operator whose left operand is an object, and the indexing of an object, are the calls of members. The left operand decides, so no operator on int or bool changes meaning, and && and || are not overloaded.

\dfrac{\begin{array}{c} \Gamma \vdash e_1 : C\qquad C \text{ has } \mathtt{operator}\oplus \text{ visible from } \Gamma \\ \Gamma \vdash e_1.\mathtt{operator}\oplus(e_2) : \tau \end{array}}{\Gamma \vdash e_1 \oplus e_2 : \tau}\;\textsf{(T-OpBin)}

\dfrac{\begin{array}{c} \Gamma \vdash e : C\qquad C \text{ has } \mathtt{operator[]} \text{ visible from } \Gamma \\ \Gamma \vdash e.\mathtt{operator[]}(i) : \tau \end{array}}{\Gamma \vdash e[i] : \tau}\;\textsf{(T-OpIndex)}

The type checker rewrites both forms into the call of the member, and from there they are ordinary method calls, with the visibility, the overload resolution and the dispatch of a method. The trace shows the rule MethodCall under the infix form, which is the point.

Some of the implementations are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.

A member may return \tau\&. Every return of its body is then over an expression that denotes a location, checked by a walk that does not enter the body of a lambda, because the return of a lambda is the lambda's.

\dfrac{\tau \text{ has values} \qquad \text{every return of } c \text{ is return } e \text{ with } \Gamma \vdash_{\ell} e : \tau}{\vdash \tau\&\ m(\ldots)\ \{c\} \text{ in } C}\;\textsf{(T-RetRef)}

\dfrac{\Gamma \vdash e : C \qquad C \text{ has } \tau\&\ \mathtt{operator[]} \text{ visible from } \Gamma}{\Gamma \vdash_{\ell} e[i] : \tau}\;\textsf{(T-LocOpIndex)}

\dfrac{\Gamma \vdash e : C \qquad C \text{ has } \tau\&\ m(\ldots) \text{ visible from } \Gamma}{\Gamma \vdash_{\ell} e.m(e_1, \ldots, e_k) : \tau}\;\textsf{(T-LocMethod)}

The annotation rewrites the return e of such a member as return &e, the location as a value, an expression no program writes. Its type is the type of the location it denotes.

\dfrac{\Gamma \vdash_{\ell} e : \tau}{\Gamma \vdash \&e : \tau}\;\textsf{(T-LocOf)}

\dfrac{\rho, \sigma \vdash e \Rightarrow_{\ell} \ell, \sigma'}{\rho, \sigma \vdash \&e \Rightarrow \mathsf{loc}\ \ell, \sigma'}\;\textsf{(LocOf)}

\dfrac{\text{the member } m \text{ of } C \text{ returns } \tau\& \qquad \text{member } \ell\ (e_1, \ldots, e_k) \Rightarrow \mathsf{loc}\ \ell', \sigma'}{\rho, \sigma \vdash e.m(e_1, \ldots, e_k) \Rightarrow_{\ell} \ell', \sigma'}\;\textsf{(MethodLoc)}

In value position the same call reads \sigma'(\ell'). A location a member returns is that of a field or of an element of a vector of the receiver, and it survives the call because the object lives in \sigma. A member that returned the location of a parameter by value would return a freed location, and reading it is error, by the general rule of locations outside \sigma.

Some of the implementations are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.