A location \ell is a natural number. Locations are never reused.

The values are \mathsf{int}\,n, \mathsf{bool}\,b, \mathsf{void}, the pointer \mathsf{loc}\,\ell, the value \mathsf{null} of nullptr, the object \mathsf{obj}\,C\,[f_1 \mapsto \ell_1, \ldots, f_n \mapsto \ell_n], a record of one location per field with its class tag, and the instance \mathsf{lib}\,L\,[\ell_0, \ldots, \ell_{n-1}] of an object type L of the library, such as a vector, with one location per element, Definition 8.2.1.

The value \mathsf{void} is the result of a call to a function without return value, and the initial content of a field of function type before the constructor assigns it. The closure is a value too, Definition 2.1.6.

The tag of an object is the class it was created with, its fields are those of the whole chain of classes, the root base first, and the tag decides the dispatch of virtual methods and the destructors that delete runs. Objects and instances of object types of the library live in the store at their own location and are reached only through pointers.

The default value of a type, which new gives to every field and element, is \mathsf{int}\,0, \mathsf{bool}\,\mathtt{false} or \mathsf{null}.

The type int has 32 bits in two's complement. The partial operation \mathsf{int32} returns the integer when it lies in the range and error otherwise.

C++17 fixes neither the width nor the representation of int. A plain int has the natural size suggested by the architecture of the execution environment, with a range of at least [-32767, 32767] (N4659 §6.9.1 paragraph 2 and §21.3.5, N1570 §5.2.4.2.1). Its representation may be two's complement, ones' complement or signed magnitude (N4659 §6.9.1 paragraph 7). The range of int is therefore a property of the platform.

The ABI of the platform fixes it. The System V AMD64 psABI and AAPCS64 both give int 32 bits, and GCC supports only two's complement integer types.

An arithmetic result outside the range of int has undefined behaviour (N4659 §8 paragraph 4), and Core C++ makes it error. That boundary has to be the boundary of the implementation Core C++ is compared with, g++ and clang on x86‑64 and ARM64. A wider range would give a value where C++ gives none, and a narrower one would give error where C++ gives a value.

The representation enters only through the lower bound -2^{31}. Core C++ has no bitwise operators, no shifts and no unsigned types, so no program observes a bit pattern. The width lives only in Int32.min and Int32.max.

\dfrac{n \in [-2^{31},\, 2^{31}-1]}{\mathsf{int32}\,n = \mathsf{int}\,n} \qquad \dfrac{n \notin [-2^{31},\, 2^{31}-1]}{\mathsf{int32}\,n = \mathsf{error}}

The environment \rho is a finite map from identifiers to locations. The notation \rho[x \mapsto \ell] extends \rho, and the most recent binding prevails.

Each binding records whether the declaration that made it allocated the location, as τ x = e does, or aliased an existing one, as the reference τ& y = e does. Block exit frees only the owned locations.

Inside a member body, this is an alias binding to the location of the receiver, made by the call and never freed by the return.

The store \sigma is a finite map from locations to values. The operation \mathrm{alloc}(\sigma, v) returns a fresh location \ell \notin \mathrm{dom}\,\sigma and the store \sigma[\ell \mapsto v]. The operation \sigma \setminus L removes the locations of L from the domain. Reading or writing outside the domain is error.

The value of a lambda is the closure \mathsf{closure}(x_1 \ldots x_k, \tau, c, [y_1 \mapsto w_1, \ldots, y_m \mapsto w_m]), with the parameters, the result type, the body and the captured copies, one value per free variable of the body.

The types std::function<τ(τ₁, …, τₖ)> of Definition 8.2.2 have closures as values.

A variable or a parameter holds a closure, a field or a vector element does not, because new would have to give it a default value and there is no empty function in this subset.

The control result r of a command is \mathsf{normal} or \mathsf{ret}\,v. A \mathsf{ret} interrupts sequence, block and loop up to the call that consumes it.

The result error is not a value of the language. It replaces the result of any dynamic judgment and propagates to the whole program.

Its causes are division by zero, int overflow, the dereference of nullptr, an index outside a vector, a negative vector size, a failed assert, a location outside \sigma, an undeclared variable or function, wrong arity, a missing return in a non void function, a second delete of the same object, and a delete through a pointer to a base class without a virtual destructor.

The typing context \Gamma is a finite map from identifiers to types. The types are \mathsf{int}, \mathsf{bool}, \mathsf{void}, a class C, a pointer \tau*, an instance L\langle\tau_1, \ldots, \tau_k\rangle of a class template of the library, a function type \tau(\tau_1, \ldots, \tau_k) as template argument, and the internal type \mathsf{nullptr\_t} of nullptr.

Class types and the object types of the library are object types, they have no values, and no variable, parameter, result or field has one. An expression of object type occurs only as the operand of ., [] or *.

Each binding carries a mark, read only or not. The mark is set on every binding of the enclosing scope when the body of a lambda is checked, so that the copies of [=] are read and never written.

The function environment gathers the functions a program declares, a finite map from a name to its declaration, built once by the elaboration and implicit in every judgment, which reads it and never changes it. Definition 1.3.1 gives the syntax of the declarations it holds.

The classes of the program form the class table, a finite map from class names to declarations. A declaration has an optional base, fields and methods with their visibility, at most one constructor and at most one destructor.

The table gives, for a class, its chain up to the root base, every field of the chain with the class that declares it, the nearest method of a given name, the subclass relation and whether some class of the chain has a virtual destructor.

The type checker consults it for types, visibility and dispatch, and new and delete for the fields to allocate and to free. Names are qualified by their namespace, N::C.

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.