The literal nullptr has the internal type \mathsf{nullptr\_t}, compatible with every pointer type and with no other. Its value is \mathsf{null}.

\dfrac{}{\Gamma \vdash \mathtt{nullptr} : \mathsf{nullptr\_t}}\;\textsf{(T-Null)}

\dfrac{}{\rho, \sigma \vdash \mathtt{nullptr} \Rightarrow \mathsf{null}, \sigma}\;\textsf{(Null)}

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 expression new C() allocates one location per field of C, each with the default value of its type, then the record itself, tagged with the class, and evaluates to a pointer to the record. Its type is C*. The empty parentheses are the whole argument list for a class without a constructor. A class with a constructor takes its arguments in those parentheses, Definition 6.2.1.

\dfrac{C \mapsto \mathtt{class}\ C\ \{\, \tau_1\, f_1; \ldots; \tau_n\, f_n; \,\}}{\Gamma \vdash \mathtt{new}\ C() : C*}\;\textsf{(T-New)}

\dfrac{\begin{array}{c} C \mapsto \mathtt{class}\ C\ \{\, \tau_1\, f_1; \ldots; \tau_n\, f_n; \,\} \\ (\ell_i, \sigma_i) = \mathrm{alloc}(\sigma_{i-1}, \mathrm{default}\,\tau_i),\ \sigma_0 = \sigma \\ (\ell, \sigma') = \mathrm{alloc}(\sigma_n, \mathsf{obj}\,C\,[f_1 \mapsto \ell_1, \ldots, f_n \mapsto \ell_n]) \end{array}}{\rho, \sigma \vdash \mathtt{new}\ C() \Rightarrow \mathsf{loc}\,\ell, \sigma'}\;\textsf{(New)}

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 dereference *e denotes the location the pointer holds. When the pointer is \mathsf{null} the result is error, where C++17 leaves the dereference undefined.

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

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

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 field access e.f denotes the location of the field f in the record that e denotes, and e->f abbreviates (*e).f, so a null pointer is error. The type of the field comes from the class table.

\dfrac{\Gamma \vdash e : C \qquad C \text{ has } \tau\, f}{\Gamma \vdash_{\ell} e.f : \tau}\;\textsf{(T-LocField)}

\dfrac{\Gamma \vdash e : C* \qquad C \text{ has } \tau\, f}{\Gamma \vdash_{\ell} e\mathtt{->}f : \tau}\;\textsf{(T-LocArrow)}

\dfrac{\rho, \sigma \vdash e \Rightarrow_{\ell} \ell, \sigma' \qquad \sigma'(\ell) = \mathsf{obj}\,C\,[\ldots f \mapsto \ell_f \ldots]}{\rho, \sigma \vdash e.f \Rightarrow_{\ell} \ell_f, \sigma'}\;\textsf{(LocField)}

\dfrac{\rho, \sigma \vdash e \Rightarrow \mathsf{loc}\,\ell, \sigma' \qquad \sigma'(\ell) = \mathsf{obj}\,C\,[\ldots f \mapsto \ell_f \ldots]}{\rho, \sigma \vdash e\mathtt{->}f \Rightarrow_{\ell} \ell_f, \sigma'}\;\textsf{(LocArrow)}

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.

Reading *e, e.f or e->f as a value is reading the content of the location it denotes, one rule for the three forms. Three typing rules give the value the type of the location. An element v[i] of a vector is a use of the library, Definition 8.1.2.

\dfrac{\Gamma \vdash e : \tau*}{\Gamma \vdash {*e} : \tau}\;\textsf{(T-Deref)}

\dfrac{\Gamma \vdash e : C \qquad C \text{ has } \tau\, f}{\Gamma \vdash e.f : \tau}\;\textsf{(T-Field)}

\dfrac{\Gamma \vdash e : C* \qquad C \text{ has } \tau\, f}{\Gamma \vdash e\mathtt{->}f : \tau}\;\textsf{(T-Arrow)}

\dfrac{\rho, \sigma \vdash e \Rightarrow_{\ell} \ell, \sigma' \qquad \ell \in \mathrm{dom}\,\sigma'}{\rho, \sigma \vdash e \Rightarrow \sigma'(\ell), \sigma'}\;\textsf{(Read)}, \quad e \in \{{*e'},\ e'.f,\ e'\mathtt{->}f\}

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.