A pointer to a derived class is accepted where a pointer to its base is expected, in declarations, assignments, arguments, returns, comparisons and the branches of ?:. It is the only conversion between class types, and the other direction is a type error.

\dfrac{D \text{ derives from } B}{D* \approx B*}\;\textsf{(Subsumption)}

A virtual method is chosen by the class tag T of the receiver, the nearest declaration in the chain of T, so a call through a base pointer reaches the override of the derived class. A non virtual method is chosen by the static class S.

A derived class redefines only a method the base declares virtual, and marks it override, so the method reached from S and the one reached from T coincide for every non virtual method.

Redefining a non virtual method, marking override without a virtual method in a base, or changing the signature is a type error.

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.

The command delete e applies to a pointer to a class or to an object type of the library, whose rule DeleteLib is in Definition 8.1.2.

On an object it runs the destructors of the chain from the tag up to the root, each with this bound to the object, and removes the record and the field locations from \sigma.

A second delete, a delete through a pointer to a base without a virtual destructor in its chain, and any later access are error, the three cases C++17 leaves undefined. delete nullptr does nothing, as in C++.

\dfrac{\Gamma \vdash e : C*}{\Gamma \vdash \mathtt{delete}\ e \dashv \Gamma}\;\textsf{(T-Delete)}

\dfrac{\Gamma \vdash e : L\langle\bar{\tau}\rangle* \qquad L\langle\bar{\tau}\rangle \text{ an object type} \qquad \Gamma \vdash_L \mathtt{delete} : \to \mathsf{void}}{\Gamma \vdash \mathtt{delete}\ e \dashv \Gamma}\;\textsf{(T-DeleteLib)}

\dfrac{\begin{array}{c} \rho, \sigma \vdash e \Rightarrow \mathsf{loc}\,\ell, \sigma_0\qquad \sigma_0(\ell) = \mathsf{obj}\,T\,[f_1 \mapsto \ell_1, \ldots, f_n \mapsto \ell_n] \\ S \text{ the static class of } e\qquad S = T \text{ or the chain of } S \text{ has a virtual destructor} \\ \text{the destructors of the chain of } T \text{ run from } T \text{ up, giving } \sigma_1 \end{array}}{\rho, \sigma \vdash \mathtt{delete}\ e \Rightarrow \mathsf{normal}, \rho, \sigma_1 \setminus \{\ell, \ell_1, \ldots, \ell_n\}}\;\textsf{(Delete)}

\dfrac{\rho, \sigma \vdash e \Rightarrow \mathsf{null}, \sigma_0}{\rho, \sigma \vdash \mathtt{delete}\ e \Rightarrow \mathsf{normal}, \rho, \sigma_0}\;\textsf{(DeleteNull)}

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.