A class has an optional base, fields and methods with a visibility, at most one constructor named after the class and at most one destructor. Members before the first section label are private, as in C++.

The class is well formed when the base exists and the chain is acyclic, the fields have types with values and repeat no field of a base, the members have distinct names, a method that redefines a method of a base finds it virtual there, carries override and keeps the signature, the constructor of the base takes no parameters, and every member body is well typed under this.

\dfrac{\begin{array}{c} B \text{ exists, chain acyclic}\qquad \text{fields storable, well formed, new in the chain} \\ \text{each redefined } m \text{ is virtual in the base, marked override, same signature} \\ B \text{ has no constructor or one without parameters} \\ [\mathtt{this} \mapsto C*, p_1, \ldots, p_k] \vdash c \dashv \Gamma' \text{ for each member body} \end{array}}{\vdash \mathtt{class}\ C\ \mathtt{:}\ \mathtt{public}\ B\ \{ \ldots \}}\;\textsf{(T-Class)}

The context of a member body binds this to C* and the parameters as variables, so the current class is the class of this in \Gamma.

A private member declared in class K is visible exactly when \Gamma(\mathtt{this}) = K*. Visibility is thus a typing rule, and the public section of a class is the signature of an abstract data type while the private section is its representation, reachable only from the member bodies of the class.

\dfrac{C \text{ has } \tau\ f \text{ declared in } K \qquad f \text{ public or } \Gamma(\mathtt{this}) = K*}{\Gamma \vdash e.f : \tau \text{ for } \Gamma \vdash e : C}\;\textsf{(Visible)}

The same premise applies to methods, Definition 6.2.3.

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.

Inside a member body this is the location of the receiver. It is bound in \rho by the call as an alias, never a variable, and it evaluates to a pointer. An unqualified name that is not a variable denotes the member of this, both in the type checker and in the evaluator.

\dfrac{\Gamma(\mathtt{this}) = C*}{\Gamma \vdash \mathtt{this} : C*}\;\textsf{(T-This)}

\dfrac{x \notin \Gamma \qquad \Gamma(\mathtt{this}) = C* \qquad \Gamma \vdash \mathtt{this}\mathtt{->}x : \tau}{\Gamma \vdash x : \tau}\;\textsf{(T-VarField)}

The same holds of a call. An unqualified name that is neither a variable nor a function of the program is a member of the receiver.

\dfrac{\begin{array}{c} f \notin \Gamma\qquad f \text{ is no function of the program}\qquad \Gamma(\mathtt{this}) = C* \\ \Gamma \vdash \mathtt{this}\mathtt{->}f(e_1, \ldots, e_k) : \tau \end{array}}{\Gamma \vdash f(e_1, \ldots, e_k) : \tau}\;\textsf{(T-CallThis)}

\dfrac{\rho(\mathtt{this}) = \ell}{\rho, \sigma \vdash \mathtt{this} \Rightarrow \mathsf{loc}\,\ell, \sigma}\;\textsf{(This)}

\dfrac{x \notin \rho \qquad \rho(\mathtt{this}) = \ell \qquad \sigma(\ell) = \mathsf{obj}\,C\,[\ldots x \mapsto \ell_x \ldots]}{\rho, \sigma \vdash x \Rightarrow_{\ell} \ell_x, \sigma}\;\textsf{(LocVarField)}

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.