The header <vector> declares template <typename T> class vector; in namespace std. A vector is an object, created with new and reached by pointer. Its value \mathsf{lib}\ \mathtt{std{:}{:}vector}\,[\ell_0, \ldots, \ell_{n-1}] holds one location per element.

The element type has values and a default, so it is not a class, a type of the library, a function type, void or \mathsf{nullptr\_t}. A vector therefore holds pointers to objects and never objects.

\dfrac{}{\Gamma \vdash_{\mathit{vector}} \mathtt{new} : \mathsf{int} \to \mathtt{std{:}{:}vector}\langle\tau\rangle*}\;\textsf{(TV-New)}

\dfrac{}{\Gamma \vdash_{\mathit{vector}} \mathtt{operator[]} : \mathsf{int} \to \tau}\;\textsf{(TV-Index)}

The use operator[] gives a location, so v[i] may stand on the left of an assignment and bind a reference.

\dfrac{\begin{array}{c} k \ge 0\qquad (\ell_i, \sigma_i) = \mathrm{alloc}(\sigma_{i-1}, \mathrm{default}\,\tau)\ (1 \le i \le k) \\ (\ell, \sigma') = \mathrm{alloc}(\sigma_k, \mathsf{lib}\ \mathtt{std{:}{:}vector}\,[\ell_1, \ldots, \ell_k]) \end{array}}{\sigma_0 \vdash_{\mathit{vector}} \mathtt{new}\langle\tau\rangle(k) \Rightarrow \mathsf{loc}\,\ell, \sigma'}\;\textsf{(V-New)}

\dfrac{0 \le i < n}{\sigma \vdash_{\mathit{vector}} \mathtt{operator[]}(\mathsf{lib}\ \mathtt{std{:}{:}vector}\,[\ell_0, \ldots, \ell_{n-1}], i) \Rightarrow \ell_i, \sigma}\;\textsf{(V-Index)}

\dfrac{}{\sigma \vdash_{\mathit{vector}} \mathtt{delete}(\mathsf{lib}\ \mathtt{std{:}{:}vector}\,[\ell_0, \ldots, \ell_{n-1}]) \Rightarrow \mathsf{void}, \sigma \setminus \{\ell_0, \ldots, \ell_{n-1}\}}\;\textsf{(V-Delete)}

A negative size and an index outside [0, n) are error, where C++17 leaves the index undefined. The receiver is evaluated before the index, the order C++17 fixes for operator[].

The header <functional> declares template <typename F> class function; in namespace std. The template argument is a function type \tau(\tau_1, \ldots, \tau_k). A value of the instance is the closure of a lambda. It is not an object and has no default, so no field and no element has the type.

\dfrac{}{\Gamma \vdash_{\mathit{function}} \tau(\tau_1, \ldots, \tau_k) \hookrightarrow \mathtt{std{:}{:}function}\langle\tau(\tau_1, \ldots, \tau_k)\rangle}\;\textsf{(TF-Conv)}

\dfrac{\text{at } \mathtt{std{:}{:}function}\langle\tau(\tau_1, \ldots, \tau_k)\rangle}{\Gamma \vdash_{\mathit{function}} \mathtt{operator()} : \tau_1 \times \cdots \times \tau_k \to \tau}\;\textsf{(TF-Call)}

\dfrac{\sigma \vdash \mathrm{apply}(v, v_1, \ldots, v_k) \Rightarrow v', \sigma'}{\sigma \vdash_{\mathit{function}} \mathtt{operator()}(v, v_1, \ldots, v_k) \Rightarrow v', \sigma'}\;\textsf{(F-Call)}

The premise of F-Call is the application of a closure, the one judgment of the language an intrinsic uses. The type is convertible, so two overloads that differ only in a parameter of this type are indistinguishable, Definition 7.1.1.

The header <cassert> declares void assert(bool condition);. In C++ assert is a macro, and with NDEBUG undefined a failed assertion calls abort (N1570 §7.2.1.1). Core C++ gives error, which ends with the same exit status.

\dfrac{}{\Gamma \vdash_{\mathit{assert}} \mathtt{call} : \mathsf{bool} \to \mathsf{void}}\;\textsf{(TA-Call)}

\dfrac{}{\sigma \vdash_{\mathit{assert}} \mathtt{call}(\mathtt{true}) \Rightarrow \mathsf{void}, \sigma}\;\textsf{(A-True)}

\dfrac{}{\sigma \vdash_{\mathit{assert}} \mathtt{call}(\mathtt{false}) \Rightarrow \mathsf{error}}\;\textsf{(A-False)}