An intrinsic L has a name, the number of its template parameters, and four judgments. The metavariable \bar{\tau} stands for its template arguments, u for a use, new, delete, a call, or a member such as operator[], and r for a value or a location.

| Judgment | Meaning | Lean | | --- | --- | --- | | \Gamma \vdash_L L\langle\bar{\tau}\rangle\ \mathsf{ok} | the instance is well formed | instOk | | \Gamma \vdash_L u : \tau_1 \times \cdots \times \tau_k \to \tau | the signature of the use u | sig | | \Gamma \vdash_L \tau \hookrightarrow L\langle\bar{\tau}\rangle | the type \tau converts to the instance | convFrom | | \sigma \vdash_L u(v_1, \ldots, v_k) \Rightarrow r, \sigma' | the result of the use u | eval |

The dynamic judgment may use one judgment of the language as a premise, the application of a closure of Definition 5.3.3. Three further marks say how the language treats the values of an instance. An object lives in the store and is reached by pointer, a type without a default is excluded from fields and elements, and a convertible type tells no two overloads apart.

The type checker rewrites every use of the library into the node L.u(e_1, \ldots, e_k), with the receiver as e_1 for a member. A call of a declared function is the use call, a call through a value of an instance is operator(), and indexing is operator[]. The evaluator has one rule for the node, whatever L. The arguments are values, evaluated left to right.

\dfrac{\Gamma \vdash_L L\langle\bar{\tau}\rangle\ \mathsf{ok} \qquad \Gamma \vdash_L \mathtt{new} : \tau_1 \times \cdots \times \tau_k \to \tau \qquad \Gamma \vdash e_i \lhd \tau_i}{\Gamma \vdash \mathtt{new}\ L\langle\bar{\tau}\rangle(e_1, \ldots, e_k) : \tau}\;\textsf{(T-NewLib)}

\dfrac{f \text{ declared by a header} \qquad \Gamma \vdash_f \mathtt{call} : \tau_1 \times \cdots \times \tau_k \to \tau \qquad \Gamma \vdash e_i \lhd \tau_i}{\Gamma \vdash f(e_1, \ldots, e_k) : \tau}\;\textsf{(T-CallLib)}

\dfrac{\Gamma \vdash e : L\langle\bar{\tau}\rangle \qquad \Gamma \vdash_L \mathtt{operator[]} : \tau_1 \to \tau \qquad \Gamma \vdash i \lhd \tau_1}{\Gamma \vdash e[i] : \tau}\;\textsf{(T-IndexLib)}

\dfrac{\begin{array}{c} \Gamma \vdash e : L\langle\bar{\tau}\rangle\qquad \Gamma \vdash_L \mathtt{operator[]} : \tau_1 \to \tau, \text{ a location} \\ \Gamma \vdash i \lhd \tau_1 \end{array}}{\Gamma \vdash_{\ell} e[i] : \tau}\;\textsf{(T-LocIndexLib)}

\dfrac{\rho, \sigma_{i-1} \vdash e_i \Rightarrow v_i, \sigma_i \quad (1 \le i \le k) \qquad \sigma_k \vdash_L \mathtt{new}\langle\bar{\tau}\rangle(v_1, \ldots, v_k) \Rightarrow v, \sigma'}{\rho, \sigma_0 \vdash \mathtt{new}\ L\langle\bar{\tau}\rangle(e_1, \ldots, e_k) \Rightarrow v, \sigma'}\;\textsf{(NewLib)}

\dfrac{\rho, \sigma_{i-1} \vdash e_i \Rightarrow v_i, \sigma_i \quad (1 \le i \le k) \qquad \sigma_k \vdash_L u(v_1, \ldots, v_k) \Rightarrow r, \sigma'}{\rho, \sigma_0 \vdash L.u(e_1, \ldots, e_k) \Rightarrow v, \sigma'}\;\textsf{(Lib)}

In the rule Lib the result is v = r for a value and v = \sigma'(r) for a location. With the same premises, a use that gives a location denotes it.

\dfrac{\rho, \sigma_{i-1} \vdash e_i \Rightarrow v_i, \sigma_i \quad (1 \le i \le k) \qquad \sigma_k \vdash_L u(v_1, \ldots, v_k) \Rightarrow \ell, \sigma'}{\rho, \sigma_0 \vdash L.u(e_1, \ldots, e_k) \Rightarrow_{\ell} \ell, \sigma'}\;\textsf{(LocLib)}

The command delete e on a pointer to an instance frees what the intrinsic owns and then the location of the instance.

\dfrac{\begin{array}{c} \rho, \sigma \vdash e \Rightarrow \mathsf{loc}\,\ell, \sigma_0\qquad \sigma_0(\ell) = \mathsf{lib}\,L\,\bar{\ell} \\ \sigma_0 \vdash_L \mathtt{delete}(\sigma_0(\ell)) \Rightarrow \mathsf{void}, \sigma_1 \end{array}}{\rho, \sigma \vdash \mathtt{delete}\ e \Rightarrow \mathsf{normal}, \rho, \sigma_1 \setminus \{\ell\}}\;\textsf{(DeleteLib)}

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.